Development of a safety critical software requirements verification method with combined CPN and PVS: a nuclear power plant protection system application

Safety-critical software systems such as certain nuclear instrumentation and control (NI&C) systems should be developed with thorough verification. This study presents a method of software requirement verification with a case study for a nuclear power plant (NPP) protection system. The verification introduces colored petri net (CPN) for system modeling and prototype verification system (PVS) for mathematical verification. In order to aid flow-through from modeling by CPN to mathematical proof by PVS, an information extractor from CPN models has been developed in this paper. In order to convert the extracted information to the PVS specification language, a translator has also been developed. This combined method has been applied to the functional requirements of the Wolsong NPP Shut Down System #2 (SDS2); logical properties of the requirements were verified. Through this research, guidelines and a tool support for the use of formal methods have been developed for application to NI&C software verification.     

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

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.     

An effective technique for the software requirements analysis of NPP safety-critical systems, based on software inspection, requirements traceability, and formal specification

A thorough requirements analysis is indispensable for developing and implementing safety-critical software systems such as nuclear power plant (NPP) software systems because a single error in the requirements can generate serious software faults. However, it is very difficult to completely analyze system requirements. In this paper, an effective technique for the software requirements analysis is suggested. For requirements verification and validation (V&V) tasks, our technique uses software inspection, requirement traceability, and formal specification with structural decomposition. Software inspection and requirements traceability analysis are widely considered the most effective software V&V methods. Although formal methods are also considered an effective V&V activity, they are difficult to use properly in the nuclear fields as well as in other fields because of their mathematical nature. In this work, we propose an integrated environment (IE) approach for requirements, which is an integrated approach that enables easy inspection by combining requirement traceability and effective use of a formal method. The paper also introduces computer-aided tools for supporting IE approach for requirements. Called the nuclear software inspection support and requirements traceability (NuSISRT), the tool incorporates software inspection, requirement traceability, and formal specification capabilities. We designed the NuSISRT to partially automate software inspection and analysis of requirement traceability. In addition, for the formal specification and analysis, we used the formal requirements specification and analysis tool for nuclear engineering (NuSRS).     

Synthesis of FBD-based PLC design from NuSCR formal specification

NuSCR is a formal specification language to document requirements for real-time embedded software with nuclear engineering applications in mind. Domain experts actively participated in selecting how to best represent various aspects. It uses tabular notations to specify required computations and automata to document state- or time-dependent behavior. As programmable logic controllers (PLCs) are widely used to implement real-time embedded software, synthesis of PLC code from a formal specification is desirable if transformation rules can be rigorously defined. In addition to improved productivity, results of safety analysis performed on requirements remain valid. In this paper, we demonstrate how NuSCR specification can be translated into semantically equivalent function block diagram (FBD) code. The process, except the initial phase where user provides information on missing or implicit details, is automated. Since executable code can be automatically generated using CASE tools from FBD, much of software development is automated. Proposed technique is currently being used in developing reactor protection system (RPS) for nuclear power plants in Korea, and experience to date has been positive. We demonstrate the proposed approach using the fixed set-point rising trip which is one of the most complex trip logics included in the RPS.     

An approach to the implementation and verification of abstract data

Abstract

The concept of abstraction can be used to simplify and formalize the design of software. However, most of the existing techniques based on abstraction only consider the control structure but not the data structures in the software. The transformation of a data abstraction, i.e., an abstract data type, to a physical data structure is a complicated process. It is composed of three major parts: a specification technique for describing a data abstraction; a deriving process for deriving the representation of the abstraction based on the specification; and a verification method for verifying the correctness of the specification and the representation of the abstraction. In this paper, we will concentrate on the last two problems, and it is assumed that the algebraic specification technique is used for describing abstract data types. Also, we will use examples to illustrate the use of the proposed approach.     

PERTS: an environment for specification and verification of reactive systems

In this paper, we describe the design and implementation of an environment for specification, analysis and verification of reactive systems. The environment allows the user to develop specification in the graphical formalism of Statecharts and analyze them using a simulation tool. A built-in translator tool translates the specification into an Esterel program for the purpose of carrying out verification. Through such an approach, we have been able to integrate the powerful graphical formalism of Statecharts, which is very appealing to engineers, and the power of the formal verification environment of Esterel. Since we translate Statecharts, which can be non-deterministic, to Esterel programs, which are fully deterministic, the system overcomes the non-determinism in the specifications by enforcing priority. The behavior of Esterel programs generated by the translator follow Harel and Naamad's ‘step’ semantics. In the paper, we describe the main components of the PERTS environment and the principles underlying the translation and illustrate the use of the system for specification and verification using an example.     

Quantitative demonstration and cost considerations of a software fault removal methodology

