Formal Verification of Cyber-Physical Automation Systems Modelled with Timed Block Diagrams

Dmitrii Drozdov*, Sandeep Patil, Victor Dubinin, Valeriy Vyatkin

*Tämän työn vastaava kirjoittaja

Tutkimustuotos: Artikkeli kirjassa/konferenssijulkaisussaConference contributionScientificvertaisarvioitu

6 Sitaatiot (Scopus)


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.

OtsikkoProceedings of the 25th IEEE International Symposium on Industrial Electronics, ISIE 2016
ISBN (elektroninen)978-1-5090-0873-5
DOI - pysyväislinkit
TilaJulkaistu - 2016
OKM-julkaisutyyppiA4 Artikkeli konferenssijulkaisuussa
TapahtumaInternational Symposium on Industrial Electronics - Santa Clara, Yhdysvallat
Kesto: 8 kesäkuuta 201610 kesäkuuta 2016
Konferenssinumero: 24


NimiProceedings of the IEEE International Symposium on Industrial Electronics
ISSN (painettu)2163-5137


ConferenceInternational Symposium on Industrial Electronics
KaupunkiSanta Clara

Siteeraa tätä