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 publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages205-220
Number of pages16
Volume2280 LNCS
Publication statusPublished - 2002 Dec 1
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)03029743
ISSN (Electronic)16113349

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
CountryFrance
CityGrenoble
Period02/4/802/4/12

Fingerprint

Requirements Specification
Formal Verification
Cost reduction
Specifications
Software
Costs
Plant shutdowns
Inspection
Specification
Specification languages
Nuclear power plants
Safety Analysis
Industrial applications
Safety-critical Systems
Nuclear Power Plant
Specification Languages
Industrial Application
Style
Formal verification
Compliance

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Kim, T., Stringer-Calvert, D., & Cha, S. (2002). Formal verification of functional properties of an SCR-style software requirements specification using PVS. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2280 LNCS, pp. 205-220). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2280 LNCS).

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

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 2280 LNCS 2002. p. 205-220 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2280 LNCS).

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

Kim, T, Stringer-Calvert, D & Cha, S 2002, Formal verification of functional properties of an SCR-style software requirements specification using PVS. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 2280 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 2280 LNCS, pp. 205-220, 8th 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, 02/4/8.
Kim T, Stringer-Calvert D, Cha S. Formal verification of functional properties of an SCR-style software requirements specification using PVS. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 2280 LNCS. 2002. p. 205-220. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Kim, Taeho ; Stringer-Calvert, David ; Cha, Sungdeok. / Formal verification of functional properties of an SCR-style software requirements specification using PVS. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 2280 LNCS 2002. pp. 205-220 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{80d79aeb518c4aa99df68a581a801f1c,
title = "Formal verification of functional properties of an 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. 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.",
author = "Taeho Kim and David Stringer-Calvert and Sungdeok Cha",
year = "2002",
month = "12",
day = "1",
language = "English",
isbn = "3540434194",
volume = "2280 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "205--220",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - GEN

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

AU - Kim, Taeho

AU - Stringer-Calvert, David

AU - Cha, Sungdeok

PY - 2002/12/1

Y1 - 2002/12/1

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

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

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

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

M3 - Conference contribution

AN - SCOPUS:57049097738

SN - 3540434194

SN - 9783540434191

VL - 2280 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 205

EP - 220

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

ER -