Modellierung und Bewertung verlässlicher Systeme

Quelle: http://univis.uni-erlangen.de/formbot/dsc_3Danew_2Fresrep_view_26rprojs_3Dtech_2FIMMD_2FIMMD3_2Fberich_26dir_3Dtech_2FIMMD_2FIMMD3_26ref_3Dresrep

1. Simulative Auswertung von UML-Statecharts

Die Bewertung von Systemen bezüglich Fragen der Fehlertoleranz und Verlässlichkeit gewinnt heuzutage durch den steigenden Einsatz eingebetteter Systeme immer mehr an Bedeutung. Dabei ist es besonders wichtig, das System frühzeitig - basierend auf dem Systemmodell - zu analysieren und auszuwerten. Der Ausgangspunkt dabei sind UML-Modelle (UML-Statecharts). Die UML hat sich in den letzten Jahren als der De-Facto-Standard der Industrie etabliert und liegt mittlerweile in der Version 2.0 vor. Durch die vollständige Transformation der Statecharts in Stochastic-Reward-Nets wird es dem Modellierer ermöglicht, seine Modelle sowohl analytisch als auch simulativ auszuwerten. Dabei war es besonders wichtig, alle Modellelemente der UML-Statecharts zu berücksichtigen und nicht nur eine beschränkte Menge zu transformieren. Der Modellierer muss dadurch nicht auf bestimmte Konzepte verzichten, die evtl. nicht in Stochastic-Reward-Netze gemappt werden konnten.

Die größte Herausforderung bei der Transformation bestand darin, die Step-Semantik der UML-Statecharts in die Interleaving-Semantik der Stochastic-Reward-Nets zu überführen. In einem Statechart können mehrere Transitionen gleichzeitig (im gleichen Step) schalten. Im Petri-Netz dagegen schaltet immer nur eine Transition, auch wenn mehrere Transitionen aktiviert sind und schalten könnten. Dies würde bedeuten, dass das Petri-Netz in einen Zustand kommt, der im Statechart gar nicht möglich ist. Um dieses Problem zu lösen, mußten alle Transitionen im Statechart, die gleichzeitig schalten können, zu einer Transition im Petri-Netz verschmolzen werden. Dies ist zum Beispiel dann der Fall, wenn das gleiche Event mehrere Transitionen triggert. Bei Complition Transitionen - Transitionen die ohne Event getriggert werden und schalten können sobald der Eingangszustand der Transition betreten wird und alle evtl. vorkommenden Entry- und Exit-Events generiert werden - tritt diese Problematik nicht auf, da laut UML-Standard alle Complition Transitionen nacheinander schalten, was der Interleaving-Semantik des Petri Netzes entspricht. Desweiteren wurden Regeln über das Eventhandling aufgesetzt. Dieser Schritt war notwendig, da im UML-Standard nichts über die Reihenfolge der Generierung und Bearbeitung von Events ausgesagt wird.

Der Transformator generiert aus dem Modell, welches im XMI-Format vorliegt, das entsprechende Stochastic-Reward-Net. Die UML-Modelle können dabei mit unterschiedlichen CASE-Tools erstellt werden. Im Moment werden die Tools Poseidon/Gentleware, Innovator/MID und Rational Rose/IBM unterstützt. Weitere Tools können berücksichtigt werden sobald sie einen XML-Export des Systemmodells unterstützen. Da die ganze Tool-Kette auf einen vollständigen und standardkonformen XMI-Output angewiesen ist, wurde ein Tool-Framework erschaffen, welches aus dem teilweise lückenhaften und oft auch fehlerhaften XMI-Output der Tools in einen standardkonformen XMI-Output transformiert.

Der Simulator simuliert das Stochastic-Reward-Net und somit auch das komplette Statechart-Modell. Daraus können dann entsprechende Informationen über das System gewonnen werden. Desweiteren wurde ein Statechart-Simulator implementiert der die Statecharts des UML-Modells simuliert. Der Simulator erlaubt sowohl eine interaktive als auch automatisierte Abläufe der Simulation. Bei der Simulation muss vorgegeben werden ob das System über eine Event-Warteschlange (und die entsprechende Auswahl-Policy für die Events) oder einen Event-Wartepool. Die Simulationstraces können anschliessend analysiert werden. Dafür werden sie in eine SQL-Datenbank importiert. Die Anfragen werden in einer dafür definierten Sprache formuliert, in SQL-Statements transformiert und entsprechend weiterverarbeitet.

