Proceedings Fifth IEEE International Symposium on Requirements Engineering (2001)
Aug. 27, 2001 to Aug. 31, 2001
Ralph D. Jeffords , Naval Research Laboratory
Constance L. Heitmeyer , Naval Research Laboratory
Abstract: In earlier work, we developed a fix point algorithm for automatically generating state invariants, properties that hold in each reachable state of a state machine model, from state-base d requirements specifications. Such invariants are useful both in validating requirements specifications and as auxiliary lemmas in proofs that a requirements specification satisfies other invariant properties. This paper describes a new related algorithm that strengthens state invariants generated by our in itial algorithm and demonstrates the new algorithm on a simplified version of an automobile cruise control system. The paper concludes by describing how the two algorithms were used to generate state invariants from a requirements specification of acryptographic device and how the invariants in conjunction with a theorem prover were used to prove formally that the device satisfies a set of critical security properties.
R. D. Jeffords and C. L. Heitmeyer, "An Algorithm for Strengthening State Invariants Generated from Requirements Specifications," Proceedings Fifth IEEE International Symposium on Requirements Engineering(RE), Toronto, Canada, 2001, pp. 0182.