This paper presents a demonstration of a methodology for fault removal during software development. The methodology encompasses the entire development history, from system and software requirements generation to system test. Thus it considers not only the faults during software testing after formal configuration controls have been invoked, but also the faults discovered prior to that phase: during system and software requirements generation, preliminary design, detailed design and code and unit testing. The agents for fault discovery used in verification and validation are called activities, techniques and tools (AT & Ts) in this paper, each having a certain maximum potential or capability for fault discovery. The AT & Ts considered include the usual specification review activities, and also certain tools not normally applied in ‘standard’ software development, such as automated requirements aids. Application of the methodology yields numbers of residual faults as of each phase of development, including those remaining to be discovered during operations and maintenance. Some previous experience and data on residual faults correspond to these results, indicating that the methodology and choice of parameters are reasonable. The methodology also allows one to calculate a relative loss due to delay in fault discovery, which, as is well known, rises rapidly when faults are not discovered during the phase in which they are generated.     

A heuristic-based approach to conceptual design

In the inherently large space of design, explicating all possible concept variants—to avoid leaving out potential concepts—is astronomically costly, if at all possible. A strategy that can assist designers in exploring and ascertaining design solutions within this vast space is therefore crucial. This work adapts a general best first heuristic algorithm for applications on conceptual design problems. The algorithm is tailored to operate on a model of conceptual design postulated in this paper. The propositions are established by an ordered series of formal definitions and mathematical assertions, which characterizes the complete theoretical model. Via a simple design case study, this product conceptualization approach is demonstrated to strategically guide designers in the exploration of design concepts.     

An introduction to compositional methods for concurrency and their application to real-time

Formal methods to specify and verify concurrent programs with synchronous message passing are discussed. We stress the development towards compositional methods, i.e. methods in which the specification of a compound program can be inferred from specifications of its constituents without reference to the internal structure of those parts. Compositionality enables verification during the process of (top-down) design — the derivation of correct programs — instead of the more familiar a-posteriori verification based on already completed program codes. We sketch the transition from non-compositional towards compositional methods for concurrent programs, indicating the main principles behind compositionality. Having achieved a compositional framework based on classical Hoare triples, we discuss extensions to achieve a convenient formalism to specify and verify reactive systems that have an intensive interaction with their environment. Next this Hoare-style framework is adapted to specify and verify real-time properties, and a compositional proof method is formulated for real-time distributed computing. Compositional reasoning during top-down development of a real-time program is illustrated by an example concerning a watchdog timer. This work was partially supported by Esprit-bra project 3096: Formal Methods and Tools for the Development of Distributed and Real-Time Systems (spec).     

Runtime verification and monitoring of embedded systems

Ensuring the correctness of software applications is a difficult task. The area of runtime verification, which combines the approaches of formal verification and testing, offers a practical but limited solution that can help in finding many errors in software. Runtime verification relies upon tools for monitoring software execution. There are particular difficulties with regard to monitoring embedded systems. The concerns for arranging non-intrusive monitoring of embedded systems in a way that is suitable for use in runtime verification methods are considered here. A number of existing runtime verification tools are referenced, highlighting their requirement for monitoring solutions. Established and emerging approaches for the monitoring of software execution using execution monitors are reviewed, with an emphasis on the approaches that are best suited for use with embedded systems. A suggested solution for non-intrusive monitoring of embedded systems is presented. The conclusions summarise the possibilities for arranging non-intrusive monitoring of embedded systems, and the potential for runtime verification to utilise such monitoring approaches.     

Operating system verification—An overview

This paper gives a high-level introduction to the topic of formal, interactive, machine-checked software verification in general, and the verification of operating systems code in particular. We survey the state of the art, the advantages and limitations of machine-checked code proofs, and describe two specific ongoing larger-scale verification projects in more detail. NICTA is funded by the Australian Government as represented by the Department of Broadband, Communications and the Digital Economy and the Australian Research Council.     

A Co-Verification Interface Design for High-Assurance CPS

Cyber-Physical Systems (CPS) tightly integrate cyber and physical components and transcend traditional control systems and embedded system. Such systems are often mission-critical; therefore, they must be high-assurance. High-assurance CPS require co-verification which takes a comprehensive view of the whole system to verify the correctness of a cyber and physical components together. Lack of strict multiple semantic definition for interaction between the two domains has been considered as an obstacle to the CPS co-verification. A Cyber/Physical interface model for hierarchical a verification of CPS is proposed. First, we studied the interaction mechanism between computation and physical processes. We further classify the interaction mechanism into two levels: logic interaction level and physical interaction level. We define different types of interface model according to combinatorial relationships of the A/D (Analog to Digital) and D/A (Digital to Analog) conversion periodical instants. This interface model has formal semantics, and is efficient for simulation and formal verification. The experiment results show that our approach has major potential in verifying system level properties of complex CPS, therefore improving the high-assurance of CPS.     

