Functionally-Equivalent Formalization and Automated Model Checking of Function Block Diagrams
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 u...
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
IEEE
2025-01-01
|
| Series: | IEEE Access |
| Subjects: | |
| Online Access: | https://ieeexplore.ieee.org/document/10857284/ |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1832088055778902016 |
|---|---|
| author | Tomas Ausberger Karel Kubicek Pavla Medvedcova |
| author_facet | Tomas Ausberger Karel Kubicek Pavla Medvedcova |
| author_sort | Tomas Ausberger |
| collection | DOAJ |
| 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. |
| format | Article |
| id | doaj-art-aff91deab00140eb89d93b8b1d7cbebe |
| institution | Kabale University |
| issn | 2169-3536 |
| language | English |
| publishDate | 2025-01-01 |
| publisher | IEEE |
| record_format | Article |
| series | IEEE Access |
| spelling | doaj-art-aff91deab00140eb89d93b8b1d7cbebe2025-02-06T00:00:19ZengIEEEIEEE Access2169-35362025-01-0113221972222910.1109/ACCESS.2025.353589010857284Functionally-Equivalent Formalization and Automated Model Checking of Function Block DiagramsTomas Ausberger0https://orcid.org/0000-0002-4230-3371Karel Kubicek1https://orcid.org/0000-0002-1228-8422Pavla Medvedcova2https://orcid.org/0000-0001-8384-8872New Technologies for the Information Society (NTIS), Faculty of Applied Sciences, University of West Bohemia in Pilsen, Pilsen, Czech RepublicNew Technologies for the Information Society (NTIS), Faculty of Applied Sciences, University of West Bohemia in Pilsen, Pilsen, Czech RepublicNew Technologies for the Information Society (NTIS), Faculty of Applied Sciences, University of West Bohemia in Pilsen, Pilsen, Czech RepublicIn 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.https://ieeexplore.ieee.org/document/10857284/Formal modelformal verificationfunction block diagramFBDfunctionally-equivalent formalizationFormalization |
| spellingShingle | Tomas Ausberger Karel Kubicek Pavla Medvedcova Functionally-Equivalent Formalization and Automated Model Checking of Function Block Diagrams IEEE Access Formal model formal verification function block diagram FBD functionally-equivalent formalization Formalization |
| title | Functionally-Equivalent Formalization and Automated Model Checking of Function Block Diagrams |
| title_full | Functionally-Equivalent Formalization and Automated Model Checking of Function Block Diagrams |
| title_fullStr | Functionally-Equivalent Formalization and Automated Model Checking of Function Block Diagrams |
| title_full_unstemmed | Functionally-Equivalent Formalization and Automated Model Checking of Function Block Diagrams |
| title_short | Functionally-Equivalent Formalization and Automated Model Checking of Function Block Diagrams |
| title_sort | functionally equivalent formalization and automated model checking of function block diagrams |
| topic | Formal model formal verification function block diagram FBD functionally-equivalent formalization Formalization |
| url | https://ieeexplore.ieee.org/document/10857284/ |
| work_keys_str_mv | AT tomasausberger functionallyequivalentformalizationandautomatedmodelcheckingoffunctionblockdiagrams AT karelkubicek functionallyequivalentformalizationandautomatedmodelcheckingoffunctionblockdiagrams AT pavlamedvedcova functionallyequivalentformalizationandautomatedmodelcheckingoffunctionblockdiagrams |