A strategy for efficiently verifying requirements

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 realworld Navy system, are presented. In the Navy example, compositional verification using either theorem proving or model checking was three times faster than verification based on the standard incremental (nonc...

• Type: Conference
• Year: 2003
• Where: SIGSOFT
• Authors: Ralph D. Jeffords, Constance L. Heitmeyer
• Keywords: Compositional Proof Rule, Compositional Proof Strategy, Incremental Proof Rule, SIGSOFT 2003, Software Engineering