Functionally-Equivalent Formalization and Automated Model Checking of Function Block Diagrams
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F49777513%3A23520%2F25%3A43976488" target="_blank" >RIV/49777513:23520/25:43976488 - isvavai.cz</a>
Result on the web
<a href="https://doi.org/10.1109/ACCESS.2025.3535890" target="_blank" >https://doi.org/10.1109/ACCESS.2025.3535890</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1109/ACCESS.2025.3535890" target="_blank" >10.1109/ACCESS.2025.3535890</a>
Alternative languages
Result language
angličtina
Original language name
Functionally-Equivalent Formalization and Automated Model Checking of Function Block Diagrams
Original language description
In the development and verification of safety-critical and safety-related Instrumentation and Control (I&C) systems, it is essential to ensure there is no deviation from the requirements of the assignment during development. Model checking is a method of formal verification which can be used to prove whether a formal model satisfies its formal requirement. Since algorithms of I&C systems are generally informal, they can not be verified by model checking directly, but they must be carefully translated. This article presents a new method based on functionally-equivalent formalisation and model checking. This method can be used for automatic verification of I&C algorithms by model checking while preserving obtained proofs from a formalised model in the original algorithm. There are several problems associated with the verification of PLCs by model checking: 1) State space explosion, 2) Model consistency, 3) Specifying Properties to be Checked, 4) Representing PLC execution cycle, 5) TONs timers representation. This aims of this article is to address points 1), 2), 4) and 5). The article also presents conditions for implementing these algorithms in a target I&C system under which the obtained proofs can also be expected in the physical I&C system. This article primarily focuses on formalisation and model checking of Function Block Diagram (FBD) algorithms. However, the presented methods can also be extended to other programming languages.
Czech name
—
Czech description
—
Classification
Type
J<sub>imp</sub> - Article in a specialist periodical, which is included in the Web of Science database
CEP classification
—
OECD FORD branch
20205 - Automation and control systems
Result continuities
Project
<a href="/en/project/9A22007" target="_blank" >9A22007: Optimization of Electric Vehicle Autonomy</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2025
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
IEEE Access
ISSN
2169-3536
e-ISSN
2169-3536
Volume of the periodical
13
Issue of the periodical within the volume
29 January 2025
Country of publishing house
US - UNITED STATES
Number of pages
33
Pages from-to
22197-22229
UT code for WoS article
001414857100021
EID of the result in the Scopus database
2-s2.0-85216946187