Promela Formal Modelling and Verification of IEC 61499 Systems with comparison to SMV
Loading...
Access rights
openAccess
acceptedVersion
URL
Journal Title
Journal ISSN
Volume Title
A4 Artikkeli konferenssijulkaisussa
This publication is imported from Aalto University research portal.
View publication in the Research portal (opens in new window)
View/Open full text file from the Research portal (opens in new window)
Other link related to publication (opens in new window)
View publication in the Research portal (opens in new window)
View/Open full text file from the Research portal (opens in new window)
Other link related to publication (opens in new window)
Authors
Date
Major/Subject
Mcode
Degree programme
Language
en
Pages
6
Series
2021 IEEE 19th International Conference on Industrial Informatics (INDIN), pp. 1-6
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
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