Automated structural analysis of SCR-style software requirements specifications using PVS

Abstract

The importance of effective requirements analysis techniques cannot be overemphasized when developing software requiring high levels of assurance. Requirements analysis can be largely classified as either structural or functional. The former investigates whether definitions and uses of variables and functions are consistent, while the latter addresses whether requirements accurately reflect users' needs. Verification of structural properties for large and complex software requirements is often repetitive, especially if requirements are subject to frequent changes. While inspection has been successfully applied to many industrial applications, the authors found inspection to be ineffective when reviewing requirements to find errors violating structural properties. Moreover, current tools used in requirements engineering provide only limited support in automatically enforcing structural correctness of the requirements. Such experience has motivated research to automate straightforward but tedious activities. This paper demonstrates that a theorem prover, PVS (Prototype Verification System), is useful in automatically verifying structural correctness of software requirements specifications written in SCR (Software Cost Reduction)-style. Requirements are automatically translated into a semantically equivalent PVS specification. Users need not be experts in formal methods or power users of PVS. Structural properties to be proved are expressed in PVS theorems, and the PVS proof commands are used to carry out the proof automatically. Since these properties are application independent, the same verification procedure can be applied to requirements of various software systems. Copyright (C) 2001 John Wiley & Sons, Ltd.