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

The importance of effective requirements analysis techniques cannot be over emphasized when developing software requiring high levels of assurance. Req uirements analysis can be largely classified as either structural or functi onal. 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 suc cessfully applied to many industrial applications, the authors found inspec tion to be ineffective when reviewing requirements to find errors violating structural properties. Moreover, current tools used in requirements engine ering provide only limited support in automatically enforcing structural co rrectness of the requirements. Such experience has motivated research to au tomate straightforward but tedious activities. This paper demonstrates that a theorem prover, PVS (Prototype Verification System), is useful in automatically verifying structural correctness of sof tware requirements specifications written in SCR (Software Cost Reduction)- style. Requirements are automatically translated into a semantically equiva lent PVS specification. Users need not be experts in formal methods or powe r users of PVS. Structural properties to be proved are expressed in PVS the orems, and the PVS proof commands are used to carry out the proof automatic ally. Since these properties are application independent, the same verifica tion procedure can be applied to requirements of various software systems. Copyright (C) 2001 John Wiley & Sons, Ltd.