Proceedings Fifth IEEE International Symposium on Requirements Engineering (2001)

Toronto, Canada

Aug. 27, 2001 to Aug. 31, 2001

ISBN: 0-7695-1125-2

pp: 0182

Ralph D. Jeffords , Naval Research Laboratory

Constance L. Heitmeyer , Naval Research Laboratory

ABSTRACT

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.

INDEX TERMS

CITATION

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.

doi:10.1109/ISRE.2001.948558

CITATIONS