NuEditor - A tool suite for specification and verification of NuSCR

Jaemyung Cho, Junbeom Yoo, Sungdeok Cha

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

4 Citations (Scopus)

Abstract

NuEditor is a tool suite supporting specification and verification of software requirements written in NuSCR, NuSCR extends SCR (Software Cost Reduction) notation that has been used in specifying requirements for embedded safety-critical systems such as a shutdown system for nuclear power plant. SCR almost exclusively depended on fine-grained tabular notations to represent not only computation-intensive functions but also time- or state-dependent operations. As a consequence, requirements became excessively complex and difficult to understand. NuSCR supports intuitive and concise notations. For example, automata is used to capture time or state-dependent operations, and concise tabular notations are made possible by allowing complex but proven-correct equations be used without having to decompose them into a sequence of primitive operations. NuEditor provides graphical editing environment and supports static analysis to detect errors such as missing or conflicting requirements. To provide high-assurance safety analysis, NuEditor can automatically translate NuSCR specification into SMV input so that satisfaction of certain properties can be automatically determined based on exhaustive examination of all possible behavior. NuEditor has been programmed to generate requirements as an XML document so that other verification tools such as PVS can also be used if needed. We have used NuEditor to specify a trip logic of RPS (Reactor Protection System) BP(Bistable Processor) and verify its correctness. It is a part of software-implemented nuclear power plant shutdown system. Domain experts found NuSCR and NuEditor to be useful and qualified for industrial use in nuclear engineering.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages19-28
Number of pages10
Volume3647 LNCS
Publication statusPublished - 2005 Dec 1
Externally publishedYes
Event2nd International Conference on Software Engineering Research and Applications, SERA 2004 - Los Angeles, CA, United States
Duration: 2004 May 52004 May 7

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3647 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other2nd International Conference on Software Engineering Research and Applications, SERA 2004
CountryUnited States
CityLos Angeles, CA
Period04/5/504/5/7

    Fingerprint

ASJC Scopus subject areas

  • Biochemistry, Genetics and Molecular Biology(all)
  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Cho, J., Yoo, J., & Cha, S. (2005). NuEditor - A tool suite for specification and verification of NuSCR. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3647 LNCS, pp. 19-28). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3647 LNCS).