Modellbasierte Analyse der Verlässlichkeit komplexer fehlertoleranter Systeme

• Antragsteller: Professor Dr. Arndt Bode; Professor Dr.-Ing. Markus Siegle
• Fachliche Zuordnung: Rechnerarchitektur, eingebettete und massiv parallele Systeme
• Förderung: Förderung von 2009 bis 2015
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 138712980

• Erstellungsjahr: 2014

Zusammenfassung der Projektergebnisse

Das Ziel dieses Forschungsprojektes war es, die Anwendbarkeit zustandsbasierter Modellierungsmethoden im Rahmen der quantitativen Bewertung fehlertoleranter Systeme zu verbessern und einem breiten Nutzerkreis zugänglich zu machen. Modelle diverser Anwendungsformalismen wie z.B. SystemC-TLM, SafeME oder AADL sollten über ein allgemeines mit Zuverlässigkeitsinformationen angereichertes Zwischenmodell in Zielformalismen überführt und schließlich analysiert werden. Die Ausdrucksstärke des Zwischenmodells sollte Modelle aus unterschiedlichen anwendungsspezifischen Beschreibungsformalismen fassen können und war somit eine wesentliche Herausforderung dieses Projekts. Zudem sollte durch das Zwischenmodell komplexes Fehlerverhalten beschreibbar sein, und die Modelle sollten komfortabel editierbar und automatisiert in formale Zielmodelle überführbar sein. Hierzu wurde die Sprache LARES zur Modellierung von rekonfigurierbaren, verlässlichen, diskreten Systemen entwickelt, die sowohl eigenständig als auch als Zwischendarstellung genutzt werden kann. Diese Sprache folgt objektorientierten Prinzipien und erlaubt die Abbildung von Hierarchien. Durch definierte Schnittstellen und Sichtbarkeitsbereiche der Komponenten und ihrer Attribute wird die Modularität der Komponenten gewährleistet. Ferner konnen Ereignisse durch spezifizierte Bedingungen ausgelöst und ein komplexes reaktives Verhalten erzielt werden. Sowohl Bedingungen als auch Reaktionen konnen hierbei über die Hierarchie hinweg und somit auf unterschiedlichen Granulationsebenen definiert werden. Die definierten Sprachmittel wurden im Laufe des Projekts mit zwei Semantiken hinterlegt. Zum einen durch eine Abbildung mit Mitteln der stochastischen Prozessalgebra CASPA (SPA), zum anderen durch flache beschriftete Transitionssysteme (LTS). Die LARES SPA-Semantik wurde hierbei so definiert, dass die LTS-Semantik der CASPA Prozessalgebra ein verhaltensäquivalentes Transitionssystem zur LARES LTS Semantik erzeugt. Da beide Semantiken durch Modelltransformationen implementiert wurden, konnte diese Äquivalenz anhand einer Reihe von Testmodellen untersucht und bestätigt werden. Diese Verhaltensaquivalenz konnte aber auch durch einen semi-formalen Beweis belegt werden. Die formale Definition von LARES durch die Diversifizierung mittels zweier Semantiken ermöglicht nicht nur die Anbindung von Prozessalgebra- und Markovkettenlöser, sondern auch automatisierte Regressionstests der definierten LARES Semantiken und ihrer fortschreitenden Implementierung. Die daraus resultierende robustere Implementierung erhöht zudem das Vertrauen in die Validität dieses Ansatzes. Die Nutzung moderner Entwicklungsmethoden, Programmiersprachen und Softwarepatterns erleichtert ferner die Wartbarkeit und künftige Weiterentwicklungen. Mit der Nutzung des “stackable trait pattern” durch die Scala Programmiersprache konnen Erweiterungen in Form neuer Sprachkonzepte und Transformationen in modularer Weise fur LARES eingeführt werden, ohne die Standardimplementation der LARES Bibliothek zu berühren. Ferner wurden modellgetriebene Softwareentwicklungstechniken (wie z.B. Eclipse EMF, Xtext, Graphiti und Epsilon) genutzt, um textuelle/graphische Editoren mit fortgeschrittenen Modellvalidierungslogiken zu implementieren. Das entstandene LARES IDE ist unter http://lares .w3.rz.unibw-muenchen.de zum Download verfügbar. Zusätzlich zu gebräuchlichen Maßen wie z.B. Zuverlässlichkeit oder Verfügbarkeit kommen auch Fragen bezüglich optimaler Schedules bestimmter Entscheidungen auf. Um diesen Aspekt abzubilden, wurden zwei Spracherweiterungen eingeführt. Diese umfassen nun Zustands- bzw. Transitionsrewards (reward extension) sowie nichtdeterministische Entscheidungen (decision extension).

