Using PVS to analyze hierarchical state-based requirements for completeness and consistency

Previously, we have defined procedures for analyzing hierarchical state based requirements specifications for two properties: (1) completeness with respect to a set of criteria related to robustness (a response is specified for every possible input and input sequence) and (2) consistency (the specification is free from conflicting requirements and undesired nondeterminism) (M.P.E. Heimdahl and N.G. Leveson, 1995; 1996). We implemented the analysis procedures in a prototype tool and evaluated their effectiveness and efficiency on a large real world requirements specification expressed in an hierarchical state based language called RSML (Requirements State Machine Language). Although our approach has been largely successful, there are some drawbacks with the current implementation that must be addressed. Our prototype implementation uses Binary Decision Diagrams (BDDs) to perform the analysis. Unfortunately, since BDDs treat predicates and functions as uninterpreted and thus fail to capture their semantics, the use of BDDs can lead to large numbers of spurious (false) error reports. We are currently investigating how the Prototype Verification System (PVS) and its theorem proving component can help us increase the accuracy of our analysis. PVS is a verification system that provides an interactive environment for writing formal specifications and checking formal proofs. The paper discusses the problems with spurious error reports and describes our experiences using the Prototype Verification System to increase the accuracy of our analysis results