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

被引：1
作者：
Shatrov, Viktor [1 ]
Vyatkin, Valeriy [2 ]
机构：
[1] ITMO Univ, Comp Technol Dept, St Petersburg, Russia
[2] Aalto Univ, Dept Elect Engn & Automat, Helsinki, Finland
来源：
2021 IEEE 19TH INTERNATIONAL CONFERENCE ON INDUSTRIAL INFORMATICS (INDIN) | 2021年
基金：
欧盟地平线“2020”;
关键词：
IEC; 61499; formal verification; model-checking; function blocks; SPIN; SMV; Promela;
D O I：
10.1109/INDIN45523.2021.9557513
中图分类号：
TP39 [计算机的应用];
学科分类号：
081203 ; 0835 ;
摘要：
This paper presents a method of formal modelling of IEC 61499 systems of Function Blocks with Promela(1). 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.
引用
收藏
页数：6
相关论文
共 50 条
  • [31] Designing Efficient Reconfigurable Control Systems Using IEC61499 and Symbolic Model Checking
    Guellouz, Safa
    Benzina, Adel
    Khalgui, Mohamed
    Frey, Georg
    Li, Zhiwu
    Vyatkin, Valeriy
    [J]. IEEE TRANSACTIONS ON AUTOMATION SCIENCE AND ENGINEERING, 2019, 16 (03) : 1110 - 1124
  • [32] Reliability of Replicated Distributed Control Systems Applications Based on IEC 61499
    Santos, Adriano A.
    da Silva, Antonio Ferreira
    Magalhaes, Antonio
    de Sousa, Mario
    [J]. INNOVATIONS IN MECHATRONICS ENGINEERING, 2022, : 301 - 312
  • [33] Design and implementation of distributed hierarchical automation and control systems with IEC 61499
    Ferrarini, L
    Veber, C
    [J]. 2005 3RD IEEE INTERNATIONAL CONFERENCE ON INDUSTRIAL INFORMATICS (INDIN), 2005, : 74 - 79
  • [34] Software Containers as a Generic Foundation for IEC 61499 Distributed Control Systems
    Senington, Richard
    [J]. ADVANCES IN MANUFACTURING TECHNOLOGY XXXII, 2018, 8 : 273 - 278
  • [35] On Automatic Generation of IEC61850/IEC61499 Substation Automation Systems Enabled by Ontology
    Yang, Chen-Wei
    Vyatkin, Valeriy
    Mousavi, Arash
    Dubinin, Victor
    [J]. IECON 2014 - 40TH ANNUAL CONFERENCE OF THE IEEE INDUSTRIAL ELECTRONICS SOCIETY, 2014, : 3577 - 3583
  • [36] Formal verification of ethical choices in autonomous systems
    Dennis, Louise
    Fisher, Michael
    Slavkovik, Marija
    Webster, Matt
    [J]. ROBOTICS AND AUTONOMOUS SYSTEMS, 2016, 77 : 1 - 14
  • [37] Safe Dynamic Reconfiguration Through Supervisory Control in IEC 61499 Compliant Systems
    Pinto, Leandro I.
    Leal, Andre B.
    Rosso, Roberto S. U., Jr.
    [J]. 2017 IEEE 15TH INTERNATIONAL CONFERENCE ON INDUSTRIAL INFORMATICS (INDIN), 2017, : 753 - 758
  • [38] Structuring Cyber-Physical Systems for Distributed Control with IEC 61499 Standard
    Cruz, Ernesto Monroy
    Carrillo, Luis Rodolfo Garcia
    Salazar, Luis Alberto Cruz
    [J]. IEEE LATIN AMERICA TRANSACTIONS, 2023, 21 (02) : 251 - 259
  • [39] Formal Modelling and Verification of Real-Time Self-Adaptive Systems
    Cicirelli, Franco
    Nigro, Libero
    Pupo, Francesco
    [J]. 2019 IEEE/ACM 23RD INTERNATIONAL SYMPOSIUM ON DISTRIBUTED SIMULATION AND REAL TIME APPLICATIONS (DS-RT), 2019, : 154 - 161
  • [40] Redesign Distributed PLC Control Systems Using IEC 61499 Function Blocks
    Dai, Wenbin
    Vyatkin, Valeriy
    [J]. IEEE TRANSACTIONS ON AUTOMATION SCIENCE AND ENGINEERING, 2012, 9 (02) : 390 - 401
12345