Carnegie Mellon: The Rare Glitch Project                                                          E. Clarke and D. Kroenig
Abstraction Hierarchy: Formalization
Formalizing TTP/C
l
l    Let rx denote the transition relation for level x
l    Let a, b denote levels and let b<a hold.
l           c ra d holds
l     iff   there is a set of states c1, …, cn with
l           ci rb ci+1 for i=1 to n-1 and
l           c1=c and cn=d
l     n can be fixed depending on the level and on c1.
Slide shows states and transition relation. If one considers a transition from, e.g., state 4 to 11, there must be a path in  the machine for the lower level that starts in state 4 and ends in state 11. The number of transitions done by the lower level is fixed in this example (it is exactly the number of macro ticks for the given message slot).