e-journal

Automated Formal Verification of Routing in Material Handling Systems

---

The design of correctly implemented controls inmaterial 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. Note to Practitioners—Routing strategies inMHS such as BHS at airports can be complex, and thus, their implementation is tedious and error-prone. Currently, these systems are simulated to validate
their control strategies, and then implemented on real equipment. With this, however, only a limited number of test cases is considered, and hence, routing errors may stay undetected. This paper proposes an approach to automatically prove the correctness of routing strategies in MHS by means of formal erification. A main difficulty of the formal verification of real-world MHS is the so-called state space explosion, i.e., the model to be verified has too many states. To also apply formal verification to these systems, a compositional approach is presented which allows to verify system properties with regard to routing in a reasonable amount of time. A case study shows the application of the approach to the
BHS of an international airport. A number of properties with respect to routing functionality have been proven automatically for this system, for instance, no unclear or unidentified bags reach an
airplane. Furthermore, the proposed approach is not restricted to routing only and can be extended for other system properties.
Index Terms—Baggage handling systems (BHS), formal verification, material handling systems (MHS), model checking, routing.

---

Ketersediaan

Tidak ada salinan data

Informasi Detail

Judul Seri

IEEE TRANSACTIONS ON AUTOMATION SCIENCE AND ENGINEERING

No. Panggil

-

Penerbit

New York : IEEE., 2013

Deskripsi Fisik

IEEE TRANSACTIONS ON AUTOMATION SCIENCE AND ENGINEERING, VOL. 10, NO. 4, OCTOBER 2013

Bahasa

English

ISBN/ISSN

1545-5955

Klasifikasi

-

Tipe Isi

-

Tipe Media

-

Tipe Pembawa

-

Edisi

VOL. 10, NO. 4, OCTOBER 2013

Subjek

TEKNIK

Info Detail Spesifik

-

Pernyataan Tanggungjawab

Yuli/Agus

Versi lain/terkait

Lampiran Berkas

Komentar

---

Anda harus masuk sebelum memberikan komentar