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

Taeho Kim, Sungdeok Cha

Research output: Contribution to journalArticlepeer-review

7 Citations (Scopus)

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 activitie s. 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.

Original languageEnglish
Pages (from-to)143-163
Number of pages21
JournalSoftware Testing Verification and Reliability
Volume11
Issue number3
DOIs
Publication statusPublished - 2001 Sept
Externally publishedYes

Keywords

  • Formal specification
  • Formal verification
  • Requirements analysis
  • Theorem proving

ASJC Scopus subject areas

  • Software
  • Safety, Risk, Reliability and Quality

Fingerprint

Dive into the research topics of 'Automated structural analysis of SCR-style software requirements specifications using PVS'. Together they form a unique fingerprint.

Cite this