Quantitative Verifikation von verteilten Systemen

verteilte, reaktive und eingebettete Systeme. Allerdings sind diese
Systeme allgegenwaertigen stochastischen Einfluessen ausgesetzt
(Ausfall von Komponenten, Ressourcenkonflikte, Signalstoerungen
etc.). Daher sind absolute Korrektheitsaussagen allzu oft
unrealistisch. Stattdessen muss die Analyse solcher Systeme es
erlauben, Korrektheitsaussagen mit quantifizierbarer Unsicherheit zu
validieren.


Dieser Vortrag befasst sich mit Konzepten und Werkzeugen, welche die
Korrektheit, Leistungsfaehigkeit und Zuverlaessigkeit verteilter
Systeme quantifizierbar machen. Dies wird auf der Basis von modernen,
hochsprachlichen Spezifikationen geschehen. Solch ein Vorgehen birgt
das Potential, die derzeit bestehende Kluft zwischen klassischer
Leistungsbewertung und formalen Verifikationstechniken zu schliessen,
und zwar in einem Anwendungsfeld, in welchem fehlerhafte
Designentscheidungen sehr schnell sehr kostspielig werden koennen.


Konkret wird der Vortrag aufzeigen, dass sich einerseits Leistungs-
und Zuverlaessigkeitsmodelle aus hochsprachlichen Spezifikationen
ableiten lassen. Andererseits wird detailliert diskutiert, wie sich
automatisierte Verifikationstechniken ("Model Checking") auf solche
Modelle anwenden lassen, um -- neben Leistungs- und
Zuverlaessigkeitseigenschaften -- auch Korrekheitseigenschaften
quantifizieren zu koennen. Die Praktikabilitaet dieses Ansatzes wird
anhand prototypischer Softwarewerkzeuge demonstriert.