NuEditor - A Tool Suite for Specification and Verification of NuSCR

摘要

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.