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

Taeho Kim, David Stringer-Calvert, Sungdeok Cha

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)

Abstract

Industrial software companies developing safety-critical systems are required to use rigorous safety analysis techniques to demonstrate compliance to regulatory bodies. While analysis techniques based on manual inspection have been successfully applied to many industrial applications, we demonstrate that inspection has limitations in locating complex errors in software requirements. In this paper, we describe the formal verification of a shutdown system for a nuclear power plant that is currently operational in Korea. The shutdown system is an embedded real-time safety-critical software, and has a description in a Software Cost Reduction (SCR) style specification language. The key component of the work described here is an automatic method for translating SCR-style Software Requirements Specifications (SRS) into the language of the PVS specification and verification system. A further component is the use of property templates to translate natural language Program Functional Specifications (PFS) into PVS, allowing for high-assurance consistency checking between the translated SRS and PFS, thereby verifying the required functional properties.

Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems - 8th Int. Conf., TACAS 2002, Held as Part of the Joint European Conf. on Theory and Practice of Software, ETAPS 2002, Proc.
EditorsJoost-Pieter Katoen, Perdita Stevens
PublisherSpringer Verlag
Pages205-220
Number of pages16
ISBN (Print)3540434194, 9783540434191
DOIs
Publication statusPublished - 2002
Externally publishedYes
Event8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Proceedings - Grenoble, France
Duration: 2002 Apr 82002 Apr 12

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2280 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Proceedings
Country/TerritoryFrance
CityGrenoble
Period02/4/802/4/12

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

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

Cite this