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 条
  • [21] Formal modelling and verification of interlocking systems featuring sequential release
    Linh Hong Vu
    Haxthausen, Anne E.
    Peleska, Jan
    SCIENCE OF COMPUTER PROGRAMMING, 2017, 133 : 91 - 115
  • [22] Fault Handling in Discrete Event Systems Applied to IEC 61499
    Leitao, Herbert A. S.
    Rosso Jr, Roberto S. U.
    Leal, Andre B.
    Zoitl, Alois
    2020 25TH IEEE INTERNATIONAL CONFERENCE ON EMERGING TECHNOLOGIES AND FACTORY AUTOMATION (ETFA), 2020, : 1039 - 1042
  • [23] Formal Verification of Cyber-Physical Automation Systems Modelled with Timed Block Diagrams
    Drozdov, Dmitrii
    Patil, Sandeep
    Dubinin, Victor
    Vyatkin, Valeriy
    PROCEEDINGS 2016 IEEE 25TH INTERNATIONAL SYMPOSIUM ON INDUSTRIAL ELECTRONICS (ISIE), 2016, : 316 - 321
  • [24] Adaptive Industrial Control Systems via IEC 61499 and Runtime Enforcement
    Faqrizal, Irman
    Salaün, Gwen
    Falcone, Yliès
    ACM Transactions on Autonomous and Adaptive Systems, 2024, 19 (04)
  • [25] On automatic generation of OPC UA connections in IEC 61499 automation systems
    Lyu, Tuojian
    Atmojo, Udayanto Dwi
    Vyatkin, Valeriy
    2022 IEEE 5TH INTERNATIONAL CONFERENCE ON INDUSTRIAL CYBER-PHYSICAL SYSTEMS, ICPS, 2022,
  • [26] Developing IEC 61499 compliant distributed systems with network enabled controllers
    Hussain, T
    Frey, G
    2004 IEEE CONFERENCE ON ROBOTICS, AUTOMATION AND MECHATRONICS, VOLS 1 AND 2, 2004, : 507 - 512
  • [27] Reliability of Replicated Distributed Control Systems Applications Based on IEC 61499
    Santos, Adriano A.
    da Silva, Antonio Ferreira
    Magalhaes, Antonio
    de Sousa, Mario
    INNOVATIONS IN MECHATRONICS ENGINEERING, 2022, : 301 - 312
  • [28] Design and implementation of distributed hierarchical automation and control systems with IEC 61499
    Ferrarini, L
    Veber, C
    2005 3RD IEEE INTERNATIONAL CONFERENCE ON INDUSTRIAL INFORMATICS (INDIN), 2005, : 74 - 79
  • [29] Designing Efficient Reconfigurable Control Systems Using IEC61499 and Symbolic Model Checking
    Guellouz, Safa
    Benzina, Adel
    Khalgui, Mohamed
    Frey, Georg
    Li, Zhiwu
    Vyatkin, Valeriy
    IEEE TRANSACTIONS ON AUTOMATION SCIENCE AND ENGINEERING, 2019, 16 (03) : 1110 - 1124
  • [30] Design and Execution Issues in IEC 61499 Distributed Automation and Control Systems
    Strasser, Thomas
    Zoitl, Alois
    Christensen, James H.
    Suender, Christoph
    IEEE TRANSACTIONS ON SYSTEMS MAN AND CYBERNETICS PART C-APPLICATIONS AND REVIEWS, 2011, 41 (01): : 41 - 51
12345