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 条
  • [1] Formal Modelling and Verification of IEC61499 Function Blocks with Abstract State Machines and SMV - Execution Semantics
    Patil, Sandeep
    Dubinin, Victor
    Vyatkin, Valeriy
    DEPENDABLE SOFTWARE ENGINEERING: THEORIES, TOOLS, AND APPLICATIONS, SETTA 2015, 2015, 9409 : 300 - 315
  • [2] Cyber-physical automation systems modelling with IEC 61499 for their formal verification
    Xavier, Midhun
    Patil, Sandeep
    Vyatkin, Valeriy
    2021 IEEE 19TH INTERNATIONAL CONFERENCE ON INDUSTRIAL INFORMATICS (INDIN), 2021,
  • [3] Formal modeling and verification of IEC 61499 function blocks on the basis of transition systems
    Dubinin, Victor
    Vyatkin, Valeriy
    Shalyto, Anatoly
    2016 INTERNATIONAL SIBERIAN CONFERENCE ON CONTROL AND COMMUNICATIONS (SIBCON), 2016,
  • [4] Formal Verification of the Control Software of a Radioactive Material Remote Handling System, Based on IEC 61499
    Lilli, Giordano
    Xavier, Midhun
    Le Priol, Etienne
    Perret, Vincent
    Liakh, Tatiana
    Oboe, Roberto
    Vyatkin, Valeriy
    IEEE OPEN JOURNAL OF THE INDUSTRIAL ELECTRONICS SOCIETY, 2023, 4 : 417 - 431
  • [5] Transformation of Simulink models to IEC 61499 Function Blocks for verification of distributed control systems
    Yang, Chia-han
    Vyatkin, Valeriy
    CONTROL ENGINEERING PRACTICE, 2012, 20 (12) : 1259 - 1269
  • [6] 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
  • [7] Formal modelling of IEC 61499 function blocks with integer-valued data types
    Gerber, Christian
    Ivanova-Vasileva, Ioanna
    Hanisch, Hans-Michael
    CONTROL AND CYBERNETICS, 2010, 39 (01): : 197 - 231
  • [8] 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
  • [9] 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
  • [10] Implementing Constrained Cyber-Physical Systems with IEC 61499
    Yoong, Li Hsien
    Roop, Partha S.
    Salcic, Zoran
    ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS, 2012, 11 (04)
12345