ECE 479: Formal Verification
Model Checking
Widely used in industry.
Model -> Transition System (TS)
Property -> Termporal Logic
Transition System
$M$: <$S$, $S_0$, $R$, $L$>
- $S$: Set of states
- $S_0$: Initial/Reset State
- $R$: Transition Relation
- $L$: Labeling Function
Atomic Propositions: Are like boolean values. Something that can be true or false.
Example
Microwave Controller
Atomic Propositions:
- $S$: Start
- $C$: Door Closed
- $E$: Error
- $H$: Heating
So you now draw the states somewhat like a FSM, with each possible state being represented.
For this example, we have:
$S = { S_1, S_2, S_3, S_4, S_5, S_6, S_7 }$
$S_0 = { S_2 }$
$R = { [S_1, S_2], [S_2, S_5], [S_5, S_2], [S_5, S_3], [S_1, S_3], [S_3, S_1], [S_3, S_6], [S_6, S_7], [S_7, S_4], [S_4, S_4], [S_4, S_3], [S_4, S_1] }$
$L(S_1) = {}$
$L(S_2) = { S, E }$
$L(S_3) = { C }$
$L(S_4) = { C, H }$
$L(S_5) = { S, C, E }$
$L(S_6) = { S, C }$
$L(S_7) = { S, C, H }$
Temporal Logic:
If you unwind the transition system, you get an infinte tree. This is called the Computation Tree
Properties: Temporal Logic: CTL*
-> CTL: Computation Tree Logic