Functionally-Equivalent Formalization and Automated Model Checking of Function Block Diagrams

Kód výsledku v 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>

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

Functionally-Equivalent Formalization and Automated Model Checking of Function Block Diagrams

Popis výsledku v původním jazyce

In the development and verification of safety-critical and safety-related Instrumentation and Control (I&amp;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&amp;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&amp;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&amp;C system under which the obtained proofs can also be expected in the physical I&amp;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.

Název v anglickém jazyce

Functionally-Equivalent Formalization and Automated Model Checking of Function Block Diagrams

Popis výsledku anglicky

In the development and verification of safety-critical and safety-related Instrumentation and Control (I&amp;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&amp;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&amp;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&amp;C system under which the obtained proofs can also be expected in the physical I&amp;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.

Druh

J_imp - Článek v periodiku v databázi Web of Science

CEP obor

—

OECD FORD obor

20205 - Automation and control systems

Projekt

<a href="/cs/project/9A22007" target="_blank" >9A22007: Optimization of Electric Vehicle Autonomy</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2025

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

IEEE Access

ISSN

2169-3536

e-ISSN

2169-3536

Svazek periodika

13

Číslo periodika v rámci svazku

29 January 2025

Stát vydavatele periodika

US - Spojené státy americké

Počet stran výsledku

33

Strana od-do

22197-22229

Kód UT WoS článku

001414857100021

EID výsledku v databázi Scopus

2-s2.0-85216946187