Safety analysis of the height control system for the Elbtunnel

A new tunnel tube crossing the river Elbe has been built in Hamburg until the end of 2002. Therefore, a new height control system was required. A computer examines the signals from light barriers and overhead sensors to detect vehicles, which try to drive into a tube with insufficient height. If necessary, it raises an alarm that blocks the road. This paper describes the application of two safety analysis techniques on this embedded system: model checking has been used to prove functional correctness with respect to a formal model. Fault tree analysis has validated the model and considered technical defects. Their combination uncovered a safety flaw, led to a precise requirement specification for the software, and showed various ways to improve system safety.     

探索便携式坐标测量类设备软件验证方法

一般检定规程或校准规范只是对探索便携式坐标测量类仪器的综合误差或硬件指标进行检定、校准,而没有对其软件功能和算法的正确性进行验证和确认。本文依据实际工作中的管控要求,对软件验证和确认的重要性、难点进行分析,提出了一种简便、易于操作,适用于企业内部计量测试机构使用的基于算法比较和设备比较的软件验证方法,并通过激光跟踪仪软件验证实例,具体描述了验证过程和验证结果。     

Safety and Reliability Estimation of Automatic Train Protection and Block System

Considering the high maintenance costs of trackside equipment and its vulnerability to natural disasters, a novel railway system named Automatic Train Protection and Block (ATPB) is proposed by the authors to aid in improving the efficiency and reducing the cost of regional train lines. It is a railway radio system based on onboard equipment. In order to ensure its system safety, the paper gives a formal analysis on the functional requirements specification for the system. Specifically, after analyzing the actual requirements, a UML model of the ATPB system is created first to check the functional completeness and structural reasonability. Second, a formal and unambiguous specification of the ATPB system is established by VDM++, i.e. VDM++ model, based on the UML class diagram. Third, the internal consistency and satisfiability of the formal specification is verified and validated. Finally, a simulation is conducted strictly according to the formal specification. Without any runtime errors, collisions or derailments, the results demonstrate the high quality of the simulation and the safety of the specification. Copyright © 2013 John Wiley & Sons, Ltd.     

A re-entrant line model for software product testing

In today’s competitive environment for software products, quality is an important characteristic. The development of large-scale software products is a complex and expensive process. Testing plays a very important role in ensuring product quality. Improving the software development process leads to improved product quality. We propose a queueing model based on re-entrant lines to depict the process of software modules undergoing testing/debugging, inspections and code reviews, verification and validation, and quality assurance tests before being accepted for use. Using the re-entrant line model for software testing, bounds on test times are obtained by considering the state transitions for a general class of modules and solving a linear programming model. Scheduling of software modules for tests at each process step yields the constraints for the linear program. The methodology presented is applied to the development of a software system and bounds on test times are obtained. These bounds are used to allocate time for the testing phase of the project and to estimate the release times of software.     

Formal verification of negotiation protocols for multi-agent manufacturing systems

Formal verification is an important means of tackling behavioural problems such as deadlocks in multi-agent systems. This paper is concerned with the role played by formal verification in the simulation-based performance analysis of multi-agent manufacturing systems. A discrete-event simulation case study is presented to show how varying certain timing parameters of the agent negotiation protocol affects the performance of a multi-agent manufacturing system as well as the chance of getting deadlocks among the software agents. When one tries to determine the optimal values of these timing parameters based on the simulation results, formal verification can help refine the results by confirming whether deadlocks among software agents are indeed possible for particular parameter values. This involves modelling the system's real-time behaviour according to the simulation model and applying the techniques and tools of model checking.     

Requirements modelling and formal analysis using graph operations

The increasing complexity of enterprise systems requires a more advanced analysis of the representation of services expected than is currently possible. Consequently, the specification stage, which could be facilitated by formal verification, becomes very important to the system life-cycle. This paper presents a formal modelling approach, which may be used in order to better represent the reality of the system and to verify the awaited or existing system's properties, taking into account the environmental characteristics. For that, we firstly propose a formalization process based upon properties specification, and secondly we use Conceptual Graphs operations to develop reasoning mechanisms of verifying requirements statements. The graphic visualization of these reasoning enables us to correctly capture the system specifications by making it easier to determine if desired properties hold. It is applied to the field of Enterprise modelling.     

New system of standard exergies of chemical elements. I. Standard exergies of ionogen elements

A system of standard exergies of chemical elements and individual substances is proposed that is based on the choice of the aqueous phase of the World Ocean — “sea water” — as an environmental niche and the choice of simple (one-element) cations and anions existing in it — with account for their concentrations — as reference substances for their constituting ionogen elements. Standard exergies of ionogen elements are calculated. Translated from Inzhenerno-Fizicheskii Zhurnal, Vol. 71, No. 3, pp. 516–520, May–June, 1998.