Automated Formal Verification of Routing in Material Handling Systems
Automated Formal Verification of Routing in Material Handling Systems
复制标题
DOI：
10.1109/tase.2013.2276763
复制
发表时间：
2013-08
影响因子：
5.6
通讯作者：
Thomas Klotz;J. Schönherr;Norman Seßler;B. Straube;Karsten Turek
中科院分区：
文献类型：
--
作者：
Thomas Klotz;J. Schönherr;Norman Seßler;B. Straube;Karsten Turek
在物料搬运系统(MHS)中正确实施控制的设计既耗时又繁琐。开发人员一方面要应对MHS日益增长的复杂性和异构性，另一方面又要应对开发周期短、对MHS要求高的问题。对于机场的行李处理系统(BHS)，无错误地实施路线策略尤其重要，因为这些策略对安全至关重要。本文提出了一种用于MHS中路由形式化验证的组合方法。该方法基于假设-保证推理理论，其中整个系统的证明是从子系统的证明中得到的。此外，该方法已在自动执行验证的工具中实现。文中给出了一个实际的例子，展示了该方法的优点和可扩展性。
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.