|Title||An Algorithm for Strengthening State Invariants Generated from Requirements Specifications|
|Publication Type||Conference Paper|
|Year of Publication||2001|
|Authors||Jeffords, R., and C. L. Heitmeyer|
|Conference Name||Fifth IEEE Int'l Symp. on Requirements Engineering (RE'01)|
|Conference Location||Toronto, Canada|
In earlier work, we developed a fixpoint algorithm for automatically generating state invariants, properties that hold in each reachable state of a state machine model, from state-based 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 initial 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 a cryptographic 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.
|NRL Publication Release Number|| |