On the verification of routing in material handling systems

Der Entwurf von modernen Logistiksystemen ist ein anspruchsvoller Prozess und gestaltet sich zunehmend schwieriger, da Größe und Komplexität ständig wachsen. Besonders die Implementierung von korrekten Routingstrategien ist für die Funktionsfähigkeit und Sicherheit dieser Systeme essentiell. Aktuell werden diese Systeme lediglich durch Simulation validiert. Im Gegensatz dazu kann mit formalen Verifikationsmethoden bewiesen werden, dass ein System seiner Spezifikation genügt. Die Arbeit von Klotz et. al [1] zeigt einen Ansatz zur Verifikation von Logistiksystemen mittels der Verifikationstechnik Model Checking. Dieser Ansatz hat aber den Nachteil, dass er nur auf Systeme moderater Größe angewendet werden kann. In der vorliegenden Arbeit wird ein kompositioneller Ansatz vorgestellt um das Routing in logistischen Systemen zu verifizieren. Dabei wird das Gesamtsystem in Teilsysteme zerlegt, die einzeln verifiziert werden. Von den Teilergebnissen wird auf Eigenschaften des Gesamtsystems geschlossen. Der vorgestellte Ansatz wurde in einem Tool implementiert und genutzt um das Routing eines Gepäcktransportsystems eines Flughafens zu verifizieren. [1] T. Klotz, B. Straube, E. Fordran, J. Haufe, F. Schulze, K. Turek, and T. Schmidt. Toward Verification of Material Handling Systems. In Proceedings of the 9th IEEE International Conference on Industrial Informatics (INDIN), pages 218-223, Lisbon, Portugal, 2011.