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] IEC 61499 and the Promise of Holonic Systems
    Brennan, Robert W.
    Lyu, Guolin
    INDUSTRIAL APPLICATIONS OF HOLONIC AND MULTI-AGENT SYSTEMS (HOLOMAS 2019), 2019, 11710 : 3 - 12
  • [22] Formal model of IEC 61499 execution trace in FBME IDE
    Liakh, Tatiana
    Sorokin, Radimir
    Akifev, Daniil
    Patil, Sandeep
    Vyatkin, Valeriy
    2022 IEEE 20TH INTERNATIONAL CONFERENCE ON INDUSTRIAL INFORMATICS (INDIN), 2022, : 588 - 593
  • [23] Formal syntax and semantics of basic function blocks in IEC 61499
    Tu, Y.
    Li, D.
    Li, S.
    PROCEEDINGS OF THE INSTITUTION OF MECHANICAL ENGINEERS PART C-JOURNAL OF MECHANICAL ENGINEERING SCIENCE, 2012, 226 (C4) : 1025 - 1035
  • [24] A Formal Perspective on IEC 61499 Execution Control Chart Semantics
    Lindgren, Per
    Lindner, Marcus
    Pereira, David
    Pinho, Luis Miguel
    2015 IEEE TRUSTCOM/BIGDATASE/ISPA, VOL 3, 2015, : 293 - 300
  • [25] Modelling Industrial Cyber-Physical Systems using IEC 61499 and OPC UA
    Dai, Wenbin
    Song, Yineng
    Zhang, Zhijie
    Wang, Peng
    Pang, Cheng
    Vyatkin, Valeriy
    2018 IEEE 16TH INTERNATIONAL CONFERENCE ON INDUSTRIAL INFORMATICS (INDIN), 2018, : 772 - 777
  • [26] PROMELA based formal verification for safety-critical software
    Xing, Liang
    Ding, Chengjun
    Du, Hupeng
    Ma, Chunyan
    Xibei Gongye Daxue Xuebao/Journal of Northwestern Polytechnical University, 2022, 40 (05): : 1180 - 1187
  • [27] Formal Modelling and Verification of Concurrent Systems with XCCS
    Szpyrka, Marcin
    Matyasik, Piotr
    PROCEEDINGS OF THE INTERNATIONAL SYMPOSIUM ON PARALLEL AND DISTRIBUTED COMPUTING, 2008, : 454 - 458
  • [28] On Portability of IEC 61499 Compliant Structures and Systems
    Hopsu, Alexander
    Atmojo, Udayanto Dwi
    Vyatkin, Valeriy
    2019 IEEE 28TH INTERNATIONAL SYMPOSIUM ON INDUSTRIAL ELECTRONICS (ISIE), 2019, : 1306 - 1311
  • [29] From IEC 61131 to IEC 61499 for Distributed Systems: A Case Study
    Gerber, Christian
    Hanisch, Hans-Michael
    Ebbinghaus, Sven
    EURASIP JOURNAL ON EMBEDDED SYSTEMS, 2008, (01)
  • [30] On Formal Analysis of IEC 61499 Applications, Part B: Execution Semantics
    Cengic, Goran
    Akesson, Knut
    IEEE TRANSACTIONS ON INDUSTRIAL INFORMATICS, 2010, 6 (02) : 145 - 154
12345