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 journalArticle

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

Fingerprint

Requirements Specification
Formal Verification
Cost reduction
Specifications
Software
Costs
Requirements
Formal methods
Specification
Safety Analysis
Safety-critical Systems
Nuclear power plants
Nuclear Power Plant
Formal Methods
Demonstrations
Compliance
Demonstrate
Template
Safety
Real-time

Keywords

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

ASJC Scopus subject areas

  • Mechanical Engineering
  • Safety, Risk, Reliability and Quality

Cite this

Formal verification of functional properties of a SCR-style software requirements specification using PVS. / Kim, Taeho; Stringer-Calvert, David; Cha, Sungdeok.

In: Reliability Engineering and System Safety, Vol. 87, No. 3, 01.03.2005, p. 351-363.

Research output: Contribution to journalArticle

@article{cd731faa6e3d42cfa3cd8236ffaf5983,
title = "Formal verification of functional properties of a SCR-style software requirements specification using PVS",
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.",
keywords = "Formal methods, Formal verification, Nuclear power plant system, Safety-critical system, Software requirements specification, Software safety",
author = "Taeho Kim and David Stringer-Calvert and Sungdeok Cha",
year = "2005",
month = "3",
day = "1",
doi = "10.1016/j.ress.2004.06.005",
language = "English",
volume = "87",
pages = "351--363",
journal = "Reliability Engineering and System Safety",
issn = "0951-8320",
publisher = "Elsevier Limited",
number = "3",

}

TY - JOUR

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

AU - Kim, Taeho

AU - Stringer-Calvert, David

AU - Cha, Sungdeok

PY - 2005/3/1

Y1 - 2005/3/1

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

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

KW - Formal methods

KW - Formal verification

KW - Nuclear power plant system

KW - Safety-critical system

KW - Software requirements specification

KW - Software safety

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

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

U2 - 10.1016/j.ress.2004.06.005

DO - 10.1016/j.ress.2004.06.005

M3 - Article

VL - 87

SP - 351

EP - 363

JO - Reliability Engineering and System Safety

JF - Reliability Engineering and System Safety

SN - 0951-8320

IS - 3

ER -