Formal verification of functional properties of a SCR-style software requirements specification using PVS

Taeho Kim, David Stringer-Calvert, Sungdeok Cha

Research output: Contribution to journalArticlepeer-review

4 Citations (Scopus)

Abstract

Industrial software companies developing safety-critical systems are required to use rigorous safety analysis techniques to demonstrate compliance to regulatory bodies. In this paper, we describe an approach to formal verification of functional properties of requirements for an embedded real-time software written in software cost reduction (SCR)-style language using PVS specification and verification system. Key contributions of the paper include development of an automated method of translating SCR-style requirements into PVS input language as well as identification of property templates often needed in verification. Using specification for a nuclear power plant system, currently in operation, we demonstrate how safety demonstration on requirements can be accomplished while taking advantage of assurance provided by formal methods.

Original languageEnglish
Pages (from-to)351-363
Number of pages13
JournalReliability Engineering and System Safety
Volume87
Issue number3
DOIs
Publication statusPublished - 2005 Mar
Externally publishedYes

Bibliographical note

Funding Information:
This work was partially supported by the Korea Science and Engineering Foundation through the Advanced Information Technology Research Center and by the National Science Foundation under grants CCR-00-82560 and CCR-00-86096.

Keywords

  • Formal methods
  • Formal verification
  • Nuclear power plant system
  • Safety-critical system
  • Software requirements specification
  • Software safety

ASJC Scopus subject areas

  • Safety, Risk, Reliability and Quality
  • Industrial and Manufacturing Engineering

Fingerprint

Dive into the research topics of 'Formal verification of functional properties of a SCR-style software requirements specification using PVS'. Together they form a unique fingerprint.

Cite this