Holger Giese Bücher

Bei der Entwicklung komplexer technischer Systeme werden verschiedene Modellierungssprachen verwendet. Zum Beispiel werden bei der Entwicklung von Systemen in der Automobilindustrie bereits früh im Entwicklungsprozess Systemmodelle verwendet, um die Anforderungen und die grobe Struktur des Gesamtsystems darzustellen. Später werden Softwaremodelle verwendet, um die konkrete Softwarearchitektur zu modellieren. Jedes Modell stellt spezifische Entwurfsaspekte mit Hilfe passender Notationen auf einem angemessenen Abstraktionsniveau dar. Wenn jedoch vom Systementwurf zum Softwareentwurf übergegangen wird, müssen die Entwicklungsingenieure sicherstellen, dass alle Entwurfsentscheidungen, die im Systemmodell enthalten sind, korrekt auf das Softwaremodell übertragen werden. Sobald danach auch noch Änderungen auftreten, muss die Konsistenz zwischen den Modellen in einem aufwändigen manuellen Schritt wiederhergestellt werden. In diesem Bericht zeigen wir, wie Modellsynchronisation und Konsistenzregeln zur Automatisierung dieses Arbeitsschrittes verwendet und die Konsistenz zwischen den Modellen sichergestellt werden können. Außerdem stellen wir einen allgemeinen Ansatz zur Modellsynchronisation vor. Neben der reinen Synchronisation umfasst unsere Lösung weiterhin Tool-Adapter, sowie Konsistenzregeln, die sowohl die Teile der Modelle abdecken, die synchronisiert werden können, als auch die restlichen Teile. Der Modellsynchronisationsalgorithmus basiert auf Tripel-Graph-Grammatiken und wird im Detail erläutert. An Hand einer konkreten Transformation zwischen SysML- und AUTOSAR-Modellen, die im Rahmen eines Industrieprojektes entwickelt wurde, wird der Ansatz demonstriert. Im Anhang des Berichts sind alle TGG-Regeln für die SysML-zu-AUTOSAR-Transformation dokumentiert.

Thetopicof“Model-BasedEngineeringofReal-TimeEmbeddedSystems”brings together a challenging problem domain (real-time embedded systems) and a - lution domain (model-based engineering). It is also at the forefrontof integrated software and systems engineering, as software in this problem domain is an essential tool for system implementation and integration. Today, real-time - bedded software plays a crucial role in most advanced technical systems such as airplanes, mobile phones, and cars, and has become the main driver and - cilitator for innovation. Development, evolution, veri? cation, con? guration, and maintenance of embedded and distributed software nowadays are often serious challenges as drastic increases in complexity can be observed in practice. Model-based engineering in general, and model-based software development in particular, advocates the notion of using models throughout the development and life-cycle of an engineered system. Model-based software engineering re- forces this notion by promoting models not only as the tool of abstraction, but also as the tool for veri? cation, implementation, testing, and maintenance. The application of such model-based engineering techniques to embedded real-time systems appears to be a good candidate to tackle some of the problems arising in the problem domain.

Architecting critical systems has gained major importance in commercial, governmental, and industrial sectors. Emerging software applications encompass practicalities that are associated with either the whole system or some of its components. Therefore, effective methods, techniques, and tools for constructing, testing, analyzing, and evaluating the architectures for critical systems are of major importance. Furthermore, these methods, techniques, and tools must address issues of dependability and security, while focusing not only on the development, but also on the deployment and evolution of the architecture. This newly established ISARCS symposium provided an exclusive forum for exchanging views on the theory and practice for architecting critical systems. Such systems are characterized by the perceived severity of consequences that faults or attacks may cause, and architecting them requires appropriate means toassure that they will fulfill their specified services in a dependable and secure manner. The different attributes of dependability and security cannot be considered in isolation for today’s critical systems, as architecting critical systems essentially means finding the right trade-off among these attributes and the various other requirements imposed on the system. This symposium therefore brought together the four communities working on dependability, safety, security, and testing/analysis, each addressing to some extent the architecting of critical systems from their specific perspective. To this end, the symposium united the following three former events: the Workshop on Architecting Dependable Systems (WADS); the Workshop on the Role of Software Architecture for Testing and Analysis (ROSATEA); and the Workshop on Views on Designing Complex Architectures.

