Paper Info
Title
An Algorithm for Strengthening State Invariants Generated from Requirements Specifications
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.
Year
DOI
Venue
2001
10.1109/ISRE.2001.948558
RE
Keywords
Field
DocType
requirements specifications,itial algorithm,state machine model,state invariants,acryptographic device,fix point algorithm,reachable state,strengthening state,requirements specification,new algorithm,new related algorithm,automobile cruise control system,automata,theorem prover,cryptography,invariance,satisfiability,systems analysis,theorem proving,formal specification,state machine,control systems,software engineering,finite state machines,testing,phase detection,requirements,security,algorithms,cruise control,software development,programming,computer algorithms
Invariant (physics),Computer science,Automated theorem proving,Algorithm,Finite-state machine,Formal specification,Theoretical computer science,Mathematical proof,Invariant (mathematics),Fixed point,Software requirements specification
Conference
Citations 
PageRank 
References 
15
0.81
14
Authors
2
Name
Order
Citations
PageRank
Ralph D. Jeffords143434.88
Constance L. Heitmeyer2898151.71