Probabilistic timed graph transformation systems
Probabilistische zeitbehaftete Graphtransformationssysteme
- 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.…
Author details: | Maria MaximovaORCiDGND, Holger GieseORCiDGND, Christian KrauseORCiDGND |
---|---|
URN: | urn:nbn:de:kobv:517-opus4-397055 |
ISBN: | 978-3-86956-405-0 |
ISSN: | 1613-5652 |
ISSN: | 2191-1665 |
Publication series (Volume number): | Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam (118) |
Publisher: | Universitätsverlag Potsdam |
Place of publishing: | Potsdam |
Publication type: | Monograph/Edited Volume |
Language: | English |
Date of first publication: | 2017/10/26 |
Publication year: | 2017 |
Publishing institution: | Universität Potsdam |
Publishing institution: | Universitätsverlag Potsdam |
Release date: | 2017/10/26 |
Tag: | Graphtransformationen; HENSHIN; PRISM Modell-Checker; PTCTL; probabilistische zeitbehaftete Automaten HENSHIN; PRISM model checker; PTCTL; graph transformations; probabilistic timed automata |
Issue: | 118 |
Number of pages: | 34 |
RVK - Regensburg classification: | ST 230 |
Organizational units: | An-Institute / Hasso-Plattner-Institut für Digital Engineering gGmbH |
DDC classification: | 0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik |
Publishing method: | Universitätsverlag Potsdam |
License (German): | Keine öffentliche Lizenz: Unter Urheberrechtsschutz |
External remark: | In Printform erschienen im Universitätsverlag Potsdam: Probabilistic timed graph transformation systems / Maria Maximova, Holger Giese, Christian Krause. – Potsdam: Universitätsverlag Potsdam, 2017. – 34 S. : Diagramme (Technische Berichte des Hasso-Plattner-Instituts für Softwaresystemtechnik an der Universität Potsdam ; 118) ISSN (print) 1613-5652 ISSN (online) 2191-1665 ISBN 978-3-86956-405-0 --> bestellen |