A strategy for efficiently verifying requirements
| Autor: | Constance L. Heitmeyer, Ralph D. Jeffords |
|---|---|
| Rok vydání: | 2003 |
| Předmět: |
Model checking
Theoretical computer science Programming language Computer science Proof complexity Software requirements specification General Medicine computer.software_genre Mathematical proof Formal methods Automated theorem proving Simple (abstract algebra) TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS State (computer science) computer |
| Zdroj: | ESEC / SIGSOFT FSE |
| ISSN: | 0163-5948 |
| DOI: | 10.1145/949952.940077 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|