Formal verification of non-functional requirements of overall instrumentation and control architectures
Loading...
Access rights
openAccess
URL
Journal Title
Journal ISSN
Volume Title
A1 Alkuperäisartikkeli tieteellisessä aikakauslehdessä
This publication is imported from Aalto University research portal.
View publication in the Research portal (opens in new window)
View/Open full text file from the Research portal (opens in new window)
Other link related to publication (opens in new window)
View publication in the Research portal (opens in new window)
View/Open full text file from the Research portal (opens in new window)
Other link related to publication (opens in new window)
Date
2024
Major/Subject
Mcode
Degree programme
Language
en
Pages
16
Series
IEEE Open Journal of the Industrial Electronics Society, Volume 5, pp. 616-631
Abstract
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.Description
Publisher Copyright: Authors
Keywords
Computer architecture, Formal verification, Function block diagrams, I&C architecture, Industrial electronics, Instruments, Ontologies, Power generation, Safety, logical programming, non-functional requirements, ontology, safety-critical systems, nonfunctional requirements, Function block diagrams (FBDs), instrumentation and control (I&C) architecture
Other note
Citation
Ovsiannikova, P, Pakonen, A, Muromsky, D, Kobzev, M, Dubinin, V & Vyatkin, V 2024, ' Formal verification of non-functional requirements of overall instrumentation and control architectures ', IEEE Open Journal of the Industrial Electronics Society, vol. 5, pp. 616-631 . https://doi.org/10.1109/OJIES.2024.3413568