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 条

[41] Formal verification of double two out of two computer systems [J].

Feng H. ;

Ma X. ;

Fu W. ;

Pan M. .

International Journal of Performability Engineering, 2018, 14 (11) :2760-2768

[42] FARAD: Automated Formal Verification of Approximate Restoring Array Dividers [J].

Jha, Chandan Kumar ;

Qayyum, Khushboo ;

Hassan, Muhammad ;

Drechsler, Rolf .

2025 38TH INTERNATIONAL CONFERENCE ON VLSI DESIGN AND 2024 23RD INTERNATIONAL CONFERENCE ON EMBEDDED SYSTEMS, VLSID, 2025, :43-48

[43] Safety Assessment of Collaborative Robotics Through Automated Formal Verification [J].

Vicentini, Federico ;

Askarpour, Mehrnoosh ;

Rossi, Matteo G. ;

Mandrioli, Dino .

IEEE TRANSACTIONS ON ROBOTICS, 2020, 36 (01) :42-61

[44] Automated Formal Verification of X Propagation with Respect to Testability Issues [J].

Dehbashi, Mehdi ;

Tille, Daniel ;

Pfannkuchen, Ulrike ;

Eggersgluess, Stephan .

2014 9TH INTERNATIONAL DESIGN & TEST SYMPOSIUM (IDT), 2014, :106-111

[45] Formal Verification of Websites [J].

Flores, Sonia ;

Lucas, Salvador ;

Villanueva, Alicia .

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2008, 200 (03) :103-118

[46] Formal Specification and Verification of Mobile Agent Systems [J].

Kahloul, L. ;

Grira, M. .

INTERNATIONAL JOURNAL OF COMPUTERS COMMUNICATIONS & CONTROL, 2014, 9 (03) :292-304

[47] Formal Verification of Hardware Components in Critical Systems [J].

Khan, Wilayat ;

Kamran, Muhammad ;

Naqvi, Syed Rameez ;

Khan, Farrukh Aslam ;

Alghamdi, Ahmed S. ;

Alsolami, Eesa .

WIRELESS COMMUNICATIONS & MOBILE COMPUTING, 2020, 2020

[48] Formal verification of cP systems using Coq [J].

Yezhou Liu ;

Radu Nicolescu ;

Jing Sun .

Journal of Membrane Computing, 2021, 3 :205-220

[49] FORMAL VERIFICATION OF P SYSTEMS USING SPIN [J].

Ipate, Florentin ;

Lefticaru, Raluca ;

Tudose, Cristina .

INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE, 2011, 22 (01) :133-142

[50] Formal Verification of Weakly-Hard Systems [J].

Huang, Chao ;

Li, Wenchao ;

Zhu, Qi .

PROCEEDINGS OF THE 2019 22ND ACM INTERNATIONAL CONFERENCE ON HYBRID SYSTEMS: COMPUTATION AND CONTROL (HSCC '19), 2019, :197-207

← 1 2 3 4 5 →