Modellbasierte Verlässlichkeitsbewertungen sind anspruchsvoll und daher fehleranfällig, insbesondere wenn Formalismen niedriger Abstraktionsstufe wie Markovketten, Stochastische Petri-Netze oder Stochastische Prozessalgebren (SPA) genutzt werden. In der industriellen Anwendung finden daher häufig Spezifikationssprachen mit höherem Abstraktionsgrad wie AADL, UML oder SysML Verwendung. Diese sind jedoch zumeist weder formal definiert noch ermöglichen sie die Modellierung zufälliger Ereignisse, ein intrinsisches Merkmal verlässlicher Systeme. Die vorliegende Dissertation greift dieses Problem auf. Sie formalisiert die Syntax und Semantik der LAnguage for REconfigurable dependable Systems (LARES), die sich sowohl als eigenständige Modellierungssprache als auch als Zwischendarstellung nutzen lässt. LARES bietet Sprachmittel zur Modellierung von Hierarchien. Hierbei unterscheidet LARES zwischen Struktur und Verhalten und trägt durch Sichtbarkeitsbereiche (von Definitionen und referenzierbaren Ausdrücken) zur Strukturierung von Modellbeschreibungen bei. Die Semantik der Sprache wird mit Hilfe von SPA und beschrifteten Transitionssystemen (LTS) definiert. Dazu werden zwei Transformationen realisiert, die ein LARES Modell automatisch in dessen SPA Darstellung oder direkt in ein LTS überführen. Zudem erläutert diese Dissertationsschrift alle Implementierungen, die zusammen die LARES Modellierungsumgebung bilden: Die Editorkomponente hebt die Syntax visuell hervor, vervollständigt automatisch Ausdrücke und prüft Kontextbedingungen zur Gewährleistung der Modellvalidität. Die Analysekomponente transformiert die Modelle und visualisiert den erzeugten Instanzbaum, den Zustandsraum oder die berechneten Verlässlichkeitsmaße. Die Bibliothekskomponente beinhaltet unter anderem Sprachdefinitionen, Parser, Transformationen und Anbindungen an externe Analysewerkzeuge. Beide Transformationen können auf ihre Korrektheit geprüft werden, da sich die erzeugten SPA- und LTS-Modelle hinsichtlich ihres Verhaltens entsprechen müssen. Des Weiteren wird ein Beweis skizziert, der die Äquivalenz dieser Transformationen zeigt. Mehrere Anwendungsbeispiele, unter anderem ein aktives Dämpfungssystem eines autonomen RailCab-Fahrzeugs, bestätigen die ausreichende Ausdrucksmächtigkeit. Sie dienen auch dazu, Metriken über die jeweilige LARES Spezifikation, die temporäre SPA Darstellung sowie die symbolische Kodierung während der Analyse zu bestimmen. Die Metriken geben Hinweis darauf, wie der LARES-Ansatz skaliert, abhängig von den genutzten Sprachkonstrukten zur Abbildung der kombinatorischen Komplexität der Modelle. Die Dissertation vergleicht und grenzt LARES gegenüber verwandten Ansätzen ab und schließt mit einigen Ideen über zukünftige Erweiterungs- und Verbesserungsmöglichkeiten.    «

Modellbasierte Verlässlichkeitsbewertungen sind anspruchsvoll und daher fehleranfällig, insbesondere wenn Formalismen niedriger Abstraktionsstufe wie Markovketten, Stochastische Petri-Netze oder Stochastische Prozessalgebren (SPA) genutzt werden. In der industriellen Anwendung finden daher häufig Spezifikationssprachen mit höherem Abstraktionsgrad wie AADL, UML oder SysML Verwendung. Diese sind jedoch zumeist weder formal definiert noch ermöglichen sie die Modellierung zufälliger Ereignisse, ein...    »