Formal Verification of Nonfunctional Requirements of Overall Instrumentation and Control Architectures
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 a...
Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
IEEE
2024-01-01
|
| Series: | IEEE Open Journal of the Industrial Electronics Society |
| Subjects: | |
| Online Access: | https://ieeexplore.ieee.org/document/10555152/ |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1841526385974181888 |
|---|---|
| author | Polina Ovsiannikova Antti Pakonen Dmitry Muromsky Maksim Kobzev Viktor Dubinin Valeriy Vyatkin |
| author_facet | Polina Ovsiannikova Antti Pakonen Dmitry Muromsky Maksim Kobzev Viktor Dubinin Valeriy Vyatkin |
| author_sort | Polina Ovsiannikova |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-e68d9eaddc47479392ed391638d38f68 |
| institution | Kabale University |
| issn | 2644-1284 |
| language | English |
| publishDate | 2024-01-01 |
| publisher | IEEE |
| record_format | Article |
| series | IEEE Open Journal of the Industrial Electronics Society |
| spelling | doaj-art-e68d9eaddc47479392ed391638d38f682025-01-17T00:01:22ZengIEEEIEEE Open Journal of the Industrial Electronics Society2644-12842024-01-01561663110.1109/OJIES.2024.341356810555152Formal Verification of Nonfunctional Requirements of Overall Instrumentation and Control ArchitecturesPolina Ovsiannikova0https://orcid.org/0000-0003-3722-2603Antti Pakonen1https://orcid.org/0000-0002-6803-2303Dmitry Muromsky2Maksim Kobzev3Viktor Dubinin4https://orcid.org/0000-0002-5761-2249Valeriy Vyatkin5https://orcid.org/0000-0002-9315-9920Department of Electrical Engineering and Automation, Aalto University, Espoo, FinlandVTT Technical Research Centre of Finland Ltd., Espoo, FinlandIndependent Researcher, RussiaIndependent Researcher, RussiaIndependent Researcher, RussiaDepartment of Electrical Engineering and Automation, Aalto University, Espoo, FinlandThe 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.https://ieeexplore.ieee.org/document/10555152/Function block diagrams (FBDs)instrumentation and control (I&C) architecturelogical programmingnonfunctional requirementsontologysafety-critical systems |
| spellingShingle | Polina Ovsiannikova Antti Pakonen Dmitry Muromsky Maksim Kobzev Viktor Dubinin Valeriy Vyatkin Formal Verification of Nonfunctional Requirements of Overall Instrumentation and Control Architectures IEEE Open Journal of the Industrial Electronics Society Function block diagrams (FBDs) instrumentation and control (I&C) architecture logical programming nonfunctional requirements ontology safety-critical systems |
| title | Formal Verification of Nonfunctional Requirements of Overall Instrumentation and Control Architectures |
| title_full | Formal Verification of Nonfunctional Requirements of Overall Instrumentation and Control Architectures |
| title_fullStr | Formal Verification of Nonfunctional Requirements of Overall Instrumentation and Control Architectures |
| title_full_unstemmed | Formal Verification of Nonfunctional Requirements of Overall Instrumentation and Control Architectures |
| title_short | Formal Verification of Nonfunctional Requirements of Overall Instrumentation and Control Architectures |
| title_sort | formal verification of nonfunctional requirements of overall instrumentation and control architectures |
| topic | Function block diagrams (FBDs) instrumentation and control (I&C) architecture logical programming nonfunctional requirements ontology safety-critical systems |
| url | https://ieeexplore.ieee.org/document/10555152/ |
| work_keys_str_mv | AT polinaovsiannikova formalverificationofnonfunctionalrequirementsofoverallinstrumentationandcontrolarchitectures AT anttipakonen formalverificationofnonfunctionalrequirementsofoverallinstrumentationandcontrolarchitectures AT dmitrymuromsky formalverificationofnonfunctionalrequirementsofoverallinstrumentationandcontrolarchitectures AT maksimkobzev formalverificationofnonfunctionalrequirementsofoverallinstrumentationandcontrolarchitectures AT viktordubinin formalverificationofnonfunctionalrequirementsofoverallinstrumentationandcontrolarchitectures AT valeriyvyatkin formalverificationofnonfunctionalrequirementsofoverallinstrumentationandcontrolarchitectures |