Carnegie Mellon: The Rare Glitch Project E. Clarke
and D. Kroenig
Done
Project Status
lVerification
done using PVS
lAbstraction
hierarchy
lInitial
predicate
lTransition
relation
¤for message slot abstraction level and
abstraction levels above; for MFM code level
¤includes membership service
¤without mode changes, download, and
reconfiguration
lParts
of the Verification of the Membership Service