An Algorithm for Strengthening State Invariants Generated from Requirements Specications

In earlier work, we developed a xpoint algorithm for automatically generating state invariants, proper-ties that hold in each reachable state of a state ma-chine model, from state-based requirements specica-tions. Such invariants are useful both in validating re-quirements specications and as auxiliary lemmas in proofs that a requirements specication satises other invariant properties. This paper describes a new re-lated algorithm that strengthens state invariants gen-erated by our initial algorithm and demonstrates the new algorithm on a simplied version of an automobile cruise control system. The paper concludes by describ-ing how the two algorithms were used to generate state invariants from a requirements specication of a cryp-tographic device and how the invariants in conjunction with a theorem prover were used to prove formally that the device satises a set of critical security properties. 1