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

Thumbnail Image

Files

isbn9789526414706.pdf (5 MB)

URL

Journal Title

Journal ISSN

Volume Title

School of Electrical Engineering | Doctoral thesis (article-based) | Defence date: 2023-10-27
Unless otherwise stated, all rights belong to the author. You may download, display and print this publication for Your own personal use. Commercial use is prohibited.

Authors

Date

2023

Department

Sähkötekniikan ja automaation laitos
Department of Electrical Engineering and Automation

Major/Subject

Mcode

Degree programme

Language

en

Pages

99 + app. 86

Series

Aalto University publication series DOCTORAL THESES, 166/2023

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.

Description

Supervising professor

Vyatkin, Valeriy, Prof., Aalto University, Department of Electrical Engineering and Automation, Finland

Thesis advisor

Buzhinsky, Igor, Dr., IPRally Technologies Oy, Finland
Chivilikhin, Daniil, Dr., Siemens DISW, Belgium

Keywords

safety-critical systems, cyber-physical systems, model checking, counterexample explanation, FBD, ontology, verification

Other note

Parts

  • [Publication 1]: P. Ovsiannikova, I. Buzhinsky, A. Pakonen, and V. Vyatkin. Oeritte: User-Friendly Counterexample Explanation for Model Checking. IEEEAccess, vol. 9, pp. 61383-61397, 2021.
    Full text in Acris/Aaltodoc: http://urn.fi/URN:NBN:fi:aalto-202105126724
    DOI: 10.1109/ACCESS.2021.3073459 View at publisher
  • [Publication 2]: P. Ovsiannikova, A. Pakonen, D. Muromsky, M. Kobzev, V. Dubinin, and V. Vyatkin. Formal verification of non-functional requirements of overall instrumentation and control architectures. Submitted to IEEE Open Journal of the Industrial Electronics Society, 30 Apr 2023
  • [Publication 3]: P. Ovsiannikova, I. Buzhinsky, A. Pakonen, and V. Vyatkin. Visual Counterexample Explanation for model checking with Oeritte. In 25th International Conference on Engineering of Complex Computer Systems (ICECCS), Singapore, pp. 01-10, October 2020.
    DOI: 10.1109/ICECCS51672.2020.00008 View at publisher
  • [Publication 4]: P. Ovsiannikova and V. Vyatkin. Towards user-friendly model checking of IEC 61499 systems. In IEEE ETFA 2021—26th IEEE International Conference on Emerging Technologies and Factory Automation, Vasteras, Sweden, pp. 01-04, September 2020.
    Full text in Acris/Aaltodoc: http://urn.fi/URN:NBN:fi:aalto-202202021668
    DOI: 10.1109/ETFA45728.2021.9613491 View at publisher
  • [Publication 5]: P. Ovsiannikova, A. Pakonen, and V. Vyatkin. Change-based causes in counterexample explanation for model checking. In IECON 2021—47th Annual Conference of the IEEE Industrial Electronics Society, Toronto, ON, Canada, pp. 1-6, October 2021.
    DOI: 10.1109/IECON48115.2021.9589122 View at publisher
  • [Publication 6]: P. Ovsiannikova, A. Pakonen, and V. Vyatkin. Automatic generation of repair suggestions for overall nuclear I&C architecture represented with an ontology. Accepted for publication in IEEE ETFA 2023—IEEE International Conference on Emerging Technologies and Factory Automation, 3 May 2023
  • [Publication 7]: P. Ovsiannikova, A. Pakonen, and V. Vyatkin. Automatic generation of repair suggestions for control logic of I&C systems. Accepted for publication in IECON 2023—49th Annual Conference of the IEEE Industrial Electronics Society (IES), 30 Apr 2023

Citation

Permanent link to this item

https://urn.fi/URN:ISBN:978-952-64-1470-6

Collections

[diss] Sähkötekniikan korkeakoulu / ELEC