004 Datenverarbeitung; Informatik
Refine
Year of publication
Document Type
- Monograph/Edited Volume (30)
- Article (2)
- Postprint (1)
Is part of the Bibliography
- yes (33) (remove)
Keywords
- cyber-physical systems (5)
- quantitative analysis (5)
- Modellierung (4)
- probabilistic timed systems (4)
- qualitative Analyse (4)
- qualitative analysis (4)
- quantitative Analyse (4)
- Graphtransformationen (3)
- Model Synchronisation (3)
- Model Transformation (3)
- Tripel-Graph-Grammatik (3)
- Verifikation (3)
- graph transformation systems (3)
- simulation (3)
- verification (3)
- AUTOSAR (2)
- Bounded Model Checking (2)
- Formale Verifikation (2)
- Forschungskolleg (2)
- Graphentransformationssysteme (2)
- Graphtransformationssysteme (2)
- Hasso Plattner Institute (2)
- Hasso-Plattner-Institut (2)
- Klausurtagung (2)
- Model Synchronization (2)
- Model-Driven Engineering (2)
- Modeling (2)
- Modellprüfung (2)
- Service-oriented Systems Engineering (2)
- SysML (2)
- Timed Automata (2)
- bounded model checking (2)
- cyber-physische Systeme (2)
- graph constraints (2)
- graph transformation (2)
- incremental graph pattern matching (2)
- k-inductive invariant checking (2)
- model checking (2)
- modeling (2)
- modellgetriebene Entwicklung (2)
- nested graph conditions (2)
- probabilistische gezeitete Systeme (2)
- probabilistische zeitgesteuerte Systeme (2)
- real-time systems (2)
- timed automata (2)
- triple graph grammars (2)
- typed attributed graphs (2)
- Ausführung von Modellen (1)
- Bisimulation (1)
- Bounded Backward Model Checking (1)
- Contracts (1)
- Cyber-Physical Systems (1)
- Cyber-Physical-Systeme (1)
- Cyber-physical-systems (1)
- Cyber-physikalische Systeme (1)
- Discrimination Networks (1)
- Echtzeitsysteme (1)
- Eingebettete Systeme (1)
- Evolution (1)
- Evolution in MDE (1)
- Fallstudie (1)
- Feedback Loops (1)
- Generalized Discrimination Networks (1)
- Graph-Constraints (1)
- Graph-basierte Suche (1)
- Graphbedingungen (1)
- Graphdatenbanken (1)
- HENSHIN (1)
- Infinite State (1)
- Inkrementelle Graphmustersuche (1)
- Interval Timed Automata (1)
- Invariant-Checking (1)
- Invarianten (1)
- Invariants (1)
- Kausalität (1)
- Kollaborationen (1)
- Laufzeitmodelle (1)
- MDE Ansatz (1)
- MDE settings (1)
- Megamodell (1)
- Megamodels (1)
- Model Execution (1)
- Modeling Languages (1)
- Modell-getriebene Softwareentwicklung (1)
- Modelle mit mehreren Versionen (1)
- Modellgetriebene Softwareentwicklung (1)
- Modellierungssprachen (1)
- Modelltransformationen (1)
- Models at Runtime (1)
- Nested Graph Conditions (1)
- PRISM Modell-Checker (1)
- PRISM model checker (1)
- PTCTL (1)
- Ph.D. Retreat (1)
- Ph.D. retreat (1)
- Quantitative Analysen (1)
- Realzeitsysteme (1)
- Research School (1)
- Runtime Binding (1)
- Runtime-monitoring (1)
- Savanne (1)
- Self-Adaptive Software (1)
- Sequenzeigenschaften (1)
- Sequenzen von s/t-Pattern (1)
- Service-Oriented Architecture (1)
- Service-Orientierte Architekturen (1)
- Service-orientierte Systme (1)
- Simulation (1)
- SoaML (1)
- Spezifikation von gezeiteten Graph Transformationen (1)
- System of Systems (1)
- Temporallogik (1)
- Trajektorien (1)
- Transformationsebene (1)
- Transformationssequenzen (1)
- Tripel-Graph-Grammatiken (1)
- Triple Graph Grammar (1)
- Triple Graph Grammars (1)
- Triple-Graph-Grammatiken (1)
- Unbegrenzter Zustandsraum (1)
- Verhaltensabstraktion (1)
- Verhaltensbewahrung (1)
- Verhaltensverfeinerung (1)
- Verhaltensäquivalenz (1)
- Verification (1)
- Wartung von Graphdatenbanksichten (1)
- Wüstenbildung (1)
- adaptive Systeme (1)
- adaptive systems (1)
- behavior preservation (1)
- behavioral abstraction (1)
- behavioral equivalenc (1)
- behavioral refinement (1)
- beschreibende Feldstudie (1)
- bisimulation (1)
- bounded backward model checking (1)
- case study (1)
- causality (1)
- code generation (1)
- collaboration (1)
- compositional analysis (1)
- cyber-physikalische Systeme (1)
- desertification (1)
- discrete-event model (1)
- discrimination networks (1)
- diskretes Ereignismodell (1)
- dynamic systems (1)
- dynamische Systeme (1)
- embedded-systems (1)
- evaluation (1)
- evolution in MDE (1)
- failure model (1)
- feedback loops (1)
- formal verification (1)
- formal verification methods (1)
- formale Verifikation (1)
- generalized discrimination networks (1)
- getypte Attributierte Graphen (1)
- global model management (1)
- globales Modellmanagement (1)
- graph databases (1)
- graph pattern matching (1)
- graph queries (1)
- graph transformations (1)
- hybrid graph-transformation-systems (1)
- hybrid systems (1)
- hybride Graph-Transformations-Systeme (1)
- inductive invariant checking (1)
- induktives Invariant Checking (1)
- inkrementelles Graph Pattern Matching (1)
- interval probabilistic timed systems (1)
- interval probabilistische zeitgesteuerte Systeme (1)
- interval timed automata (1)
- invariant checking (1)
- k-Induktion (1)
- k-induction (1)
- k-inductive invariants (1)
- k-induktive Invarianten (1)
- k-induktive Invariantenprüfung (1)
- k-induktives Invariant-Checking (1)
- kompositionale Analyse (1)
- metric temporal logic (1)
- metric termporal graph logic (1)
- metrisch temporale Graph Logic (1)
- metrische Temporallogik (1)
- model transformation (1)
- model-driven engineering (1)
- multi-version models (1)
- nested application conditions (1)
- parallel and sequential independence (1)
- parallele und Sequentielle Unabhängigkeit (1)
- partial application conditions (1)
- partielle Anwendungsbedingungen (1)
- performance (1)
- probabilistic timed automata (1)
- probabilistische zeitbehaftete Automaten (1)
- qualitative model (1)
- qualitatives Modell (1)
- reconfigurable systems (1)
- relational model transformation (1)
- relationale Modelltransformationen (1)
- research school (1)
- runtime monitoring (1)
- s/t-pattern sequences (1)
- savanna (1)
- search plan generation (1)
- self-healing (1)
- semantics preservation (1)
- sequence properties (1)
- service-oriented systems (1)
- service-oriented systems engineering (1)
- specification of timed graph transformations (1)
- static analysis (1)
- statische Analyse (1)
- symbolic analysis (1)
- symbolic graphs (1)
- symbolische Analyse (1)
- symbolische Graphen (1)
- system of systems (1)
- temporal logic (1)
- trajectories (1)
- transformation level (1)
- transformation sequences (1)
- typed graph transformation systems (1)
- typisierte attributierte Graphen (1)
- verschachtelte Anwednungsbedingungen (1)
- verschachtelte Anwendungsbedingungen (1)
- view maintenance (1)
The correctness of model transformations is a crucial element for the model-driven engineering of high quality software. A prerequisite to verify model transformations at the level of the model transformation specification is that an unambiguous formal semantics exists and that the employed implementation of the model transformation language adheres to this semantics. However, for existing relational model transformation approaches it is usually not really clear under which constraints particular implementations are really conform to the formal semantics. In this paper, we will bridge this gap for the formal semantics of triple graph grammars (TGG) and an existing efficient implementation. Whereas the formal semantics assumes backtracking and ignores non-determinism, practical implementations do not support backtracking, require rule sets that ensure determinism, and include further optimizations. Therefore, we capture how the considered TGG implementation realizes the transformation by means of operational rules, define required criteria and show conformance to the formal semantics if these criteria are fulfilled. We further outline how static analysis can be employed to guarantee these criteria.
Service-oriented modeling employs collaborations to capture the coordination of multiple roles in form of service contracts. In case of dynamic collaborations the roles may join and leave the collaboration at runtime and therefore complex structural dynamics can result, which makes it very hard to ensure their correct and safe operation. We present in this paper our approach for modeling and verifying such dynamic collaborations. Modeling is supported using a well-defined subset of UML class diagrams, behavioral rules for the structural dynamics, and UML state machines for the role behavior. To be also able to verify the resulting service-oriented systems, we extended our former results for the automated verification of systems with structural dynamics [7, 8] and developed a compositional reasoning scheme, which enables the reuse of verification results. We outline our approach using the example of autonomous vehicles that use such dynamic collaborations via ad-hoc networking to coordinate and optimize their joint behavior.
Model-driven software development requires techniques to consistently propagate modifications between different related models to realize its full potential. For large-scale models, efficiency is essential in this respect. In this paper, we present an improved model synchronization algorithm based on triple graph grammars that is highly efficient and, therefore, can also synchronize large-scale models sufficiently fast. We can show, that the overall algorithm has optimal complexity if it is dominating the rule matching and further present extensive measurements that show the efficiency of the presented model transformation and synchronization technique.