DERty UML

Der modellbasierte Entwurf eingebetteter Systeme ist ein hochaktuelles Arbeitsgebiet in der Forschung und in der Industrie. Basierend auf den Prinzipien der Model Driven Architecture unterstützt der modellbasierte Entwurf Prinzipien der Wiederverwendung mit Hilfe von höheren Modellierungs- und Spezifikationssprachen. Diese ermöglichen die Beschreibung der Hauptaspekte eingebetteter Systeme auf höheren Abstraktionsebenen und realisieren gleichzeitig eine Entkopplung der Systemeigenschaften von der konkreten Implementierungsplattform. Die Unified Modeling Language (UML) ist eine solche Modellierungssprache.

Ein wichtiger Aspekt der Modellierung eingebetteter und elektronischer Systeme ist die domänen-spezifische Anpassung und Anwendung der UML. Zur Anwendung der UML auf dem Gebiet der Modellierung, Analyse und Synthese von Systems-on-Chip (SoC) initiierten wir 2004 zusammen mit den Cadence Berkeley Labs einen Workshop der Design Automation Conference, welcher 2006 zum dritten Mal erfolgreich durchgeführt wurde. Der Workshop etablierte sich mittlerweile als international anerkanntes Forum zur Anwendung der UML im Bereich der C/C++-basierten Modellierung elektronischer bzw. eingebetteter Systeme. Mittlerweile entwickelte sich hieraus ein eigenständiges Forschungsgebiet, um u.a. domänen-spezifische UML-Verfeinerungen, wie z.B. das UML-Profil für SoCs und die SysML (System Modelling Language) in die industrielle Anwendung zu bringen. Weitergehende Arbeiten auf diesem Gebiet finden in Kooperation mit 16 der führenden europäischen Halbleiterfirmen, wie z.B. ARM, Infineon, NXP und ST Microelectronics, im Rahmen des von der EU geförderten SPRINT (Open SoC Design Platform for Reuse and Integration of IPs) Projektes statt. Hier soll durch die UML eine gemeinsame Sicht zum IP-Management auf Basis von IEEE SystemC und SPIRIT IP-XACT realisiert werden.

Andere technischen Arbeiten auf diesem Gebiet konzentrierten sich in Kooperation mit der Fachgruppe von Prof. Engels (Insitut für Informatik) auf die Untersuchung von ausführbaren Spezifikationen auf der Grundlage von UML 2.0. Die Ausführbarkeit von UML wird erreicht, indem eine UML-Teilmenge um eine spezielle wohldefinierte Semantik und entsprechende Spezialisierungen der UML-Diagramme samt einer Action Language zur Beschreibung einzelner Aktionen in diesen Diagrammen erweitert wird. Unser Interesse konzentriert sich dabei besonders auf die Domäne der eingebetteten und elektronischen Systeme mit ihren spezifischen Anforderungen wie z.B. Echtzeitverhalten. Zur Spezifikation dieser Systeme verwenden wir auf Basis eines UML Profils neben Klassendiagrammen zur Strukturbeschreibung eine Kombination von Aktivitäten-, Sequenz- und StateMachine-Diagrammen zur Verhaltensbeschreibung. StateMachines wurden für diesen Anwendungsbereich noch um Basiskonzepte wie z.B. zur Definition von Interrupts erweitert und ermöglichen zudem die Spezifikation von Timeouts. Im Zuge dieser Arbeiten wird ferner untersucht, inwieweit sich Aktivitätendiagramme zur Beschreibung feingranularer Parallelität auf der Basis einer plattformunabhängigen Ausführung auf einer sog. UML Virtual Machine (UVM) verwenden lassen.

Detaillierte Informationen

Validierung und Verifikation

