Formal Verification of Nonfunctional Requirements of Overall Instrumentation and Control Architectures

Autor: Polina Ovsiannikova, Antti Pakonen, Dmitry Muromsky, Maksim Kobzev, Viktor Dubinin, Valeriy Vyatkin
Jazyk: angličtina
Rok vydání: 2024
Předmět:
Zdroj: IEEE Open Journal of the Industrial Electronics Society, Vol 5, Pp 616-631 (2024)
Druh dokumentu: article
ISSN: 2644-1284
DOI: 10.1109/OJIES.2024.3413568
Popis: The design of safety-critical cyber–physical systems requires a rigorous check of their operation logic, as well as an analysis of their overall instrumentation and control (I&C) architectures. In this article, we focus on the latter and use formal verification methods to reason about the correctness of an I&C architecture represented with an ontology, using the example of a nuclear power plant design. A safe nuclear power plant must comply with the defense-in-depth principle, which introduces constraints on the physical and functional components of the I&C systems it consists of. This work presents a method for designing nonfunctional requirements using function block diagrams, its definition using logical programming, and demonstrates its implementation in a graphical tool, FBQL. The tool takes as input an ontology representing the I&C architecture to be checked and allows visual design of complex nonfunctional requirements as well as explanation of the results of the checks.
Databáze: Directory of Open Access Journals