Durchgängiger Entwurf diskreter Steuerungsprogramme mit Unterstützung durch formale Methoden
Final Report Abstract
Die Modellierung von Systemen in verschiedenen Abstraktionsgraden zum Zweck der Analyse ist in allen ingenieurs- wie naturwissenschaftlichen Fächern gängige Praxis. Dabei bestimmt die Form und die gewünschte Genauigkeit der Darstellung der zu untersuchenden Prozesse die Art und Komplexität der Modelle. Entsprechend des zugrundeliegenden Charakters der Prozesse werden meist rein kontinuierliche oder rein diskrete Modellformen gewählt. Jede Form für sich besitzt Methoden zur Analyse bezüglich bestimmter Eigenschaften und zur Synthese von Modellerweiterungen zur Erreichung bestimmter Eigenschaften. Viele Prozesse lassen sich jedoch nicht oder nur erschwert rein kontinuierlich bzw. rein diskret modellieren, vielmehr besitzen sie inhärent kontinuierliches und diskretes Verhalten. Aus diesem Grund ist in den letzten Jahrzehnten das Forschungsgebiet der hybriden Systeme entstanden, welches die Anpassung und Neuentwicklung von Methodiken zur Analyse und Synthese in diesem Gebiet nach sich zieht. Im Rahmen des Forschungsvorhabens wurde das Petri-Netz-Zustandsraummodell (PNZ) mit der weit verbreiteten Modellform Hybrider Automat verglichen. Eine Eignung zur Modellierung in PNZ konnte festgestellt werden, hinsichtlich der Übersichtlichkeit und der Praxisanwendung sind Vorteile auf Seiten der PNZ erkennbar, wobei die Äquivalenz der Darstellungsmächtigkeit gezeigt wurde. Mit Hilfe der PNZ sind technische Systeme darstellbar, eine strukturierte Modellierung mit Einteilung in Strecke und Steuerung ist möglich, wenn auch in der Praxis nicht immer angewendet. Die Modularitat der PNZ erübrigt die Betrachtung und Entwicklung von Hierarchisierungskonzepten für diese Modellform, jedoch für reine Stellen-/TVansitionsnetze wurde im Rahmen des Vorhabens in einer freien Kooperation mit Frau Dr.-Ing. Julia Padberg vom Lehrstuhl für Theoretische Informatik und Formale Spezifikation der Technischen Universität Berlin ein Konzept zur vertikalen Hierarchisierung von Petri-Netzen unter Berücksichtigung der Gewährleistung von bestimmten Netzeigenschaften entwickelt und in der Modellfabrik des Instituts für Regelungstechnik appliziert. Eine Erweiterung des PNZ um Test- und Inhibitorkanten ist ermöglicht worden und schafft damit eine klarere Darstellung im diskreten Teil des Modells, was dem Gedanken des Rapid-Control-Prototyping (RCP) entspricht. Die Erweiterung fußt dabei auf der Beschränktheit der verwendeten Netze. Deren Netzeigenschaften können aufgrund des Determinismus der Untersuchungsalgorithmen weiterhin automatisiert geprüft werden. Zur Analyse des PNZ wird vorgeschlagen, der Untersuchung mit Hilfe des Evolutionsgraphen eine benutzerinteraktive Analyse des diskreten Teils des PNZ mit reduzierter Variation der Eingangsstellen voranzustellen und damit die Variation der Ausgangsstellen festzulegen. Diese können wiederum verwendet werden, um ausgewählte Simulationen des kontinuierlichen Teils auf Plausibilität zu prüfen. Die Implementierung in Netlab erschließt dabei die Gegenrichtung der Toolkopplung. Wie Matlab zur hybriden Simulation Netlab bereits als Server aufruft, ruft Netlab zur Erstellung des Evolutionsgraphen Matiab als Server auf Erprobt wird diese Methodik des unterstützten Entwurfs an der Modellfabrik des Instituts für Regelungstechnik mittels OFC Ethernetanbindung. Im Rahmen zukünftiger Arbeiten sind zwei Aspekte als interessant zu bewerten: Für rein diskrete Systeme konnte der sinnvolle Einsatz eine hierarchischen Modellierung und Verifikation formal gezeigt werden. Aufgeworfene Fragen bezüglich einer Automation der Erstellung der abstrakten EXPORT- Komponenten, sowie Überlegungen zu Top-Down oder Bottom-Up Vorgehen bei der Modellierung mit hierachischem Ansatz sowie die Kopplung mit Steuerungssyntheseansätzen sollen in weiterer Zusammenarbeit mit Dr.-Ing. Julia Padberg geklärt werden, welche formale Aspekte mit Mitteln der theoretischen Informatik beleuchtet. Desweiteren sind Aktivitäten geplant, bei denen stochastische Ansätze mit Petri-Netzen gekoppelt werden sollen. Dabei soll unter anderem die Einschränkung der deterministischen Modellierung mit rein diskreten Petri-Netzen oder hybrider Petri-Netz-Zustandsräume möglichst aufgelöst und Unsicherheiten wie Komponentenausfall oder Messungenauigkeiten abgebildet werden.
Publications
- Netlab und Netlab Toolbox für Matlab/Simulink. In: Entwurf komplexer Automatisierungsysteme, Seiten 35-55, Braunschweig, Mm 2006. E. Schnieder
Orth, P., U. Küssel und D. Abel
- A Component-Based Verification Approach Based on Petri Net Components. In: Proceedings of the 6th Symposium FORMS/FORMAT, Juni 2007
Padberg, J . und U. Küssel
- Durchgängiger Entwurf diskreter Steuerungsprogramme mit Unterstützung durch formale Methode. Interner Forschungsbericht, Institut für Reglungstechnik, RWTH Aachen, 2008
Küssel, U.
- Hierarchical Modelling and Verification Based on Petri Net Components with Multiple Import Interfaces. In: Proceedings of the 17th IFAC World Congress, Juli 2008
Küssel, U., J. Padberg und D. Abel
