Formale Synthese verteilter Steuerungen
Final Report Abstract
Ziel des Vorhabens war es, formale Synthesemethoden für verteilte Steuerungen zu erarbeiten und zu implementieren. Bei verteilten Steuerungen ist die Steuerungsaufgabe auf mehrere Komponenten aufgeteilt, die zum Beispiel auf unterschiedlichen, auch räumlich voneinander getrennten, Ressourcen ausgeführt werden. Verteilte Steuerungen bieten die Möglichkeit, die steigende Komplexität von Steuerungsaufgaben zu beherrschen und die räumliche Distanz der Steuerung zum gesteuerten Prozess zu verringern. Die Modularität kann genutzt werden, um die Flexibilität und Rekonfigurierbarkeit von Produktionsabläufen zu erhöhen. Als Ausgangspunkt für die Synthese wurden modulare Streckenmodelle in der Modellform sichere Netz Condition/Event Systeme (Abk. SNCES) und Spezifikationen von verbotenen Zuständen in Form von Zustandsprädikaten erstellt und verwendet. Verboten sind dabei Situationen in der Strecke, in denen Gefahr für Menschen, Maschinen, die Umwelt oder das Produkt existieren. Neben dem besonderen Anspruch verteilte Steuerungen zu erzeugen, liegt das Hauptaugenmerk auf der Beherrschbarkeit der Berechnungskomplexität. Es gilt die explizite Analyse des exponentiell über der Modellkomplexität wachsenden Zustandsraumes zu umgehen. Die Idee ist es, mittels struktureller Methoden zur Ermittlung von Invarianten und der Rückwärtssuche im Modellnetz alle nicht steuerbaren Trajektorien zu verbotenen Zuständen zu bestimmen. Die Steuerungseingriffe müssen das Eintreten in eine solche Trajektorie verhindern. Hierfür können zum einen steuerbare Zustandsübergängen (Schritte) blockiert werden, wir sprechen von der passiven Steuerung, oder die Steuerung erzwingt bestimmte Zustandsübergänge, aus deren Folgezustand keine Trajektorie zu verbotenen Zuständen erreicht wird, wir sprechen von der aktiven Steuerung. Ausgehend von den spezifizierten verbotenen Zuständen werden alle Schritte analysiert, die in einen verbotenen Zustand führen können. Für jeden Schritt wird überprüft, ob seine Aktivierung durch aktive oder passive Steuerungsaktionen verhindert werden kann. Ist das der Fall, wird eine entsprechende Steuerungskomponente erzeugt. Andernfalls gilt der den Schritt aktivierende Zustand ebenfalls als verboten. Auf diese Weise werden die nicht steuerbaren Trajektorien bestimmt, und die Analyse ist beendet, wenn die Aktivierung aller zuletzt berechneten Schritte verhindert werden kann oder kein noch nicht analysierter Vorzustand existiert. Für jede Teilsteuerung werden bei der Analyse sowohl die Funktionalität zur Beeinflussung der zugehörigen Teilstrecke als auch die notwendigen Kommunikationsfunktionen zu anderen Teilsteuerungen synthetisiert. Erfüllt eine gegebene Anfangsmarkierung keines der die verbotenen Zustände beschreibenden Prädikate, wird die Spezifikation als steuerbar bezeichnet. Als Resultat ergibt sich ein Modell von verteilten, untereinander kommunizierenden Steuerungen. Die Teilsteuerungen bestehen aus Kommunikationsfunktionen und Entscheidungsfunktionen. Kommunikationsfunktionen bestimmen die Werte von Kommunikationsvariablen und übermitteln diese an andere Teilsteuerungen. Entscheidungsfunktionen bestimmen die Werte von lokalen Steuerungsausgängen auf der Basis lokaler Beobachtung und den Werten von Kommunikationsvariablen. Jeder Funktionstyp einer Teilsteuerung wird in einen Basic Function Block (Basic FB) nach IEC 61499 überführt. Diese werden unter Nutzung eines IEC 61499 Entwicklungswerkzeugen auf verteilten Steuerungssystemen der Arbeitsgruppe implementiert und an Benchmarks demonstriert. Die Algorithmen zur Bestimmung von Zustandsinvarianten, für die Rückwärtssuche und die Verteilung der Steuerungsfunktionen sind in einem prototypenhaften Tool implementiert. Durch die Anwendung der erarbeiteten, formal korrekten Synthesealgorithmen können korrekte Steuerungskomponenten für Sicherheitsspezifikationen erstellt werden. Gerade im Bereich der Sicherheitsanforderungen ist der Anspruch an korrekte Implementierung besonders hoch und kann durch formale Synthese erfüllt werden. Die Implementierung in Basic FBs nach IEC 61499 ist dabei nur eine Möglichkeit und wurde unter anderem wegen der Möglichkeit gewählt, echt verteilte Steuerungen abzubilden. Methoden zur Implementierung zentraler Steuerungsmodelle in IEC 61131 sind in früheren Projekten erarbeitet worden und können ebenfalls Anwendung finden. Die verbesserte Rückwärtssuche lässt sich ohne weitere Anpassungen auch zur Synthese von Steuerungsfunktionen für zentrale Steuerungen einsetzen.
Publications
- Event graph-based approach to interpretation of NCES models. In: Proceedings of the 7th International Conference of Science and Technology “New Information Technologies and Systems” (NITiS2006), Part 1, Penza, Russia, November 2006, S. 172–186
Dubinin, V.N.; Hanisch, H.-M. and Missal, D.
- Safe net condition/event system models for synthesis of distributed controllers. In: Proceedings of the 7th International Conference of Science and Technology ”New Information Technologies and Systems” (NITiS2006), Part 1, Penza, Russia, November 2006, S. 186–198
Missal, D. und Hanisch, H.-M.
- Synthesis of Distributed Controllers by Means of a Monolithic Approach. In: 11th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA’2006), Prague, September 2006, S. 356–363
Missal, D. and Hanisch, H.-M.
- Hierarchical Distributed Controllers - Design and Verification. In: Proceedings of the IEEE International Conference on Emerging Technologies and Factory Automation (ETFA´2007). Patras-Griechenland, 2007, S. 657-664
Missal, D.; Hirsch, H. und Hanisch, H.-M.
- Modular Plant Modelling for Distributed Control. In: Proceedings of 2007 IEEE International Conference on Systems, Man and Cybernetics, Montréal, Canada, October 2007, S. 3475-3480
Missal, D. und Hanisch, H.-M.
- Reverse partially-marked safe net condition/event systems and its interpretation. In: Proceedings of the 6th All-Russian scientific-practical Conference with the international participation Contemporary Information Technologies in Science, Education and Practice", November 27-28, 2007, Orenburg, Russia, S.168-191
Dubinin, V.N. und Missal, D.
- A Modular Synthesis Approach for Distributed Safety Controllers, Part A: Modelling and Specification. In: 17th IFAC World Congress, proceedings. Seoul, Korea, IFAC, July 2008, S. 14 473–14 478
Missal, D. und Hanisch, H.-M.
- A Modular Synthesis Approach for Distributed Safety Controllers, Part B: Modular Control Synthesis. In: 17th IFAC World Congress, proceedings, Seoul, Korea, July 2008, S. 14 479–14 484
Missal, D. und Hanisch, H.-M.
- Design and Verification of Distributed Industrial Manufacturing Control Systems. In: Proceedings of the Annual Conference of the IEEE Industrial Electronics Society (IECON´2008), Orlando-Florida, USA 2008, S. 152-157
Hirsch, M.; Missal, D. und Hanisch, H.-M.
- Reconfiguration of Embedded Systems. In: Proceedings of the International Conference on Informatics in Control, Automation and Robotics (ICINCO´2008). Funchal, Madeira-Portugal, 2008, S. 157- 162
Khalgui, M.; Hirsch, M.; Missal, D. und Hanisch, H.-M.
- Synthesis of Distributed Forcing/Locking Safety Controllers. In: Proceedings of the Annual Conference of the IEEE Industrial Electronics Society (IECON´2008). Orlando-Florida, USA 2008, S. 383?390
Missal, D. and Hanisch, H.-M.
- One Decade of IEC 61499 Modeling and Verification - Results and Open Issues. In: Proceedings of the IFAC Symposium on Information Control Problems in Manufacturing (INCOM'09). Moscow, Russia 2009, S. 211-216
Hanisch, H.-M.; Hirsch, M.; Missal, D.; Preusse, S. und Gerber, C.
- Synthesis of Distributed Safety Controllers with Incomplete State Observation. In: Annual Conference of the IEEE Industrial Electronics Society (IECON´2009), proceedings. Porto, Portugal, 2009
Missal, D. und Hanisch, H.-M.
