Methods and tools aiding in the analysis of specification failures during the design process of safety-critical cyber-physical systems

Abstract

The current thesis presents methods and tools for user-friendly analysis of functional and non-functional requirements failures of safety-critical systems, exemplified by nuclear power plants (NPPs) Instrumentation and control (I&C) systems. The domain is characterized by the limited tool support of the engineers during the design phase when the control logic and overall architecture are decided upon.

In this work, we deal with two aspects of the design process of safety-critical I&C systems which are related to checking whether the system under development satisfies its requirements. First, we consider functional requirements, which are properties of control programs that are verified using model checking.

Here, the main contribution is the method and the tool, Oeritte, for the graphical explanation of the results of such checks, counterexamples, having control systems implemented as function block diagrams (FBD).

This part is followed by addressing the non-functional requirements of safety-critical I&;C systems using an ontological model of an overall I&C architecture. We heavily use the context of NPP, where one subset of non-functional requirements is derived from the design principles such as defense-in-depth. Such requirements, for instance, include physical separation, diversity, communication independence, and fault tolerance of I&C systems in the overall I&C architecture. In the thesis, we propose the method and tool for designing such complex requirements using FBDs with service blocks connected to the knowledge base.

Finally, this work addresses the task of proposing fixes to the issues found after checking both types of properties. In case of failures of the functional specification, fixes take the form of adjustments to an FBD that represents the control program of an I&C system. The fixes are composed of add/remove operations over function blocks and connections in the diagram. Then, we propose to fix overall design failures by introducing changes to the design facts stored in the ontology describing an overall I&C architecture. We do not change the structure of the ontology here, but we work solely with the design facts stored in an RDF form.