Verschiedene Arten von getypten attributierten Graphen werden verwendet, um Zustände von Systemen in unterschiedlichen Anwendungsbereichen zu beschreiben. Der etablierte Formalismus der Graphtransformationen bietet ein Modell, um Zustandssequenzen für dynamische Systeme zu definieren. Wir betrachten einen erweiterten Fall solcher Sequenzen, bei dem Zeit zwischen zwei Systemzuständen vergeht, und führen eine Logik ein, um diese Sequenzen zu beschreiben. Mit dieser Logik drücken wir Eigenschaften über die Struktur und Attribute von Zuständen aus und beschreiben temporale Vorkommen von Zuständen, die durch ihre innere Struktur verbunden sind. Diese Eigenschaften können bisher von keiner existierenden Logik auf Graphen vergleichbar dargestellt werden. Zunächst führen wir Graphen mit Änderungshistorie ein, indem wir jedes Graphelement mit einem Zeitstempel seiner Erzeugung und, falls nötig, seiner Löschung versehen. Dann definieren wir eine Logik auf Graphen, indem wir den Temporaloperator Until in die etablierte Logik der verschachtelten Graphbedingungen integrieren. Wir beweisen, dass unsere Logik gleich ausdrucksmächtig ist wie die Logik der verschachtelten Graphbedingungen, indem wir eine passende Reduktionsoperation definieren. Schließlich ermöglicht uns die Implementierung dieser Reduktionsoperation die werkzeukbasierte Analyse von metrisch-temporallogischen Eigenschaften für Zustandssequenzen.

Service-Orientierte Architekturen ermöglichen die dynamische Zusammensetzung und Rekonfiguration komplexer IT-Landschaften durch die Bindung von Service Contracts zur Laufzeit, das Starten neuer Komponenten und das Beenden veralteter. Die Evolution dieser Systeme umfasst nicht nur den Austausch von Komponenten-Implementierungen, sondern auch das Hinzufügen neuer Service-Contracts. Aktuelle Ansätze zur Modellierung und Verifikation unterstützen diese Eigenschaften oft nur unvollständig. In diesem Bericht präsentieren wir eine Erweiterung des OMG-Vorschlags zur Service-Modellierung mit UML - SoaML - die diese Einschränkungen beseitigt. Unser Ansatz ermöglicht die Modellierung von Service Contracts auf verschiedenen Abstraktionsniveaus und bietet eine fundierte formale Semantik für alle Modellierungskonzepte sowie die Verifikation kritischer Eigenschaften. Der kompositionale und inkrementelle Verifikationsansatz erlaubt die Überprüfung komplexer Eigenschaften, einschließlich Kommunikationsparameter und Zeit. Er deckt die dynamische Bindung von Service Contracts, den Austausch von Komponenten und die Evolution des Systems durch das Hinzufügen neuer Service Contracts ab. Die Modellierungs- und Verifikationsfähigkeiten unseres Ansatzes werden durch ein Beispiel aus dem Lieferkettenmanagement veranschaulicht.

This book constitutes the refereed proceedings of the 14th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2012, and the 32nd IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems, FORTE 2012, held in Stockholm, Sweden, in June 2012, as one of the DisCoTec 2012 events. The 16 revised full papers presented were carefully reviewed and selected from 42 submissions. They cover a wide range of topics combining theory and practice in application areas of telecommunication services, Internet, embedded and real-time systems, networking and communication security and reliability, sensor networks, service-oriented architecture, and Web services.

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.

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. Die Model-getriebene Softwareentwicklung benötigt Techniken zur Übertragung von Änderungen zwischen verschiedenen zusammenhängenden Modellen, um vollständig nutzbar zu sein. Bei großen Modellen spielt hier die Effizienz eine entscheidende Rolle. In diesem Bericht stellen wir einen verbesserten Modellsynchronisationsalgorithmus vor, der auf Tripel-Graph-Grammatiken basiert. Dieser arbeitet sehr effizient und kann auch sehr große Modelle schnell synchronisieren. Wir können zeigen, dass der Gesamtalgortihmus eine optimale Komplexität aufweist, sofern er die Ausführung dominiert. Die Effizient des Algorithmus' wird durch einige Benchmarkergebnisse belegt.

This book constitutes the thoroughly refereed post-workshop proceedings of 10 internationl workshops and 2 symposia held as satellite events of the 10th International Conference on Model Driven Engineering Languages and Systems, MoDELS 2007, in Nashville, TN, USA, in September/October 2007 (see LNCS 4735). The 29 revised full papers were carefully selected for inclusion in the book and are presented along with a doctoral and an educators' symposium section. The papers are organized in topical sections representing the various workshops: aspect-oriented modeling (AOM 2007), language engineering (ATEM2007), model driven development of advanced user interfaces (MDDAUI 2007), model size metrics (MSM 2007), model-based design of trustworthy health information systems (MOTHIS 2007), model-driven engineering, verification and validation (MoDeVVa 2007), modelling systems with OCL (Ocl4All 2007), Models@run. time, multi-paradigm modeling: concepts and tools (MPM 2007), quality in modeling, doctoral symposium, and educators' symposium.