A5 | Softwaretechnik und formale Analyse
In einem modellbasierten Entwicklungsprozess wurde in enger Zusammenarbeit mit den Software entwickelnden Teilprojekten die speziell auf die Anforderungen von Parallelkinematiken zugeschnittene Softwarearchitektur PROSA-X entwickelt. Es entstanden detaillierte UML-Modelle der Architektur und des Verhaltens der verschiedenen PROSA-X-Module.
Bei der werkzeuggestützten, formalen Verifikation der UML-Modelle wurden wesentliche Effizienzverbesserungen für den Anwendungsfall PC-basierte Steuerungen erzielt, indem spezifische Elemente des RTOS QNX bei der Modelltransformation von UML-Statecharts in Timed Automata, die Eingangssprache des Echtzeit-Modelcheckers UPPAAL, gezielt berücksichtigt werden. Zusätzlich wurde zur Verifikation des Echtzeitverhaltens die Schedulability der SW-Prozesse von PROSA-X mit dem UML-Profile for Schedulability, Performance and Time modelliert und werkzeuggestützt analysiert. Technisch wird die Analyse ebenfalls über eine Modelltransformation realisiert, die UML-Modelle mit geeigneten Werkzeugen zur Schedulability-Analyse verbindet. Des Weiteren wurde ein Werkzeug geschaffen das mit Hilfe des hybriden Modelcheckers HyTech eine formale Analyse von Aktionsprimitiv-Netzen ermöglicht, die komplexe Roboteraufgaben beschreiben.
Zur Unterstützung des Testens wurden unter Verwendung von Teilen der Werkzeugkette zur formalen Verifikation Testsuiten aus den Entwurfsmodellen erzeugt, die einerseits eine Reihe von Abdeckungen des Modells gewährleisten, aber auch Fehler spezieller aus dem Mutationstesten gewonnener Typen garantiert erkennen. Durch den Einsatz der speziell entwickelten Optimierungsheuristiken konnte die Ausführungszeit der generierten Testsuiten stark vermindert werden. Zudem wurde ein XML-Format für Testfälle spezifiziert, welches vom Analysewerkzeug des Teilprojekts B1 interpretiert wird, um durch die Ausführung der Testfälle das Verhalten von Systemkomponenten mit dem des Entwurfsmodells zu vergleichen. Zusätzlich wurden verschiedene Softwarewerkzeuge geschaffen, um Konfiguration und Betrieb der PROSA-X Teilkomponenten zu vereinfachen.
Für die effiziente Unterstützung der Softwarerentwicklung entstanden einige Werkzeuge auf Basis so genannter leichtgewichtiger Analysemethoden. So wurde beispielsweise eine Simulationsumgebung geschaffen, die wesentliche Mechanismen des Zielbetriebssystems QNX bereitstellt und in der Verhaltensmodelle der verschiedenen Steuerungskomponenten ausgeführt werden können. Es entstanden zusätzlich eine generische Oberfläche zur Beobachtung und Manipulation von PROSA-X-Komponenten zur Laufzeit sowie ein Werkzeug, das aus einem XML-Schema intelligente Eingabemasken für die Erstellung von Konfigurationsdateien des eingesetzten Echtzeitprotokolls erzeugt und so Fehler verhindert.
In Zukunft soll die bestehende Softwarearchitektur um Konzepte des Autonomic Computing erweitert werden, um durch verschiedene Aspekte des Self-Management den Betrieb und die Rekonfiguration von Parallelstrukturen zu vereinfachen.
Selbstkonfiguration soll Administration, Weiterentwicklung und Betrieb der komplexen Architektur vereinfachen. Durch Selbstoptimierungs- und Selbstheilungsmechanismen soll das System leistungsfähiger und sicherer werden. Es werden geeignete Modellierungsformalismen untersucht und erweitert, um Systeme mit autonom agierenden Komponenten zu beschreiben und wesentliche Eigenschaften über formale Analysen gewährleisten zu können. Das Teilprojekt A5 wird Techniken und Musterlösungen zur Integration von selbständig agierenden, optimierenden bzw. sich an wechselnde Anforderungen anpassende Komponenten entwickeln. Dazu werden Werkzeuge und Methoden bereitgestellt, die den Entwurf, die Realisierung sowie formale Analysen unterstützen. Bestehende Verhaltensmodelle der PROSA-X Komponenten werden angepasst und um zusätzliche Modelle für die autonome Entscheidungsfindung erweitert. So soll vor der Realisierung formal verifiziert werden, ob bestimmte Strategien einer autonomen Komponente tatsächlich der Optimierung übergeordneter Ziele zuträglich sind und ob wichtige funktionale und zeitkritische Eigenschaften weiterhin gewährleistet sind. Konkrete Realisierungen sind für den Steuerungskern, das Echtzeitprotokoll IAP sowie das erweiterte Analysewerkzeug von Teilprojekt B1 geplant.