Carnegie Mellon: The Rare Glitch Project                                                          E. Clarke and D. Kroenig
Formalizing a Protocol Standard
Formalizing TTP/C
l1.  Define set of states
2.  Define set of valid initial states
l
3.  Define transition relation
l
1
4
2
3
5
6
7
8
9
10
1
3
Verification: Prove Properties on paths
l
Verifying properties means that one considers all paths that are allowed by the set of initial states and the transition function. One then checks properties of these paths.