Ralph D. Jeffords
Abstract
This paper describes a compositional proof strategy for verifying properties of requirements specifications. The proof strategy, which may be applied using either a model checker or a theorem prover, uses known state invariants to prove state and transition invariants. Two proof rules are presented: a standard incremental proof rule analogous to Manna and Pnueli's incremental proof rule and a compositional proof rule. The advantage of applying the compositional rule is that it decomposes a large verification problem into smaller problems which often can be solved more efficiently than the larger problem. The steps needed to implement the compositional rule are described, and the results of applying the proof strategy to two examples, a simple cruise control system and a real-world Navy system, are presented. In the Navy example, compositional verification %based on the compositional proof using either theorem proving or model checking was three times faster than verification %model checking using based on the standard incremental (noncompositional) rule. In addition to the two above rules for proving invariants, a new compositional proof rule is presented for circular assume-guarantee proofs of invariants. While in principle the strategy and %the rules described for proving invariants may be applied to any state-based specification with parallel composition of components, the specifications in the paper are expressed in the SCR (Software Cost Reduction) tabular notation, the auxiliary invariants used in the proofs are automatically generated invariants, and the verification is supported by the SCR tools.
- M. Abadi and L. Lamport. Conjoining specifications. ACM Trans. Prog. Lang. and Sys., 17(3):507--535, May 1995.]] Google Scholar
Digital Library
- R. Alur and T. A. Henzinger. Computer-aided verification. draft book manuscript, Sept. 1999.]]Google Scholar
- R. Alur and T. A. Henzinger. Reactive modules. Formal Methods in Sys. Design, 15:7--48, July 1999.]] Google ScholarDigital Library
- M. Archer. TAME: Using PVS strategies for special-purpose theorem proving. Annals of Mathematics and Artificial Intelligence, 29(1--4), February 2001.]] Google ScholarDigital Library
- G. Berry and G. Gonthier. The Esterel synchronous program-ming language: Design, semantics, implementation. Science of Computer Programming, 19, 1992.]] Google ScholarDigital Library
- R. Bharadwaj. A framework for the formal analysis of multi-agent systems. In Proc. Formal Aspects of Multi-Agent Systems (FAMAS'03), Warsaw, Poland, Apr. 2003. ETAPS 2003.]]Google Scholar
- R. Bharadwaj and C. Heitmeyer. Model checking com-plete requirements specifications using abstraction. Auto-mated Software Engineering Journal, 6(1), Jan. 1999.]] Google ScholarDigital Library
- R. Bharadwaj and S. Sims. Salsa: Combining constraint solvers with BDDs for automatic invariant checking. In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2000), Berlin, Mar. 2000.]] Google ScholarDigital Library
- K. M. Chandy and J. Misra. Proofs of networks of processes. IEEE Trans. Softw. Engin., SE-7(4):417--426, Apr. 1981.]]Google ScholarDigital Library
- Y. Choi and M. P. E. Heimdahl. Model checking RSML-e requirements. In Proc. 7th IEEE Int'l Symp. on High Assurance Sys. Engin. (HASE'02), Tokyo, Japan, Oct. 2002.]] Google ScholarDigital Library
- A. Cimatti et al. NuSMV 2: An open source tool for symbolic model checking. In Proc. Computer-Aided Verification (CAV 2002), Copenhagen, Denmark, July 2002.]] Google ScholarDigital Library
- E. M. Clarke, O. Grumberg, and D. A. Peled. Model Check-ing. MIT press, 1999.]] Google ScholarDigital Library
- S. Graf and H. Saidi. Construction of abstract state graphs with PVS. In O. Grumberg, editor, Proc. 9th International Conference on Computer Aided Verification (CAV'97),volume 1254, pages 72--83. Springer Verlag, 1997.]] Google ScholarDigital Library
- N. Halbwachs, F. Lagnier, and C. Ratel. Programming and verifying real-time systems by means of the synchronous data-flow language LUSTRE. IEEE Trans. Softw. Engin., 18(9):785--793, Sept. 1992.]] Google ScholarDigital Library
- C. Heitmeyer. Software Cost Reduction. In J. J. Marciniak, editor, Encyclopedia of Software Engineering. John Wiley & Sons, Inc., New York, NY, second edition, 2002.]]Google Scholar
- C. Heitmeyer, M. Archer, R. Bharadwaj, R. Jeffords, and J. Kirby, Jr. Tools for tabular specification and analysis of requirements. Technical report, Naval Research Laboratory, Washington, DC, 2003. To appear.]]Google Scholar
- C. Heitmeyer, J. Kirby, B. Labaw, M. Archer, and R. Bharadwaj. Using abstraction and model checking to detect safety violations in requirements specifications. IEEE Trans. on Softw. Eng., 24(11), Nov. 1998.]] Google ScholarDigital Library
- C. Heitmeyer, J. Kirby, Jr., B. Labaw, and R. Bharadwaj. SCR*: A toolset for specifying and analyzing software requirements. In Proc. Computer-Aided Verification, 10th Annual Conf. (CAV'98), Vancouver, Canada, 1998.]] Google ScholarDigital Library
- C. L. Heitmeyer, R.D. Jeffords, and B.G.Labaw. Automated consistency checking of requirements specifications. ACM Transactions on Software Engineering and Methodology, 5(3):231--261, April--June 1996.]] Google ScholarDigital Library
- G. J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279--295, May 1997.]] Google ScholarDigital Library
- R. Jeffords and C. Heitmeyer. Automatic generation of state invariants from requirements specifications. In Proc. Sixth ACM SIGSOFT Symp. on Foundations of Software Engineering, Nov. 1998.]] Google ScholarDigital Library
- R. D. Jeffords and C. L. Heitmeyer. An algorithm for strengthening state invariants generated from requirements specifica-tions. In Proc. of the Fifth IEEE International Symposium on Requirements Engineering, Aug. 2001.]]Google ScholarDigital Library
- J. Kirby, Jr. Example NRL/SCR software requirements for an automobile cruise control and monitoring system. Technical Report TR-87-07, Wang Institute of Graduate Studies, 1987.]]Google Scholar
- J. Kirby, Jr., M. Archer, and C. Heitmeyer. SCR: A practical approach to building a high assurance COMSEC system. In Proceedings of the 15th Annual Computer Security Applications Conference (ACSAC '99). IEEE Computer Society Press, Dec. 1999.]] Google ScholarDigital Library
- Y. Lakhnech, S. Bensalem, S. Berezin, and S. Owre. Incremental verification by abstraction. In T. Margaria and W. Yi, editors, Proc. Tools and Algorithms for Construction and Analysis of Systems (TACAS'01), number 2031 in LNCS, pages 98--112. Springer-Verlag, Apr. 2001.]] Google ScholarDigital Library
- Z. Manna et al. STeP: the Stanford Temporal Prover. Techni-cal Report STAN-CS-TR-94-1518, Stanford Univ., Stanford, CA, June 1994.]] Google ScholarDigital Library
- Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, NY, 1995.]] Google ScholarDigital Library
- K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.]] Google ScholarDigital Library
- K. L. McMillan. Getting Started with SMV: User's Manual. Cadence Berkeley Laboratories, Berkeley, CA, Mar. 1999.]]Google Scholar
- K. L. McMillan. A methodology for hardware verification using compositional model checking. Science of Comput. Prog., 37:279--309, 2000.]] Google ScholarDigital Library
- K. S. Namjoshi and R. J. Trefler. On the completeness of compositional reasoning. In E. A. Emerson and A. P. Sistla, editors, Proc. Computer-Aided Verification (CAV'00), Chicago, IL, July 2000. LNCS 1855, Springer-Verlag.]] Google ScholarDigital Library
- D. L. Parnas and J. Madey. Functional documentation for computer systems. Science of Computer Programming, 25(1):41--61, Oct. 1995.]] Google ScholarDigital Library
- A. Pnueli. In transition from global to modular temporal reasoning about programs. In K. R. Apt, editor, Proc. NATO Adv. Study Inst. on Logics and Models of Concurrent Systems,La Colle-sur-Loup, France, Oct. 1984. Springer-Verlag.]] Google ScholarDigital Library
- J. Ramish. Empirical studies of compositional abstraction. Technical report, Naval Research Laboratory, Washington, DC, 2003. Draft.]]Google Scholar
- H. Saïdi and N. Shankar. Abstract and model check while you prove. In Proc. Computer-Aided Verification (CAV99), Trento,Italy, July 1999.]] Google ScholarDigital Library
- N. Shankar, S. Owre, and J. Rushby. The PVS proof checker: A reference manual. Technical report, Computer Science Lab, SRI Intern., Menlo Park, CA, 1993.]]Google Scholar
- A. J. van Schouwen. The A-7 requirements model: Re-examination for real-time systems and an application for monitoring systems. Technical Report TR 90-276, Queen's Univ., Kingston, ON, Canada, 1990.]]Google Scholar
Index Terms
- A strategy for efficiently verifying requirements
Recommendations
A strategy for efficiently verifying requirements
ESEC/FSE-11: Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineeringThis paper describes a compositional proof strategy for verifying properties of requirements specifications. The proof strategy, which may be applied using either a model checker or a theorem prover, uses known state invariants to prove state and ...
Modeling and Verification of Reactive Systems using Rebeca
Actor-based modeling has been successfully applied to the representation of concurrent and distributed systems. Besides having an appropriate and efficient way for modeling these systems, one needs a formal verification approach for ensuring their ...
Model Checking Complete Requirements Specifications Using Abstraction
Although model checking has proven remarkably effective in detecting errors in hardware designs, its success in the analysis of software specifications has been limited. Model checking algorithms for hardware verification commonly use Binary Decision ...
Comments