• search hit 10 of 33
Back to Result List

Cyber-physical systems with dynamic structure : towards modeling and verification of inductive invariants

  • Cyber-physical systems achieve sophisticated system behavior exploring the tight interconnection of physical coupling present in classical engineering systems and information technology based coupling. A particular challenging case are systems where these cyber-physical systems are formed ad hoc according to the specific local topology, the available networking capabilities, and the goals and constraints of the subsystems captured by the information processing part. In this paper we present a formalism that permits to model the sketched class of cyber-physical systems. The ad hoc formation of tightly coupled subsystems of arbitrary size are specified using a UML-based graph transformation system approach. Differential equations are employed to define the resulting tightly coupled behavior. Together, both form hybrid graph transformation systems where the graph transformation rules define the discrete steps where the topology or modes may change, while the differential equations capture the continuous behavior in between such discreteCyber-physical systems achieve sophisticated system behavior exploring the tight interconnection of physical coupling present in classical engineering systems and information technology based coupling. A particular challenging case are systems where these cyber-physical systems are formed ad hoc according to the specific local topology, the available networking capabilities, and the goals and constraints of the subsystems captured by the information processing part. In this paper we present a formalism that permits to model the sketched class of cyber-physical systems. The ad hoc formation of tightly coupled subsystems of arbitrary size are specified using a UML-based graph transformation system approach. Differential equations are employed to define the resulting tightly coupled behavior. Together, both form hybrid graph transformation systems where the graph transformation rules define the discrete steps where the topology or modes may change, while the differential equations capture the continuous behavior in between such discrete changes. In addition, we demonstrate that automated analysis techniques known for timed graph transformation systems for inductive invariants can be extended to also cover the hybrid case for an expressive case of hybrid models where the formed tightly coupled subsystems are restricted to smaller local networks.show moreshow less
  • Cyber-physical Systeme erzielen ihr ausgefeiltes Systemverhalten durch die enge Verschränkung von physikalischer Kopplung, wie sie in Systemen der klassichen Igenieurs-Disziplinen vorkommt, und der Kopplung durch Informationstechnologie. Eine besondere Herausforderung stellen in diesem Zusammenhang Systeme dar, die durch die spontane Vernetzung einzelner Cyber-Physical-Systeme entsprechend der lokalen, topologischen Gegebenheiten, verfügbarer Netzwerkfähigkeiten und der Anforderungen und Beschränkungen der Teilsysteme, die durch den informationsverabeitenden Teil vorgegeben sind, entstehen. In diesem Bericht stellen wir einen Formalismus vor, der die Modellierung der eingangs skizzierten Systeme erlaubt. Ein auf UML aufbauender Graph-Transformations-Ansatz wird genutzt, um die spontane Bildung eng kooperierender Teilsysteme beliebiger Größe zu spezifizieren. Differentialgleichungen beschreiben das kombinierte Verhalten auf physikalischer Ebene. In Kombination ergeben diese beiden Formalismen hybride Graph-Transformations-Systeme, inCyber-physical Systeme erzielen ihr ausgefeiltes Systemverhalten durch die enge Verschränkung von physikalischer Kopplung, wie sie in Systemen der klassichen Igenieurs-Disziplinen vorkommt, und der Kopplung durch Informationstechnologie. Eine besondere Herausforderung stellen in diesem Zusammenhang Systeme dar, die durch die spontane Vernetzung einzelner Cyber-Physical-Systeme entsprechend der lokalen, topologischen Gegebenheiten, verfügbarer Netzwerkfähigkeiten und der Anforderungen und Beschränkungen der Teilsysteme, die durch den informationsverabeitenden Teil vorgegeben sind, entstehen. In diesem Bericht stellen wir einen Formalismus vor, der die Modellierung der eingangs skizzierten Systeme erlaubt. Ein auf UML aufbauender Graph-Transformations-Ansatz wird genutzt, um die spontane Bildung eng kooperierender Teilsysteme beliebiger Größe zu spezifizieren. Differentialgleichungen beschreiben das kombinierte Verhalten auf physikalischer Ebene. In Kombination ergeben diese beiden Formalismen hybride Graph-Transformations-Systeme, in denen die Graph-Transformationen diskrete Schritte und die Differentialgleichungen das kontinuierliche, physikalische Verhalten des Systems beschreiben. Zusätzlich, präsentieren wir die Erweiterung einer automatischen Analysetechnik zur Verifikation induktiver Invarianten, die bereits für zeitbehaftete Systeme bekannt ist, auf den ausdrucksstärkeren Fall der hybriden Modelle.show moreshow less

Download full text files

Export metadata

Additional Services

Share in Twitter Search Google Scholar Statistics
Metadaten
Author:Basil Becker, Holger GieseORCiDGND
URN:urn:nbn:de:kobv:517-opus-62437
ISBN:978-3-86956-217-9
Series (Serial Number):Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam (64)
Publisher:Universitätsverlag Potsdam
Place of publication:Potsdam
Document Type:Monograph/Edited Volume
Language:English
Year of Completion:2012
Publishing Institution:Universität Potsdam
Release Date:2012/12/21
Tag:Cyber-Physical-Systeme; Modellierung; Verifikation; hybride Graph-Transformations-Systeme
Cyber-physical-systems; hybrid graph-transformation-systems; modeling; verification
Pagenumber:iv, 27
RVK - Regensburg Classification:ST 230
Organizational units:An-Institute / Hasso-Plattner-Institut für Digital Engineering gGmbH
Dewey Decimal Classification:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
Publication Way:Universitätsverlag Potsdam
Licence (German):License LogoKeine Nutzungslizenz vergeben - es gilt das deutsche Urheberrecht
Notes extern:
In Printform erschienen im Universitätsverlag Potsdam:

Cyber-physical systems with dynamic structure : towards modeling and verification of inductive invariants / Basil Becker ; Holger Giese. - Potdam : Universitätsverlag Potsdam, 2012. - iv, 27 S : Ill., graph. Darst.
(Technische Berichte des Hasso-Plattner-Instituts für Softwaresystemtechnik an der Universität Potsdam ; 64)
ISSN (print) 1613-5652
ISSN (online) 2191-1665
ISBN 978-3-86956-217-9
--> bestellen