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 条

[41] Intelligent Component-Based Automation of Baggage Handling Systems With IEC 61499 [J].

Black, Geoff ;

Vyatkin, Valeriy .

IEEE TRANSACTIONS ON AUTOMATION SCIENCE AND ENGINEERING, 2010, 7 (02) :337-351

[42] Formal verification of reconfigurable systems [J].

Rahim, Muhammad Abdul Basit Ur ;

Raheem, Muhammad Ahsan Ur ;

Sohail, Muhammad Khalid ;

Farid, Mohammad Atif ;

Mufti, Muhammad Rafiq .

SOFT COMPUTING, 2023,

[43] An Example of Modeling Manufacturing Systems Using Petri Nets and the IEC 61499 Standard [J].

Vlad, Valentin ;

Ciufudean, Calin ;

Graur, Adrian ;

Filote, Constantin .

PROCEEDINGS OF THE 13TH WSEAS INTERNATIONAL CONFERENCE ON SYSTEMS: RECENT ADVANCES IN SYSTEMS, 2009, :357-+

[44] Formal Modelling and Verification of Spinlocks at Instruction Level [J].

Zhang, Leping ;

Zhang, Qianying ;

Wang, Guohui ;

Shi, Zhiping ;

Wu, Minhua ;

Guan, Yong .

2019 26TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC), 2019, :355-362

[45] Explicit-Symbolic Modelling for Formal Verification [J].

Costa, Umberto ;

Campos, Sergio ;

Vieira, Newton ;

Deharbe, David .

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 130 :301-321

[46] Modelling and Formal Verification of Neuronal Archetypes Coupling [J].

De Maria, Elisabetta ;

L'Yvonnet, Thibaud ;

Gaffe, Daniel ;

Ressouche, Annie ;

Grammont, Franck .

PROCEEDINGS OF THE EIGHTH INTERNATIONAL CONFERENCE ON COMPUTATIONAL SYSTEMS-BIOLOGY AND BIOINFORMATICS (CSBIO 2017), 2017, :3-10

[47] Multi-agent Based IEC 61499 Function Block Modelling for Distributed Intelligent Automation [J].

Lyu, Guolin ;

Brennan, Robert W. .

FLEXIBLE AUTOMATION AND INTELLIGENT MANUFACTURING: THE HUMAN-DATA-TECHNOLOGY NEXUS, FAIM 2022, VOL 2, 2023, :395-407

[48] Identifying repeating patterns in IEC 61499 systems using Feature-Based embeddings [J].

Unterdechler, Markus ;

Gutierrez, Antonio M. ;

Sonnleithner, Lisa ;

Rabiser, Rick ;

Zoitl, Alois .

2022 IEEE 27TH INTERNATIONAL CONFERENCE ON EMERGING TECHNOLOGIES AND FACTORY AUTOMATION (ETFA), 2022,

[49] Formal Specification and Verification of Autonomous Robotic Systems: A Survey [J].

Luckcuck, Matt ;

Farrell, Marie ;

Dennis, Louise A. ;

Dixon, Clare ;

Fisher, Michael .

ACM COMPUTING SURVEYS, 2019, 52 (05)

[50] Automated Formal Verification of Routing in Material Handling Systems [J].

Klotz, Thomas ;

Schoenherr, Jens ;

Sessler, Norman ;

Straube, Bernd ;

Turek, Karsten .

IEEE TRANSACTIONS ON AUTOMATION SCIENCE AND ENGINEERING, 2013, 10 (04) :900-915

← 1 2 3 4 5 →