Eine analytische Auswertung des Modells ist unter der Voraussetzung möglich, dass der Zustandsraum nicht explodiert, was insbesondere bei komplexeren Modellen der Fall sein kann. Dies könnte durch eine Vereinfachung des Systemmodells evtl. umgangen werden, was meist zu trivialen Modellen führt. Deshalb ist in solchen Fällen die simulative Auswertung des kompletten Modells vorzuziehen. (K. Kosmidis)

2. Patterns und Szenarien in UML

Die Erarbeitung einer semantisch fundierten Darstellung von Patterns und Szenarien mittels der UML und von Verfahren zur Verifikation von Implementationen gegen solche Spezifikationen wurde fortgesetzt.

Zur Darstellung sowohl von Anforderungen an die Implementation eines Systems als auch von Patterns, die im Rahmen der Implementation eine Rolle spielen sollen, eignet sich aus dem Repertoire der Sprachelemente der UML besonders das der Kollaboration, das eine Menge von Objekten, die jeweils in bestimmten, konkreten Rollen auftreten, zueinander in Beziehung setzt und ihre zum erreichen bestimmter Ziele erforderlichen Interaktionen (Szenarien) als Sequenzen von ausgetauschten Nachrichten beschreibt. Für die Darstellung der Implementation des Systems dienen in erster Linie Klassendiagramme für die statische Struktur, sowie Zustandsdiagramme (State Charts) für die Verhaltensbeschreibung. Zwischen Systembeschreibung auf der einen und Szenarien auf der anderen Seite soll nun ein Abgleich realisiert werden, der sie auf Konsistenz prüft. Hierfür wurde eine Abbildung der erforderlichen UML-Elemente nach VHDL vorgeschlagen, die zum einen Klassen mit ihrem Verhalten widerspiegelt, zum anderen aus den Szenairen Testumgebungen generiert, die dann zur simulativen Überprüfung mittels gängiger VHDL-Simulationssysteme eingesetzt werden können. Die Entscheidung, ob es sinnvoll ist, eine vollständige, formale Verifikation durchzuführen, steht noch aus.

Die aus der Annäherung an VHDL folgende Hardwarenähe lässt es zudem wünschenswert erscheinen, sich künftig bei der Auffassung der UML in Richtung des UML-RT-Ansatzes zu orientieren, der eine bessere Integration von Hard- und Softwaremodellen ermöglicht. Dies spiegelt sich auch in der Gestaltung von UML-Profilen wider, die die Anbindung und Einbettung von Szenarien in Modelle für den Anwender erleichtern und durch geeignete Einschränkungen und Dokumentation dem Modellierer eine Orientierungsrichtlinie für den Patterneinsatz an die Hand geben sollen. (M. Sand)

3. Spezifikation von Systemen und Komponenten durch formale und semiformale Methoden

Die Arbeiten zum BMBF-geförderten Projekt "Intellectual Property Prinzipien für konfigurierbare Basisband SoCs in Internet-Protokoll-basierten Mobilfunknetzen (IP2)" (Ekompass-Förderschwerpunkt) wurden weitergeführt.

Das Projekt IP2 zielt auf neuartige EDA-Methoden und Produkte für zukünftige Generationen von Mobilfunksystemen. Arbeitsinhalte sind die Erforschung formaler Methoden zur Spezifikation protokollverarbeitender, reaktiver Systeme, neuartiger anwendungsspezifischer CAE-Methoden, wie angepasste Prinzipien des Intellectual Property und architekturgenaues Prototyping sowie ihre produktive Verwertung bei der Ausarbeitung und Optimierung neuartiger konfigurierbarer System-on-Chips (SoCs). Diese sollen in zukünftigen Internet Protokoll-basierten Mobilfunknetzen zum Einsatz kommen. Unterstützt werden sowohl existierende GSM-basierte Netzwerke und ihre GPRS-Derivate, als auch neue UMTS- und Hiperlan-basierte Lösungen, um mobile Datenraten von weit über 2 Mb/s zu erzielen. Dabei soll die Wettbewerbsfähigkeit durch das Setzen von Standards in diesem Bereich erfolgreich verbessert werden.

