Modeling and verification of material handling systems

This thesis presents a novel approach for the verification of controls in material handling systems. While currently these controls are mostly validated using simulation, in the proposed approach, the correctness of the involved controls is automatically proven by means of model checking. Model checking is a formal method that automatically verifies whether a system meets its specification by exhaustively analyzing a model of the corresponding system. To achieve a model of the material handling system, a modeling methodology has been developed and is introduced in this thesis. The methodology is based on the definition of material handling system elements, which are models of technical components such as conveyors or pushers. By interconnecting these elements, a model of the material handling system is built, which thereafter can be fed into a model checker to prove certain properties on the model. In order to also verify large and complex material handling systems, a compositional approach is proposed. There, the overall material handling system is partitioned into subsystems, which are subsequently verified separately. From the proofs of the subsystems, a proof of a property of the whole material handling system is derived. Practical experiments show how the proposed approach handles the verification of real-world material handling systems.