Erhöhung der Betriebssicherheit von Materialflusssteuerung durch Anwendung von Methoden des Schaltkreisentwurfs, insb. des Model Checkings
Final Report Abstract
Die Materialflusssteuerung hat großen Einfluss auf die Betriebssicherheit (Leistungsfähigkeit und Zuverlässigkeit) von Materialflusssystemen. Der Steuerungsentwurf wird traditionell mithilfe der Materialflusssimulation überprüft. Das erfordert aufwändige Experimente zur Fehleranalyse und Modell-Evaluierung, ohne vollständige Sicherheit zu liefern. Um diese methodischen Defizite bei der Entwicklung von Materialflusssteuerungen zu beheben und sicherzustellen, dass eine Steuerung tatsächlich stets erwartungskonform und konfliktfrei funktioniert, wurden - im Rahmen einer Zusammenarbeit des Institutsteils Entwurfsautomatisierung des Fraunhofer-Instituts für Integrierte Schaltungen mit der Professur für Technische Logistik der Technischen Universität Dresden - erprobte Methoden der formalen Verifikation aus der industriellen Schaltkreisentwicklung auf die Steuerungsentwicklung für Materialflusssysteme übertragen. Mithilfe der formalen Verifikation mittels Model Checking wird das Systemverhalten vollständig (in der Art eines mathematischen Beweises) auf Fehlerfreiheit geprüft. Voraussetzung sind eine formale Beschreibung des Systems und eine formale Spezifikation der Anforderungen. Der Model Checker bestätigt daraufhin entweder die Korrektheit des Entwurfs oder liefert ein Gegenbeispiel, das zu einem Fehler führt. Im Ergebnis der Forschungsarbeiten liegen nunmehr Model-Checker-Modelle für alle wesentlichen Komponenten von Stetigförderersystemen vor. Diese Modelle lassen sich zu komplexen Systemen verknüpfen. Große Materialflusssysteme lassen sich nach einer Partitionierung entlang der Grenzen ihrer Funktionsbereiche in akzeptabler Zeit prüfen. Es konnte gezeigt werden, dass die Verfahren zur Prüfung von Anforderungen nach zielgenauen, kollisionsfreien und blockierungsfreien Transportabläufen geeignet sind und dass sich die Simulations- und Verifikations-Modelle vergleichbar verhalten. Durch die entwickelten Verfahren eröffnen sich interessante Perspektiven in zweierlei Hinsicht: (a) Zur Verifikation wird die Steuerungslogik formalisiert beschrieben; mithin können daraus Code-Bausteine für den Materialflussrechner abgeleitet werden. So würde sichergestellt, dass dessen Implementation bei der Inbetriebnahme der in der Planungsphase formulierten Spezifikation entspricht, was heute nur mit Einschränkungen durch eine Emulation unter Zuhilfenahme eines Simulationsmodells zu gewährleisten ist. (b) Wenn es zudem gelingt, beim Model Checking bspw. Aussagen zu Durchlaufzeiten zu gewinnen, könnte sich ggf. die Erstellung eines Simulations-Modells erübrigen. Daher sind die Ansätze geeignet, den Prozess des Entwurfs und der Implementation von Materialflusssteuerungen grundlegend zu verändern.
Publications
- (2012): Compositional verification of material handling systems. In: Proceedings of the 17th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA) (Krakow, Polen, 17. September 2012), S. 1-8. - ISBN: 978-1-4673-4737-2, 978-14673-4735-8, 978-1-4673-4736-5
Klotz, Seßler, Straube, Fordran, Turek & Schönherr
(See online at https://doi.org/10.1109/ETFA.2012.6489595) - (2012): On the formal verification of routing in material handling systems. In: Proceedings of the 8th annual IEEE International Conference on Automation Science and Engineering (CASE 2012) (Seoul, Korea, 20. August 2012), S. 8-13. - ISBN: 978-1-4673-0430-6, 978-14673-0429-0, 978-1-4673-0428-3. Ausgezeichnet mit dem „Best Conference Paper Award“
Klotz, Seßler, Straube, Fordran, Turek & Schönherr
(See online at https://doi.org/10.1109/CoASE.2012.6386358) - Ein Ansatz zur Verifikation von Materialflusssteuerungen. In: Tagungsband des 15. Workshops “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” (Kaiserslautern, 5. März 2012), S. 61-71
Klotz, Straube, Fordran, Seßler, Haufe & Schulze
- Automated Formal Verification of Routing in Material Handling Systems. In: IEEE Transactions on Automation Science and Engineering, Bd. 10 (Oktober 2013), Nr. 4, S. 900-915
Klotz, Schönherr, Seßler, Straube & Turek
(See online at https://doi.org/10.1109/TASE.2013.2276763) - Ein Ansatz zur Verifikation von Materialflusssystemen durch Model Checking. In: Simulation in Produktion und Logistik 2013 (Paderborn, 9. Oktober 2013), hrsg.v. Dangelmaier, Laroque & Klaas, S. 385-394 (HNI-Verlagsschriftenreihe 316). - ISBN: 978-3-942647-35-9
Turek, Klotz, Schmidt & Straube
- (2014): Neue Methode zur Erhöhung der Betriebssicherheit von Materialflusssystemen. In: Tagungsband zum 23. Deutschen Materialfluss-Kongress (München, 20. März 2014)
Schmidt, Turek & Klotz
