Effiziente Verifikation von Performability-Eigenschaften verteilter Systeme
Zusammenfassung der Projektergebnisse
In diesem Projekt ging es um die automatische Überprüfung von quantitativen Anforderungen an verteilte Systeme, deren Verhalten mittels stochastischer Modelle beschrieben wird. Anwendungsgebiete sind verteilte Rechensysteme, vernetzte eingebettete Systeme (z.B. Sensornetze oder verteilte Fertigungssysteme), sowie verschiedenste Ausprägungen von Kommunikationssystemen. Quantitative Anforderungen sind (im Gegensatz zu rein funktionalen, qualitativen Anforderungen) solche, die sich auf quantifizierbare Größen wie Geschwindigkeit der Bearbeitung, Leistungsfähigkeit, Verlässlichkeit oder Energieverbrauch beziehen. Angesichts der zunehmenden Anforderungen an verteilte Systeme kommt der Bewertung und dem Nachweis solcher quantitativen Gesichtspunkte eine immer größere Bedeutung zu. Im Projekt "Effiziente Verifikation von Performability-Eigenschaften verteilter Systeme" wurde einerseits die Theorie der Verifikation mittels Model Checking durch die Entwicklung einer ausdrucksstarken temporalen Logik und zugehöriger effizienter Analyseverfahren, die auf symbolischen Datenstrukturen basieren, vorangetrieben. Andererseits wurde eine protoypische Implementierung eines entsprechenden Verifikations Werkzeugs (CASPA) erstellt, die die theoretischen Konzepte in ein praktisch nutzbares und nun allgemein verfügbares Werkzeug überführt. Derzeit und in der absehbaren Zukunft arbeiten wir an einer Weiterentwicklung der Methodik und an Verbesserungen unseres Werkzeugs CASPA. Bezüglich der numerischen Auswertung der dem Modell zugrundeliegenden Markovkette, die den rechenzeitintensivsten Anteil der Model Checking Algorithmen darstellt, sind wir mittlerweile durch die Entwicklung von symbolischen Multilevel-Verfahren um eine gutes Stück vorangekommen. Außerdem wurde durch die Erweiterung unserer Modellwelt um zeitlose Aktionen (zusätzlich zu Aktionen mit exponentiell verteilter Verzögerung) und durch die Entwicklung einer graphisch orientierten Modellierungsumgebung, die gemeinsam mit der ursprünglich rein textuellen Benutzerschnittstelle benutzt werden kann, die praktische Einsatzfähigkeit des Werkzeugs CASPA (auch durch Nicht-Experten) deutlich verbessert, so dass dieses mittlerweile auch von anderen Forschungsgruppen genutzt wird. Künftig planen wir, stochastische Prozessalgebren (und damit das Werkzeug CASPA) als Zielformalismus für aus Anwendungsformalismen wie AADL oder SystemC transformierte Verlässlichkeitsmodelle zu nutzen.
Projektbezogene Publikationen (Auswahl)
- A stochastic extension of the logic PDL. In: Sixth Int. Workshop on Performability Modeling of Computer and Communication Systems (PMCCS6), pages 58-61, Monticello, Illinois, 2003
M. Kuntz and M. Siegle
- CASPA: A performance evaluation tool based on stochastic process algebra and symbolic data structures. In: Tool Proc. of the 2003 Illinois Int. Multiconference on Measurement, Modelling, and Evaluation of Computer-Communication Systems, Tech. Report 781 / 2003 of the University of Dortmund, pages 19-21, 2003
M. Kuntz, M. Siegle, and E. Werner
- A Stochastic Extension of the Logic PDL. Technical report 2004/05, Universität der Bundeswehr München, Fakultät für Informatik, 2004
M. Kuntz and M. Siegle
- CASPA - A Tool for Symbolic Performance and Dependability Evaluation. In: Supplemental Volume to Proceedings of DSN'04, pages 90-91. IEEE Press, 2004
M. Kuntz, M. Siegle, and E. Werner
- Model Checking Actionand State-Labelled Markov Chains. In: Proc. of Int. Conf. on Dependable Systems and Networks (DSN), pages 701-710. IEEE Press, 2004
C. Baier, L. Cloth, B. Haverkort, M. Kuntz, and M. Siegle
- Performance Evaluation using multi-terminal binary decision diagrams. Proc. of the 12th GI/ITG Conf. on Measuring, Modelling and Evaluation of Computer and Communication Systems (MMB) together with the 3rd Polish-German Teletraffic Symposium (PCTS), Dresden, pages 179-184, VDE-Verlag, 2004.
E. Werner
- Symbolic Performance and Dependability Evaluation with the Tool CASPA. In: Proc. of First European Performance Engineering Workshop (FORTE'04 workshop), pages 293-307. Springer, LNCS 3236, 2004
M. Kuntz, M. Siegle, and E. Werner
- CASPA: Symbolic model checking of stochastic systems. In: Proc. of 13th GI/ITG Conference on Measuring, Modelling and Evaluation of Computer and Communication Systems (MMB), pages 469-472, Nürnberg, Germany, 2006. VDE Verlag
M. Kuntz and M. Siegle
- Symbolic Model Checking of Stochastic Systems: Theory and Implementation. In: A. Valmari, editor, Proc. of 13th Int. SPIN Workshop, pages 89-107. Springer, LNCS 3925, 2006
M. Kuntz and M. Siegle
- Symbolic Semantics and Verification of Stochastic Process Algebras. PhD thesis. University of Erlangen-Nürnberg, Technische Fakultät, 2006
M. Kuntz
- Verifying Finite State Machines in Probabilistic Environments. In: Proc. of 9th ITG/GI/CMM Workshop "Methoden zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV)", pages 248-254, 2006
M. Siegle
- Model Checking Markov Chains with Actions and State Labels. IEEE Transactions on Software Engineering, 33(4):209-224, 2007
C. Baier, L. Cloth, B. Haverkort, M. Kuntz, and M. Siegle
- Recent extensions to the stochastic process algebra tool CASPA. In: 5th International Conference on the Quantitative Evaluation of Sys Terns (QEST'08), pages 113-114. IEEE Computer Society, 2008
M. Riedl, J. Schuster, and M. Siegle
- Am Efficient Symbolic Elimination Algorithm for the Stochastic Process Algebra Tool CASPA. In: 35th Int. Conf. on Current Trends in Theory and Practice of Computer Science (SOFSEM'09), pages 485-496. Springer LNCS 5404, 2009
J. Bachmann, M. Riedl, J. Schuster, and M. Siegle
