Compositional verification of material handling systems

The design of properly working material handling systems (MHS) is a difficult process as these systems consist of a vast number of single elements with dedicated controls. While currently these systems are usually validated using simulation, formal methods provide a means to analyze the complete behavior of a system. However, these methods can often only be applied to systems of a moderate size, which hampers their application to verify real-world systems. This paper presents an approach to the compositional verification of MHS, which is based on the theory of assume-guarantee reasoning. The approach has been implemented in a tool that automatically carries out the verification. The application of the approach is shown using a real-world example.