Promela Formal Modelling and Verification of IEC 61499 Systems with comparison to SMV

Loading...
Thumbnail Image
Journal Title
Journal ISSN
Volume Title
Conference article in proceedings
Date
2021-10-11
Major/Subject
Mcode
Degree programme
Language
en
Pages
6
1-6
Series
2021 IEEE 19th International Conference on Industrial Informatics (INDIN)
Abstract
This paper presents a method of formal modelling of IEC 61499 systems of Function Blocks with Promela1. The existing method of formal verification of IEC 61499 using SMV (Symbolic Model Verifier) is compared with a new approach of verification using SPIN2 which is an explicit-state model-checker. The performance of both approaches is studied using a set of deterministic systems of multiple computational units as an example and a more complex non-deterministic elevator model.
Description
Keywords
Performance evaluation, Computational modeling, Memory management, XML, Tools, Elevators, IEC Standards
Other note
Citation
Shatrov , V & Vyatkin , V 2021 , Promela Formal Modelling and Verification of IEC 61499 Systems with comparison to SMV . in 2021 IEEE 19th International Conference on Industrial Informatics (INDIN) . , 9557513 , IEEE , pp. 1-6 , IEEE International Conference on Industrial Informatics , Palma de Mallorca , Spain , 21/07/2021 . https://doi.org/10.1109/INDIN45523.2021.9557513