Ein weiterer Aspekt im Kontext des modellbasierten Entwurfs sind effiziente Validierungs- und Verifikationsmethoden, die eine möglichst vollständige Korrektheitsüberprüfung der modellierten eingebetteten Systeme auf unterschiedlichen Abstraktionsebenen unterstützen. In diesem Umfeld konzentrieren sich unsere Forschungsaktivitäten auf die systematische Anwendung verschiedener formaler Techniken zum Zweck der Spezifikation, der Systemmodellierung sowie der Verifikation. Ein Ziel ist die Integration dieser Techniken in den modellgetriebenen Entwicklungsprozess für komplexe eingebettete Systeme mit verteilter Steuerung, die Echtzeit- und Sicherheitsanforderungen erfüllen müssen. Die Hauptthemenumfassen ausführbare Spezifikationen, die Formalisierung von UML, eine Integration heterogener Modellierungsprachen auf semantischer Ebene sowie die Anwendung von Methoden zur Unterstützung vollautomatischer funktionaler Verifikation von verteilten Systemen unter Echtzeit- und Sicherheitsbedingungen. Die hier genannten Themen werden im Rahmen des vom BMBF geförderten Projekts IMMOS und innerhalb des Sonderforschungsbereich (SFB) 614 untersucht, wobei zum Einen Automobilelektronik und zum Anderen selbstoptimierende Multi-Agenten Systeme (MAS) mit mechatronischen Komponenten als Anwendungsgebiet betrachtet werden.

Systematisches Testen

In Kooperation mit DaimlerChrysler und dSPACE wurde ein einheitliches Austauschformat für modellbasierte Tests auf Basis von XML erarbeitet, das u.a. Unterstützung für zeitbehaftete Signalverläufe, wie sie in der Automobilelektronik auftreten, bietet. Diese sog. TestML ermöglicht die Integration verschiedenster Testwerkzeuge zur Erstellung von Testumgebungen, sowohl für Software-in-the-Loop (SIL), als auch für Hardware-in-the-Loop (HIL) Testverfahren. Weitere Arbeiten konzentrierten sich auf die Erweiterung der Klassifikationsbaummethode für eingebettete Systeme (CTM/ES) um zusätzliche Beschreibungsmöglichkeiten für Signalverläufe und Ereignisse (Events), sowie auf eine Erweiterung zur Spezifikation funktionaler Überdeckungskriterien. Diese Arbeiten wurden im Rahmen des IMMOS-Projekts umgesetzt und werden im Kontext des SFB 614 im Teilprojekt B3 fortgeführt.

Online Verifikation

In vielen Anwendungsdomänen wird die Anwendung formaler Spezifikations- und Verifikationstechniken in den Entwurfsphasen des Entwicklungsprozesses als ausreichend angesehen. Mechatronische Systeme, die z.B. in der Automobilindustrie eingesetzt werden, lassen sich jedoch zu selbstoptimierenden Systemen weiterentwickeln. Ein selbstoptimierendes System kann zur Laufzeit sein Verhalten ändern, indem es auf sichere und konsistente Weise dynamisch seine Komponenten verändert und austauscht. Der SFB 614 bearbeitet Ansätze zur Entwicklung derartig komplexer mechatronischer Systeme mit Eigenschaften der Selbstreflektion, Selbstadaption und Selbstoptimierung. Im Teilprojekt C2 des SFB 614 wird an selbstoptimierenden mechatronischen Echtzeitanwendungen mit hochdynamischen Software-Komponenten gearbeitet.

Die sichere und vorhersagbare Ausführung solcher Anwendungen erfordert neue Ansätze der Verifikation. Im Teilprojekt C2 wird daher eine neuartige Technik des Online-Model-Checking kontextspezifischer Laufzeitkomponenten umgesetzt. Diese Verifikationsmethode wird als Dienst des zugrundeliegenden Echtzeit-Betriebssystems (RTOS) zur Verfügung gestellt. Die nötige Echtzeitfähigkeit dieses Dienstes erfordert die Ausführung des Model-Checking zur Laufzeit auf UML-Modellebene. Zum Einsatz kommen hier RT-UML Modelle. Die zu prüfenden Eigenschaften liegen als RT-OCL vor, deren zugrundeliegende Temporallogik auf ACTL/LTL Formeln beschränkt ist. Als Verfahren wird ein erweitertes Bounded Model-Checking angewandt. Das Online Model-Checking wird über das RTOS als Zwischenschicht verzahnt mit der zu prüfenden Komponente ausgeführt. Dadurch können potentielle Fehlerzustände, z.B. durch eine Rekonfiguration zur Laufzeit, vorhergesagt werden und ermöglichen dem System mit minimalem Zeitverlust eine Rückfallstrategie zu einem sicheren Zustand.

zurück zur Übersicht