TitleAn Algorithm for Strengthening State Invariants Generated from Requirements Specifications
Publication TypeConference Paper
Year of Publication2001
AuthorsJeffords, R., and C. L. Heitmeyer
Conference NameFifth IEEE Int'l Symp. on Requirements Engineering (RE'01)
Conference LocationToronto, Canada
Abstract

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.

Full Text

JeffordsHeitmeyer2001.pdf

NRL Publication Release Number

01-1221.1-0512