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.
| Original language | English |
|---|---|
| Title of host publication | 2021 IEEE 19th International Conference on Industrial Informatics (INDIN) |
| Publisher | IEEE |
| Pages | 1-6 |
| Number of pages | 6 |
| ISBN (Electronic) | 978-1-7281-4395-8 |
| ISBN (Print) | 978-1-7281-4396-5 |
| DOIs | |
| Publication status | Published - 11 Oct 2021 |
| MoE publication type | A4 Conference publication |
| Event | IEEE International Conference on Industrial Informatics - Palma de Mallorca, Spain, Palma de Mallorca, Spain Duration: 21 Jul 2021 → 23 Jul 2021 https://2021.ieee-indin.org/ |
Conference
| Conference | IEEE International Conference on Industrial Informatics |
|---|---|
| Abbreviated title | INDIN |
| Country/Territory | Spain |
| City | Palma de Mallorca |
| Period | 21/07/2021 → 23/07/2021 |
| Internet address |
Keywords
- Performance evaluation
- Computational modeling
- Memory management
- XML
- Tools
- Elevators
- IEC Standards