Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Formal Verification of Nonfunctional Requirements of Overall Instrumentation and Control Architectures
Department of Electrical Engineering and Automation, Aalto University, Espoo, Finland.ORCID iD: 0000-0003-3722-2603
VTT Technical Research Centre of Finland Ltd., Espoo, Finland.ORCID iD: 0000-0002-6803-2303
Independent Researcher, Russia.
Independent Researcher, Russia.
Show others and affiliations
2024 (English)In: IEEE Open Journal of the Industrial Electronics Society, E-ISSN 2644-1284, Vol. 5, p. 616-631Article in journal (Refereed) Published
Abstract [en]

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.

Place, publisher, year, edition, pages
IEEE, 2024. Vol. 5, p. 616-631
Keywords [en]
Function block diagrams (FBDs), instrumentation and control (I&C) architecture, logical programming, nonfunctional requirements, ontology, safety-critical systems
National Category
Computer Sciences
Research subject
Dependable Communication and Computation Systems
Identifiers
URN: urn:nbn:se:ltu:diva-108369DOI: 10.1109/OJIES.2024.3413568ISI: 001262725700003Scopus ID: 2-s2.0-85196071885OAI: oai:DiVA.org:ltu-108369DiVA, id: diva2:1885622
Note

Validerad;2024;Nivå 1;2024-07-24 (signyg);

Fulltext license: CC BY-NC-ND

Available from: 2024-07-24 Created: 2024-07-24 Last updated: 2024-07-24Bibliographically approved

Open Access in DiVA

fulltext(2397 kB)73 downloads
File information
File name FULLTEXT01.pdfFile size 2397 kBChecksum SHA-512
2865cac12cfa0c048e6adab24929dd9cc0bf803610f8808688f04a440e70216d9f696bca1acdc7fd342d2552a8e19ea9cf1927b27f898410ec6b94b605c7508f
Type fulltextMimetype application/pdf

Other links

Publisher's full textScopus

Authority records

Vyatkin, Valeriy

Search in DiVA

By author/editor
Ovsiannikova, PolinaPakonen, AnttiDubinin, ViktorVyatkin, Valeriy
By organisation
Computer Science
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 73 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 320 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf