@misc{Giese2017,
  author    = {Giese, Holger},
  title     = {Formal models and analysis for self-adaptive cyber-physical systems},
  series = {Lecture notes in computer science},
  volume    = {10231},
  journal   = {Lecture notes in computer science},
  editor    = {Kouchnarenko, Olga and Khosravi, Ramtin},
  publisher = {Springer},
  address   = {Cham},
  isbn      = {978-3-319-57666-4},
  issn      = {0302-9743},
  doi       = {10.1007/978-3-319-57666-4_1},
  pages     = {3 -- 9},
  year      = {2017},
  abstract  = {In this extended abstract, we will analyze the current challenges for the envisioned Self-Adaptive CPS. In addition, we will outline our results to approach these challenges with SMARTSOS [10] a generic approach based on extensions of graph transformation systems employing open and adaptive collaborations and models at runtime for trustworthy self-adaptation, self-organization, and evolution of the individual systems and the system-of-systems level taking the independent development, operation, management, and evolution of these systems into account.},
  language  = {en}
}
@book{DyckGiese2017,
  author    = {Dyck, Johannes and Giese, Holger},
  title     = {k-Inductive invariant checking for graph transformation systems},
  number    = {119},
  publisher = {Universit{\"a}tsverlag Potsdam},
  address   = {Potsdam},
  isbn      = {978-3-86956-406-7},
  issn      = {1613-5652},
  url       = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus4-397044},
  publisher      = {Universit{\"a}t Potsdam},
  pages     = {45},
  year      = {2017},
  abstract  = {While offering significant expressive power, graph transformation systems often come with rather limited capabilities for automated analysis, particularly if systems with many possible initial graphs and large or infinite state spaces are concerned. One approach that tries to overcome these limitations is inductive invariant checking. However, the verification of inductive invariants often requires extensive knowledge about the system in question and faces the approach-inherent challenges of locality and lack of context. To address that, this report discusses k-inductive invariant checking for graph transformation systems as a generalization of inductive invariants. The additional context acquired by taking multiple (k) steps into account is the key difference to inductive invariant checking and is often enough to establish the desired invariants without requiring the iterative development of additional properties. To analyze possibly infinite systems in a finite fashion, we introduce a symbolic encoding for transformation traces using a restricted form of nested application conditions. As its central contribution, this report then presents a formal approach and algorithm to verify graph constraints as k-inductive invariants. We prove the approach's correctness and demonstrate its applicability by means of several examples evaluated with a prototypical implementation of our algorithm.},
  language  = {en}
}
@book{MaximovaGieseKrause2017,
  author    = {Maximova, Maria and Giese, Holger and Krause, Christian},
  title     = {Probabilistic timed graph transformation systems},
  number    = {118},
  publisher = {Universit{\"a}tsverlag Potsdam},
  address   = {Potsdam},
  isbn      = {978-3-86956-405-0},
  issn      = {1613-5652},
  url       = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus4-397055},
  publisher      = {Universit{\"a}t Potsdam},
  pages     = {34},
  year      = {2017},
  abstract  = {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 use the PRISM model checker to analyze PTGTS models with respect to PTCTL properties.},
  language  = {en}
}
@book{DyckGieseLambers2017,
  author    = {Dyck, Johannes and Giese, Holger and Lambers, Leen},
  title     = {Automatic verification of behavior preservation at the transformation level for relational model transformation},
  number    = {112},
  publisher = {Universit{\"a}tsverlag Potsdam},
  address   = {Potsdam},
  isbn      = {978-3-86956-391-6},
  issn      = {1613-5652},
  url       = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus4-100279},
  publisher      = {Universit{\"a}t Potsdam},
  pages     = {viii, 112},
  year      = {2017},
  abstract  = {The correctness of model transformations is a crucial element for model-driven engineering of high quality software. In particular, behavior preservation is the most important correctness property avoiding the introduction of semantic errors during the model-driven engineering process. Behavior preservation verification techniques either show that specific properties are preserved, or more generally and complex, they show some kind of behavioral equivalence or refinement between source and target model of the transformation. Both kinds of behavior preservation verification goals have been presented with automatic tool support for the instance level, i.e. for a given source and target model specified by the model transformation. However, up until now there is no automatic verification approach available at the transformation level, i.e. for all source and target models specified by the model transformation. In this report, we extend our results presented in [27] and outline a new sophisticated approach for the automatic verification of behavior preservation captured by bisimulation resp. simulation for model transformations specified by triple graph grammars and semantic definitions given by graph transformation rules. In particular, we show that the behavior preservation problem can be reduced to invariant checking for graph transformation and that the resulting checking problem can be addressed by our own invariant checker even for a complex example where a sequence chart is transformed into communicating automata. We further discuss today's limitations of invariant checking for graph transformation and motivate further lines of future work in this direction.},
  language  = {en}
}