Abstract
In this paper a new modelling approach is presented to be used for formal-verification of block-diagram executable specifications of distributed industrial cyber-physical systems following the IEC 61499 standard. The approach allows usage of timers and arithmetic operations in the controller code. SMV model-checker is used as the target tool. The function block modelswith multiple communicating plant-controller closed-loops are transformed to the SMV modelling language using a dedicated model-generator tool. The paper first deals with SMV modelling of the IEC 61499 specific timer function block types. In particular, modelling of hierarchical function block systems with timers located at different levels of hierarchy is addressed. The paper then presents plant abstraction techniques so that the complexity of cyber-physical systems models is reduced. The abstraction uses discrete-timed state machine model implemented in UPPAAL. Delays in the plant model are interpreted as model time constraints. The approach is illustrated with an example of formal verification of a modular mechatronic automated system. The achieved results extend the abilities in validation of real cyber-physical automation systems. The paper also demonstrates how this result helps in counterexample guided simulation in Ciros 3D simulation environment, which improves practical usability of formal verification.
Original language | English |
---|---|
Title of host publication | Proceedings of the 25th IEEE International Symposium on Industrial Electronics, ISIE 2016 |
Publisher | IEEE |
Pages | 316-321 |
Number of pages | 6 |
ISBN (Electronic) | 978-1-5090-0873-5 |
DOIs | |
Publication status | Published - 2016 |
MoE publication type | A4 Conference publication |
Event | International Symposium on Industrial Electronics - Santa Clara, United States Duration: 8 Jun 2016 → 10 Jun 2016 Conference number: 24 http://isie2016.org/ |
Publication series
Name | Proceedings of the IEEE International Symposium on Industrial Electronics |
---|---|
Publisher | IEEE |
ISSN (Print) | 2163-5137 |
Conference
Conference | International Symposium on Industrial Electronics |
---|---|
Abbreviated title | ISIE |
Country/Territory | United States |
City | Santa Clara |
Period | 08/06/2016 → 10/06/2016 |
Internet address |
Keywords
- Cyber-physical systems
- formal verification
- model-checking
- timed formalisms
- IEC 61499
- SMV