Projektbezogene Publikationen (Auswahl)

• An Efficient Symbolic Elimination Algorithm for the Stochastic Process Algebra Tool CASPA. In M. Nielsen et al., editors, SOFSEM 2009: Theory and Practice of Computer Science, volume 5404 of Lecture Notes in Computer Science, pages 485–496. Springer, 2009
  J. Bachmann, M. Riedl, J. Schuster, and M. Siegle
  
• LARES - A Novel Approach for Describing System Reconfigurability in Dependability Models of Fault-Tolerant Systems. In C. Guedes Soares, R. Bri, and S. Martorell, editors, Reliability, Risk, and Safety: Theory and Applications. Proceedings of the European Safety and Reliability Conference (ESREL ’09), volume 1, pages 153–160. CRC Press, 2009
  A. Gouberman, M. Riedl, J. Schuster, M. Siegle, and M. Walter
  
• Dependability Model Transformation – A Stochastic Process Algebra Semantics for ZuverSicht Models. In B. Ale, I. Papazoglou, and E. Zio, editors, Reliability, Risk and Safety: Back to the Future. Proceedings of the European Safety and Reliability Conference (ESREL ’10), pages 932–940. CRC Press London, 2010
  M. Riedl, J. Schuster, M. Siegle, M. Blum, and F. Schiller
  
• Symbolic calculation of k-shortest paths and related measures with the stochastic process algebra tool CASPA. In Proc. of 1st Int. Workshop on Dynamic Aspects in Dependability Models for Fault-Tolerant Systems (DYADEM-FTS, in conjunction with EDCC 2010), pages 13–18. ACM, 2010
  M. Guenther, J. Schuster, and M. Siegle
  
• Considering dependent components in the terminal pair reliability problem. In DYADEM-FTS 2011, 415-422, 2011
  M. Lê and M. Walter
  
• Path-based calculation of MTTFF, MTTFR, and asymptotic unavailability with the stochastic process algebra tool CASPA. Proc. of the Institution of Mechanical Engineers, Part O: Journal of Risk and Reliability, 225(4):399–406, 2011
  J. Schuster and M. Siegle
  
• A LAnguage for REconfigurable dependable Systems: Semantics & Dependability Model Transformation. In Proceedings of the 6th International Workshop on Verification and Evaluation of Computer and Communication Systems (VECOS ’12), eWiC, pages 78–89. British Computer Society, August 2012
  M. Riedl and M. Siegle
  
• A Modelling and Analysis Environment for LARES. In J. B. Schmitt, editor, Measurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance, volume 7201 of Lecture Notes in Computer Science, pages 244–248. Springer, 2012
  A. Gouberman, M. Riedl, J. Schuster, and M. Siegle
  
• Bounds for Two-Terminal Network Reliability with Dependent Basic Events. In MMB’12/DFT’12 Proceedings of the 16th international GI/ITG conference on Measurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance, 31-45, 2012
  M. Lê and M. Walter
  
• A memory-efficient bounding algorithm for the two-terminal reliability problem. Electronic Notes in Theoretical Computer Science, 291:15–25, 2013
  M. Lê, M. Walter, and J. Weidendorfer
  
• Bewertung der Zuverlässigkeit selbstoptimierender Systeme mit dem LARES-Framework. In J. Gausemeier et al., editors, 9. Paderborner Workshop Entwurf Mechatronischer Systeme, HNI-Verlagsschriftenreihe, pages 161–174, Paderborn, 2013. Heinz-Nixdorf-Institut
  T. Meyer, C. Sondermann-Wölke, W. Sextro, M. Riedl, A. Gouberman, and M. Siegle
  
• A Specification Language for Reconfigurable Dependable Systems, its Formalisation and Analysis Environment. PhD thesis, Universität der Bundeswehr München, Neubiberg, Deutschland, July 2014
  M. Riedl
  
• An IDE for the LARES Toolset. In K. Fischbach and U. R. Krieger, editors, Measurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance, volume 8376 of Lecture Notes in Computer Science, pages 240–254. Springer International Publishing, 2014
  A. Gouberman, C. Grand, M. Riedl, and M. Siegle