Filtern
Erscheinungsjahr
Dokumenttyp
- Monographie/Sammelband (31)
- Wissenschaftlicher Artikel (16)
- Sonstiges (5)
- Postprint (1)
Gehört zur Bibliographie
- ja (53)
Schlagworte
- cyber-physical systems (5)
- quantitative analysis (5)
- Modellierung (4)
- probabilistic timed systems (4)
- qualitative Analyse (4)
- qualitative analysis (4)
- quantitative Analyse (4)
- simulation (4)
- Graphtransformationen (3)
- Model Synchronisation (3)
- Model Transformation (3)
- Model-Driven Engineering (3)
- Tripel-Graph-Grammatik (3)
- Verifikation (3)
- graph transformation systems (3)
- performance (3)
- self-healing (3)
- verification (3)
- AUTOSAR (2)
- Bounded Model Checking (2)
- Cyber-Physical Systems (2)
- Evolution (2)
- Formale Verifikation (2)
- Forschungskolleg (2)
- Graphentransformationssysteme (2)
- Graphtransformationssysteme (2)
- HENSHIN (2)
- Hasso Plattner Institute (2)
- Hasso-Plattner-Institut (2)
- Klausurtagung (2)
- Model Synchronization (2)
- Modeling (2)
- Modellprüfung (2)
- PRISM model checker (2)
- PTCTL (2)
- Service-oriented Systems Engineering (2)
- SysML (2)
- Timed Automata (2)
- bounded model checking (2)
- code generation (2)
- cyber-physische Systeme (2)
- evaluation (2)
- feedback loops (2)
- graph constraints (2)
- graph transformation (2)
- hybrid systems (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)
- reconfigurable systems (2)
- timed automata (2)
- triple graph grammars (2)
- typed attributed graphs (2)
- Ausführung von Modellen (1)
- Behavioral equivalence and refinement (1)
- Bisimulation (1)
- Bisimulation and simulation (1)
- Bounded Backward Model Checking (1)
- Contracts (1)
- Cyber-Physical-Systeme (1)
- Cyber-physical-systems (1)
- Cyber-physikalische Systeme (1)
- Design (1)
- Discrimination Networks (1)
- Dynamic Data Structures (1)
- Echtzeitsysteme (1)
- Eingebettete Systeme (1)
- Empirical research (1)
- Evolution in MDE (1)
- Fallstudie (1)
- Feedback Loops (1)
- Flexible Resource Manager (1)
- Formal verification of behavior preservation (1)
- Generalized Discrimination Networks (1)
- Graph transformation (1)
- Graph transformations (1)
- Graph-Constraints (1)
- Graph-basierte Suche (1)
- Graphbedingungen (1)
- Graphdatenbanken (1)
- Infinite State (1)
- Inkrementelle Graphmustersuche (1)
- Interval Timed Automata (1)
- Invariant checking (1)
- Invariant-Checking (1)
- Invarianten (1)
- Invariants (1)
- Kausalität (1)
- Kollaborationen (1)
- Languages Model-driven engineering (1)
- Laufzeitmodelle (1)
- MDE Ansatz (1)
- MDE settings (1)
- Megamodell (1)
- Megamodels (1)
- Model Execution (1)
- Model-driven engineering (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)
- Ph.D. Retreat (1)
- Ph.D. retreat (1)
- Probabilistic timed automata (1)
- Quantitative Analysen (1)
- Realzeitsysteme (1)
- Relational model transformation (1)
- Research School (1)
- Runtime Binding (1)
- Runtime WCET Analysis (1)
- Runtime-monitoring (1)
- Safety Critical Systems (1)
- Savanne (1)
- Self-Adaptive Software (1)
- Self-aware computing systems (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)
- Software Engineering (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 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)
- adaptation rules (1)
- adaptive Systeme (1)
- adaptive systems (1)
- architecture-based adaptation (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)
- 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)
- evolution in MDE (1)
- failure model (1)
- failure profile (1)
- failure profile model (1)
- formal testing (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 conditions (1)
- graph databases (1)
- graph pattern matching (1)
- graph queries (1)
- graph transformations (1)
- hybrid graph-transformation-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)
- layered architecture (1)
- metric temporal graph logic (1)
- metric temporal logic (1)
- metric termporal graph logic (1)
- metrisch temporale Graph Logic (1)
- metrische Temporallogik (1)
- model interpreter (1)
- model transformation (1)
- model-driven engineering (1)
- modeling language (1)
- models at runtime (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)
- probabilistic timed automata (1)
- probabilistische zeitbehaftete Automaten (1)
- qualitative model (1)
- qualitatives Modell (1)
- relational model transformation (1)
- relationale Modelltransformationen (1)
- research school (1)
- reward (1)
- runtime monitoring (1)
- s/t-pattern sequences (1)
- savanna (1)
- scalability (1)
- search plan generation (1)
- self-adaptive software (1)
- semantics preservation (1)
- sequence properties (1)
- service-oriented systems (1)
- service-oriented systems engineering (1)
- simulator (1)
- software evolution (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)
- timed graph (1)
- trajectories (1)
- transformation (1)
- transformation level (1)
- transformation sequences (1)
- typed attributed symbolic graphs (1)
- typed graph transformation systems (1)
- typisierte attributierte Graphen (1)
- utility (1)
- verschachtelte Anwednungsbedingungen (1)
- verschachtelte Anwendungsbedingungen (1)
- view maintenance (1)
Advanced mechatronic systems have to integrate existing technologies from mechanical, electrical and software engineering. They must be able to adapt their structure and behavior at runtime by reconfiguration to react flexibly to changes in the environment. Therefore, a tight integration of structural and behavioral models of the different domains is required. This integration results in complex reconfigurable hybrid systems, the execution logic of which cannot be addressed directly with existing standard modeling, simulation, and code-generation techniques. We present in this paper how our component-based approach for reconfigurable mechatronic systems, MECHATRONIC UML, efficiently handles the complex interplay of discrete behavior and continuous behavior in a modular manner. In addition, its extension to even more flexible reconfiguration cases is presented.
Advanced mechatronic systems have to integrate existing technologies from mechanical, electrical and software engineering. They must be able to adapt their structure and behavior at runtime by reconfiguration to react flexibly to changes in the environment. Therefore, a tight integration of structural and behavioral models of the different domains is required. This integration results in complex reconfigurable hybrid systems, the execution logic of which cannot be addressed directly with existing standard modeling, simulation, and code-generation techniques. We present in this paper how our component-based approach for reconfigurable mechatronic systems, M ECHATRONIC UML, efficiently handles the complex interplay of discrete behavior and continuous behavior in a modular manner. In addition, its extension to even more flexible reconfiguration cases is presented.
The correctness of model transformations is a crucial element for model-driven engineering of high-quality software. In particular, behavior preservation is an important correctness property avoiding the introduction of semantic errors during the model-driven engineering process. Behavior preservation verification techniques show some kind of behavioral equivalence or refinement between source and target model of the transformation. Automatic tool support is available for verifying behavior preservation at the instance level, i.e., for a given source and target model specified by the model transformation. However, until now there is no sound and automatic verification approach available at the transformation level, i.e., for all source and target models. In this article, we extend our results presented in earlier work (Giese and Lambers, in: Ehrig et al (eds) Graph transformations, Springer, Berlin, 2012) and outline a new transformation-level approach for the sound and automatic verification of behavior preservation captured by bisimulation resp.simulation for outplace model transformations specified by triple graph grammars and semantic definitions given by graph transformation rules. In particular, we first show how behavior preservation can be modeled in a symbolic manner at the transformation level and then describe that transformation-level verification of behavior preservation can be reduced to invariant checking of suitable conditions for graph transformations. We demonstrate that the resulting checking problem can be addressed by our own invariant checker for an example of a transformation between sequence charts and communicating automata.
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.
The correctness of model transformations is a crucial element for 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 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 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. While 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 and runtime checks can be employed to guarantee these criteria.
The analysis of behavioral models is of high importance for cyber-physical systems, as the systems often encompass complex behavior based on e.g. concurrent components with mutual exclusion or probabilistic failures on demand. The rule-based formalism of probabilistic timed graph transformation systems is a suitable choice when the models representing states of the system can be understood as graphs and timed and probabilistic behavior is important. However, model checking PTGTSs is limited to systems with rather small state spaces.
We present an approach for the analysis of large scale systems modeled as probabilistic timed graph transformation systems by systematically decomposing their state spaces into manageable fragments. To obtain qualitative and quantitative analysis results for a large scale system, we verify that results obtained for its fragments serve as overapproximations for the corresponding results of the large scale system. Hence, our approach allows for the detection of violations of qualitative and quantitative safety properties for the large scale system under analysis. We consider a running example in which we model shuttles driving on tracks of a large scale topology and for which we verify that shuttles never collide and are unlikely to execute emergency brakes. In our evaluation, we apply an implementation of our approach to the running example.
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.
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 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.
In the world of model-driven engineering (MDE) support for traceability and maintenance of traceability information is essential. On the one hand, classical traceability approaches for MDE address this need by supporting automated creation of traceability information on the model element level. On the other hand, global model management approaches manually capture traceability information on the model level. However, there is currently no approach that supports comprehensive traceability, comprising traceability information on both levels, and efficient maintenance of traceability information, which requires a high-degree of automation and scalability. In this article, we present a comprehensive traceability approach that combines classical traceability approaches for MDE and global model management in form of dynamic hierarchical mega models. We further integrate efficient maintenance of traceability information based on top of dynamic hierarchical mega models. The proposed approach is further outlined by using an industrial case study and by presenting an implementation of the concepts in form of a prototype.