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

Taeho Kim, Sungdeok Cha

Research output: Contribution to journalArticle

6 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 Sep 1
Externally publishedYes

Fingerprint

Cost reduction
Structural analysis
Specifications
Structural properties
Inspection
Requirements engineering
Formal methods
Industrial applications

Keywords

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

ASJC Scopus subject areas

  • Computer Graphics and Computer-Aided Design
  • Software

Cite this

Automated structural analysis of SCR-style software requirements specifications using PVS. / Kim, Taeho; Cha, Sungdeok.

In: Software Testing Verification and Reliability, Vol. 11, No. 3, 01.09.2001, p. 143-163.

Research output: Contribution to journalArticle

@article{c445ec9360ee496186748216d733e708,
title = "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 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.",
keywords = "Formal specification, Formal verification, Requirements analysis, Theorem proving",
author = "Taeho Kim and Sungdeok Cha",
year = "2001",
month = "9",
day = "1",
doi = "10.1002/stvr.218",
language = "English",
volume = "11",
pages = "143--163",
journal = "Software Testing Verification and Reliability",
issn = "0960-0833",
publisher = "John Wiley and Sons Ltd",
number = "3",

}

TY - JOUR

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

AU - Kim, Taeho

AU - Cha, Sungdeok

PY - 2001/9/1

Y1 - 2001/9/1

N2 - 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.

AB - 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.

KW - Formal specification

KW - Formal verification

KW - Requirements analysis

KW - Theorem proving

UR - http://www.scopus.com/inward/record.url?scp=0035447825&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0035447825&partnerID=8YFLogxK

U2 - 10.1002/stvr.218

DO - 10.1002/stvr.218

M3 - Article

AN - SCOPUS:0035447825

VL - 11

SP - 143

EP - 163

JO - Software Testing Verification and Reliability

JF - Software Testing Verification and Reliability

SN - 0960-0833

IS - 3

ER -