Maria Maximova, Holger Giese, Christian Krause

• Today, software has become an intrinsic part of complex distributed embedded real-time systems. The next generation of embedded real-time systems will interconnect the today unconnected systems via complex software parts and the service-oriented paradigm. Therefore besides timed behavior and probabilistic behaviour also structure dynamics, where the architecture can be subject to changes at run-time, e.g. when dynamic binding of service end-points is employed or complex collaborations are established dynamically, is required. However, a modeling and analysis approach that combines all these necessary aspects does not exist so far. To fill the identified gap, we propose Probabilistic Timed Graph Transformation Systems (PTGTSs) as a high-level description language that supports all the necessary aspects of structure dynamics, timed behavior, and probabilistic behavior. We introduce the formal model of PTGTSs in this paper and present a mapping of models with finite state spaces to probabilistic timed automata (PTA) that allows to useToday, software has become an intrinsic part of complex distributed embedded real-time systems. The next generation of embedded real-time systems will interconnect the today unconnected systems via complex software parts and the service-oriented paradigm. Therefore besides timed behavior and probabilistic behaviour also structure dynamics, where the architecture can be subject to changes at run-time, e.g. when dynamic binding of service end-points is employed or complex collaborations are established dynamically, is required. However, a modeling and analysis approach that combines all these necessary aspects does not exist so far. To fill the identified gap, we propose Probabilistic Timed Graph Transformation Systems (PTGTSs) as a high-level description language that supports all the necessary aspects of structure dynamics, timed behavior, and probabilistic behavior. We introduce the formal model of PTGTSs in this paper and present a mapping of models with finite state spaces to probabilistic timed automata (PTA) that allows to use the PRISM model checker to analyze PTGTS models with respect to PTCTL properties.…
• Software gehört heutzutage zu einem wesentlichen Bestandteil von komplexen eingebetteten Echtzeitsystemen. Die nächste Generation von eingebetteten Echtzeitsystemen wird in der Zukunft die bisher nicht verbundenen Systeme durch komplexe Softwarelösungen unter der Verwendung des serviceorientierten Paradigmas verbinden. Deswegen wird neben der Beschreibung des zeitbehafteten und probabilistischen Verhaltens auch die Betrachtung der Strukturdynamik benötigt, um die Modellierung der Architekturänderungen während der Laufzeit zu ermöglichen, wie z. B. die dynamische Anbindung von den Endpunkten der Services oder die dynamische Erstellung der komplexen Kollaborationen. Allerdings gibt es noch keinen Ansatz für die Modellierung und Analyse, der all diese drei notwendigen Aspekte kombiniert. Um die identifizierte Lücke zu schließen, führen wir probabilistische zeitbehaftete Graphtransformationssysteme (kurz PTGTS) ein, die als abstrakte Beschreibungssprache dienen und die notwendigen Aspekte der Strukturdynamik, des zeitbehaftetenSoftware gehört heutzutage zu einem wesentlichen Bestandteil von komplexen eingebetteten Echtzeitsystemen. Die nächste Generation von eingebetteten Echtzeitsystemen wird in der Zukunft die bisher nicht verbundenen Systeme durch komplexe Softwarelösungen unter der Verwendung des serviceorientierten Paradigmas verbinden. Deswegen wird neben der Beschreibung des zeitbehafteten und probabilistischen Verhaltens auch die Betrachtung der Strukturdynamik benötigt, um die Modellierung der Architekturänderungen während der Laufzeit zu ermöglichen, wie z. B. die dynamische Anbindung von den Endpunkten der Services oder die dynamische Erstellung der komplexen Kollaborationen. Allerdings gibt es noch keinen Ansatz für die Modellierung und Analyse, der all diese drei notwendigen Aspekte kombiniert. Um die identifizierte Lücke zu schließen, führen wir probabilistische zeitbehaftete Graphtransformationssysteme (kurz PTGTS) ein, die als abstrakte Beschreibungssprache dienen und die notwendigen Aspekte der Strukturdynamik, des zeitbehafteten Verhaltens und des probabilistischen Verhaltens unterstützen. Außerdem stellen wir den Formalismus der probabilistischen zeitbehafteten Graphtransformationssysteme vor und definieren eine Abbildung zwischen den Modellen mit endlichen Zustandsräumen und probabilistischen zeitbehafteten Automaten, die die Nutzung des PRISM Modell-Checkers für die Analyse der PTGTS Modelle in Bezug auf PTCTL Eigenschaften ermöglichen.…