Sciweavers

SIGSOFT
2003
ACM

A strategy for efficiently verifying requirements

14 years 4 months ago
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...
Ralph D. Jeffords, Constance L. Heitmeyer
Added 20 Nov 2009
Updated 20 Nov 2009
Type Conference
Year 2003
Where SIGSOFT
Authors Ralph D. Jeffords, Constance L. Heitmeyer
Comments (0)