Automated Formal Verification of Routing in Material Handling Systems

被引：0

作者：

Klotz, Thomas ^{[1
]}

Schoenherr, Jens ^{[2
]}

Sessler, Norman ^{[1
]}

Straube, Bernd ^{[1
]}

Turek, Karsten ^{[3
]}

机构：

[1] Fraunhofer Inst Integrated Circuits, Design Automat Div, D-01069 Dresden, Germany

[2] Dresden Univ Appl Sci, D-01069 Dresden, Germany

[3] Tech Univ Dresden, Inst Mat Handling & Ind Engn, D-01062 Dresden, Germany

来源：

IEEE TRANSACTIONS ON AUTOMATION SCIENCE AND ENGINEERING | 2013年 / 10卷 / 04期

关键词：

Baggage handling systems (BHS); formal verification; material handling systems (MHS); model checking; routing; NET DECOMPOSITION APPROACH; DEADLOCK; LOGIC; MODEL;

D O I：

10.1109/TASE.2013.2276763

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

The design of correctly implemented controls in material handling systems (MHS) is time consuming and cumbersome. The developer has to deal with an ever increasing complexity and heterogeneity of MHS on the one hand, but also with short development cycles and high demands to MHS on the other hand. For baggage handling systems (BHS) at airports, the error-free implementation of routing strategies is especially of importance, as these strategies are critical to safety. This paper proposes a compositional approach to the formal verification of routing in MHS. The approach is based on the theory of assume-guarantee reasoning, where proofs of the overall system are derived from proofs of subsystems. Moreover, the approach has been implemented in a tool that automatically carries out the verification. A real-world example is discussed in this paper, showing the benefits and scalability of the presented approach.

引用

页码：900 / 915

页数：16

共 50 条

[31] CHALLENGES IN FORMAL METHODS FOR TESTING AND VERIFICATION OF CLOUD COMPUTING SYSTEMS [J].

Gawanmeh, Amjad ;

Alomari, Ahmad .

SCALABLE COMPUTING-PRACTICE AND EXPERIENCE, 2015, 16 (03) :321-332

[32] A Formal Framework of Model and Logical Embeddings for Verification of Stochastic Systems [J].

Das, Susmoy ;

Sharma, Arpit .

39TH ANNUAL ACM SYMPOSIUM ON APPLIED COMPUTING, SAC 2024, 2024, :1712-1721

[33] Spiking neural P systems: matrix representation and formal verification [J].

Gheorghe, Marian ;

Lefticaru, Raluca ;

Konur, Savas ;

Niculescu, Ionut Mihai ;

Adorna, Henry N. .

JOURNAL OF MEMBRANE COMPUTING, 2021, 3 (02) :133-148

[34] Formal Verification of Cloud and Fog Systems: A Review and Research Challenges [J].

Fakhfakh, Fairouz ;

Kallel, Slim ;

Cheikhrouhou, Saoussen .

JOURNAL OF UNIVERSAL COMPUTER SCIENCE, 2021, 27 (04) :341-363

[35] Formal Verification of Concurrent Systems via Directed Model Checking [J].

Gradara, Sara ;

Santone, Antonella ;

Villani, Maria Luisa .

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2007, 185 (93-105) :93-105

[36] Formal Specification and Verification of Self-Adaptive Concurrent Systems [J].

Fakhir, Muhammad Ilyas ;

Kazmi, Syed Asad Raza .

IEEE ACCESS, 2018, 6 :34790-34803

[37] Challenges in formal methods for testing and verification of cloud computing systems [J].

Gawanmeh, Amjad ;

Alomari, Ahmad .

Scalable Computing, 2015, 16 (03) :321-332

[38] Formal Specification and Verification of a Data Replication Approach in Distributed Systems [J].

Souri, Alireza .

INTERNATIONAL JOURNAL OF NEXT-GENERATION COMPUTING, 2016, 7 (01) :18-37

[39] Formal Verification and Synthesis for Discrete-Time Stochastic Systems [J].

Lahijanian, Morteza ;

Andersson, Sean B. ;

Belta, Calin .

IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2015, 60 (08) :2031-2045

[40] Formal Verification of Control Modules in Cyber-Physical Systems [J].

Grobelna, Iwona .

SENSORS, 2020, 20 (18) :1-23

← 1 2 3 4 5 →