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
Node 5 has two successor nodes; might be two ways to implement a specific detail as allowed by the standard
One must model them both