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] RVF - AN AUTOMATED FORMAL VERIFICATION SYSTEM
    WANG, TC
    GOLDBERG, A
    LECTURE NOTES IN ARTIFICIAL INTELLIGENCE, 1992, 607 : 735 - 739
  • [42] Automated formal verification for VHDL designs
    Lin, FY
    Li, HC
    COMPUTERS AND THEIR APPLICATIONS - PROCEEDINGS OF THE ISCA 11TH INTERNATIONAL CONFERENCE, 1996, : 174 - 177
  • [43] Automated formal analysis and verification: an overview
    Krena, Bohuslav
    Vojnar, Tomas
    INTERNATIONAL JOURNAL OF GENERAL SYSTEMS, 2013, 42 (04) : 335 - 365
  • [44] Formal Verification of the Control Software of a Radioactive Material Remote Handling System, Based on IEC 61499
    Lilli, Giordano
    Xavier, Midhun
    Le Priol, Etienne
    Perret, Vincent
    Liakh, Tatiana
    Oboe, Roberto
    Vyatkin, Valeriy
    IEEE OPEN JOURNAL OF THE INDUSTRIAL ELECTRONICS SOCIETY, 2023, 4 : 417 - 431
  • [45] On-line reconfiguration to enhance the routing flexibility of complex automated material handling operations
    Wong, M. M.
    Tan, C. H.
    Zhang, J. B.
    Zhuang, L. Q.
    Zhao, Y. Z.
    Luo, M.
    ROBOTICS AND COMPUTER-INTEGRATED MANUFACTURING, 2007, 23 (03) : 294 - 304
  • [46] Approach to a Simulation-Based Verification Environment for Material Handling Systems
    Seidel, Stephan
    Donath, Ulrich
    Haufe, Juergen
    2012 IEEE 17TH CONFERENCE ON EMERGING TECHNOLOGIES & FACTORY AUTOMATION (ETFA), 2012,
  • [47] Formal Modeling and Verification of Rumor Routing Protocol
    Yasin, Daniyal
    Saghar, Kashif
    Younis, Shahzad
    2016 13TH INTERNATIONAL BHURBAN CONFERENCE ON APPLIED SCIENCES AND TECHNOLOGY (IBCAST), 2016, : 318 - 323
  • [48] Formal verification of the RCMP Egress routing logic
    Murugesh, P
    Tahar, S
    ICM'99: ELEVENTH INTERNATIONAL CONFERENCE ON MICROELECTRONICS - PROCEEDINGS, 1999, : 89 - 92
  • [49] Formal model of human material-handling tasks for control of manufacturing systems
    Shin, Dongmin
    Wysk, Richard A.
    Rothrock, Ling
    IEEE TRANSACTIONS ON SYSTEMS MAN AND CYBERNETICS PART A-SYSTEMS AND HUMANS, 2006, 36 (04): : 685 - 696
  • [50] Introduction to automated material handling systems in LCD panel production lines
    Jang, Young Jae
    Choi, Gi-Han
    2006 IEEE INTERNATIONAL CONFERENCE ON AUTOMATION SCIENCE AND ENGINEERING, VOLS 1 AND 2, 2006, : 223 - +
12345