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 Verification of IEC61499 Function Blocks with Abstract State Machines and SMV - Modelling
    Patil, Sandeep
    Dubinin, Victor
    Vyatkin, Valeriy
    2015 IEEE TRUSTCOM/BIGDATASE/ISPA, VOL 3, 2015, : 313 - 320
  • [2] A Comparison of Formal Verification Approaches for IEC 61499
    Blech, Jan Olaf
    Lindgren, Per
    Pereira, David
    Vyatkin, Valeriy
    Zoit, Alois
    2016 IEEE 21ST INTERNATIONAL CONFERENCE ON EMERGING TECHNOLOGIES AND FACTORY AUTOMATION (ETFA), 2016,
  • [3] 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,
  • [4] 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
  • [5] Towards formal verification of IEC61499: modelling of data and algorithms in NCES
    Pang, Cheng
    Vyatkin, Valeriy
    2007 5TH IEEE INTERNATIONAL CONFERENCE ON INDUSTRIAL INFORMATICS, VOLS 1-3, 2007, : 879 - 884
  • [6] 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,
  • [7] Modelling and verification of IEC 61499 applications using Prolog
    Dubinin, Victor
    Vyatkin, Valeriy
    Hanisch, Hans-Michael
    2006 IEEE CONFERENCE ON EMERGING TECHNOLOGIES & FACTORY AUTOMATION, VOLS 1 -3, 2006, : 764 - +
  • [8] Monitoring design pattern for distributed automation systems in IEC 61499 and its formal modelling
    Jhunjhunwala, Pranay
    Zoitl, Alois
    Atmojo, Udayanto Dwi
    Vyatkin, Valeriy
    2022 IEEE 31ST INTERNATIONAL SYMPOSIUM ON INDUSTRIAL ELECTRONICS (ISIE), 2022, : 220 - 225
  • [9] Formal models for the verification of IEC 61499 function block based control applications
    Lueder, Arndt
    Schwab, Christian
    Tangermann, Marcus
    Peschke, Joern
    ETFA 2005: 10TH IEEE INTERNATIONAL CONFERENCE ON EMERGING TECHNOLOGIES AND FACTORY AUTOMATION, VOL 1, PTS 1 AND 2, PROCEEDINGS, 2005, : 105 - 112
  • [10] Formal modeling and verification in the software engineering framework of IEC61499: a way to self-verifying systems
    Vyatkin, V
    Hanisch, HM
    ETFA 2001: 8TH IEEE INTERNATIONAL CONFERENCE ON EMERGING TECHNOLOGIES AND FACTORY AUTOMATION, VOL 2, PROCEEDINGS, 2001, : 113 - 118
12345