Ziel des Projekt-Arbeitspaketes 1, in dem Lucent Technologies, der Lehrstuhl für rechnergestützten Schaltungsentwurf und der Lehrstuhl 3 kooperieren, ist die Entwicklung einer formalen Spezifikationsmethodik speziell für reaktive Systeme. Das Leistungsvermögen formaler Spezifikationsverfahren hinsichtlich praktischer Anforderungen wurde analysiert und basierend auf Forschungen aus dem Bereich der Software Entwicklung wurde die existierende Notation SCR (Software Cost Reduction) zur Sprache ADeVA (Advanced Design and Verification of ASICs) erweitert, um asynchrones Verhalten auf Systemebene beschreiben zu können. Erste Ergebnisse wurden in Form einer Studie umgesetzt. Bei dieser Transformierung vorhandener, natürlich sprachiger Spezifikationen in eine formale Spezifikation ließen sich vielversprechende Ergebnisse zeigen, besonders hinsichtlich der Skalierbarkeit auf industrielle Designgrößen.

Mit der abstrakten Systemspezifikation als Basis wird die Verbindung zwischen formalen Methoden und simulationsbasierten Verfahren angestrebt in der Art, dass aus der formalen Spezifikation Simulationsstimuli und Verifikationspfade abgeleitet werden. Dies wird durch das Werkzeug Guwen geleistet, welches mittels Modellprüfung den Zustandsraum von ADeVA-Spezifikationen exploriert und dabei Testpfade bestimmt. Die Arbeiten an Guwen wurden 2003 begonnen und ergaben eine erste prototypische Version.

Projektübergreifend kooperiert IP2 mit dem Projekt VALSE-XT, ebenfalls aus dem Ekompass-Förderschwerpunkt, welches u.a. Schnittstellen zwischen der ADeVA Methodik und formaler Modellprüfung untersucht. Ziel ist es, Eigenschaftsprüfungen speziell für ASIC Komponenten auf Systemebene durchführen zu können. (S. Gossens, F. Wang)
	Projektleitung:
Prof. a.D. Dr. Dr. h.c. Mario Dal Cin

Beteiligte:
Dipl.-Inf. Stefan Gossens, Dipl.-Inf. Konstantinos Kosmidis, Dipl.-Inf. David Kreische, Dr.-Ing. Matthias Sand, F. Wang

Laufzeit: 1.1.2003 - 31.12.2004

Publikationen
Heinkel U. ; Mayer C. ; Pleickhardt J. ; Knäblein J. ; Sahm H. ; Webb C. ; Haas W. ; Gossens, Stefan: An Optimized Flow for Designing high-speed, large-scale CMOS ASIC SoCs . In: n.b. (Hrsg.) : Proc. SAMOS III Workshop: Systems, Architectures, MOdeling, and Simulation (SAMOS III Workshop: Systems, Architectures, MOdeling, and Simulation Samos, Greece July 2003). 2003, S. ..

Haas, W. ; Gossens, Stefan ; Heinkel, U.: Semantics of a Formal Specification Language for Advanced Design and Verification of ASICs (ADeVA) . In: n.b. (Hrsg.) : Proc. 11th E.I.S.-Workshop (11th E.I.S.-Workshop Erlangen April 2003). 2003, S. 51-56.

Heinkel U ; Mayer C. ; Pleickhardt J. ; Knäblein J. ; Sahm H. ; Webb C. ; Haas W. ; Gossens, Stefan: Specification, Design and Verification of Systems-on-Chip in a Telecom Application . In: n.b. (Hrsg.) : Proc. 11th E.I.S.-Workshop (11th E.I.S.-Workshop, Erlangen April 2003). 2003, S. 45-50.

Gossens, Stefan ; Dal Cin, Mario: Strukturelle Analyse explizit fehlertoleranter Programme . In: n.b. (Hrsg.) : Proc. 5th Workshop Software-Reengineering (5th Workshop Software-Reengineering Bad Honnef May 2003). 2003, S. ..

Sand, Matthias: Patterns for Model Verification . In: n.b. (Hrsg.) : Supplement to Proc. HASE 2005: International Symposium on High Assurance Systems Engineering (Ninth IEEE International Sympossium on High Assurance Systems Engineering Heidelberg, Germany 12-14. October 2005). 2005, S. 3-4.