DC Field | Value | Language |
---|---|---|
dc.contributor.author | Kim, T | ko |
dc.contributor.author | Stringer-Calvert, D | ko |
dc.contributor.author | Cha, Sungdeok | ko |
dc.date.accessioned | 2013-03-06T18:09:20Z | - |
dc.date.available | 2013-03-06T18:09:20Z | - |
dc.date.created | 2012-02-06 | - |
dc.date.created | 2012-02-06 | - |
dc.date.issued | 2005-03 | - |
dc.identifier.citation | RELIABILITY ENGINEERING & SYSTEM SAFETY, v.87, no.3, pp.351 - 363 | - |
dc.identifier.issn | 0951-8320 | - |
dc.identifier.uri | http://hdl.handle.net/10203/87897 | - |
dc.description.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. (C) 2004 Elsevier Ltd. All rights reserved. | - |
dc.language | English | - |
dc.publisher | ELSEVIER SCI LTD | - |
dc.subject | SAFETY-CRITICAL SOFTWARE | - |
dc.subject | PROTECTION SYSTEM APPLICATION | - |
dc.subject | COMBINED CPN | - |
dc.title | Formal verification of functional properties of a SCR-style software requirements specification using PVS | - |
dc.type | Article | - |
dc.identifier.wosid | 000226311400006 | - |
dc.identifier.scopusid | 2-s2.0-9444259226 | - |
dc.type.rims | ART | - |
dc.citation.volume | 87 | - |
dc.citation.issue | 3 | - |
dc.citation.beginningpage | 351 | - |
dc.citation.endingpage | 363 | - |
dc.citation.publicationname | RELIABILITY ENGINEERING & SYSTEM SAFETY | - |
dc.identifier.doi | 10.1016/j.ress.2004.06.005 | - |
dc.contributor.nonIdAuthor | Kim, T | - |
dc.contributor.nonIdAuthor | Stringer-Calvert, D | - |
dc.type.journalArticle | Article | - |
dc.subject.keywordAuthor | safety-critical system | - |
dc.subject.keywordAuthor | software safety | - |
dc.subject.keywordAuthor | software requirements specification formal methods | - |
dc.subject.keywordAuthor | formal verification | - |
dc.subject.keywordAuthor | nuclear power plant system | - |
dc.subject.keywordPlus | SAFETY-CRITICAL SOFTWARE | - |
dc.subject.keywordPlus | PROTECTION SYSTEM APPLICATION | - |
dc.subject.keywordPlus | COMBINED CPN | - |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.