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
N1 - Copyright:
Copyright 2020 Elsevier B.V., All rights reserved.
PY - 2002
Y1 - 2002
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
U2 - 10.1007/3-540-46002-0_15
DO - 10.1007/3-540-46002-0_15
M3 - Conference contribution
AN - SCOPUS:57049097738
SN - 3540434194
SN - 9783540434191
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 205
EP - 220
BT - Tools 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.
A2 - Katoen, Joost-Pieter
A2 - Stevens, Perdita
PB - Springer Verlag
T2 - 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
Y2 - 8 April 2002 through 12 April 2002
ER -