Sven Schneider

Holger Giese

Maria Maximova

The analysis of behavioral models such as Graph Transformation Systems (GTSs) is of central importance in model-driven engineering. However, GTSs often result in intractably large or even infinite state spaces and may be equipped with multiple or even infinitely many start graphs. To mitigate these problems, static analysis techniques based on finite symbolic representations of sets of states or paths thereof have been devised. We focus on the technique of k-induction for establishing invariants specified using graph conditions. To this end, k-induction generates symbolic paths backwards from a symbolic state representing a violation of a candidate invariant to gather information on how that violation could have been reached possibly obtaining contradictions to assumed invariants. However, GTSs where multiple agents regularly perform actions independently from each other cannot be analyzed using this technique as of now as the independence among backward steps may prevent the gathering of relevant knowledge altogether. In this paper, we extend k-induction to GTSs with multiple agents thereby supporting a wide range of additional GTSs. As a running example, we consider an unbounded number of shuttles driving on a large-scale track topology, which adjust their velocity to speed limits to avoid derailing. As central contribution, we develop pruning techniques based on causality and independence among backward steps and verify that k-induction remains sound under this adaptation as well as terminates in cases where it did not terminate before.

Invariant Analysis for Multi-Agent Graph Transformation Systems using k-Induction

Stefan Neumann

The proper composition of independently developed components of an embedded real- time system is complicated due to the fact that besides the functional behavior also the non-functional properties and in particular the timing have to be compatible. Nowadays related compatibility problems have to be addressed in a cumbersome integration and configuration phase at the end of the development process, that in the worst case may fail. Therefore, a number of formal approaches have been developed, which try to guide the upfront decomposition of the embedded real-time system into components such that integration problems related to timing properties can be excluded and that suitable configurations can be found. However, the proposed solutions require a number of strong assumptions that can be hardly fulfilled or the required analysis does not scale well. In this paper, we present an approach based on timed automata that can provide the required guarantees for the later integration without strong assumptions, which are difficult to match in practice. The approach provides a modular reasoning scheme that permits to establish the required guarantees for the integration employing only local checks, which therefore also scales. It is also possible to determine potential configuration settings by means of timed game synthesis.

Scalable compatibility for embedded real-time components via language progressive timed automata

Edward A. Lee

Bernhard Rumpe

Gabor Karsai

Bernhard Schätz

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.

International Dagstuhl Workshop, Dagstuhl Castle, Germany, November 4-9, 2007. Revised Selected Papers

Model-Based Engineering of Embedded Real-Time Systems

Mary Shaw

Rogério de Lemos

Hausi A. Müller

Although the self-adaptability of systems has been studied in a wide range of disciplines, from biology to robotics, only recently has the software engineering community recognized its key role in enabling the development of self-adaptive systems that are able to adapt to internal faults, changing requirements, and evolving environments. The 15 carefully reviewed papers included in this state-of-the-art survey were presented at the International Seminar on "Software Engineering for Self-Adaptive Systems", held in Dagstuhl Castle, Germany, in October 2010. Continuing the course of the first book of the series on "Software Engineering for Self-Adaptive Systems" the collection of papers in this second volume comprises a research roadmap accompanied by four elaborating working group papers. Next there are two parts - with three papers each - entitled "Requirements and Policies" and "Design Issues"; part four of the book contains four papers covering a wide range of "Applications".

International Seminar Dagstuhl Castle, Germany, October 24-29, 2010 Revised Selected and Invited Papers

Software Engineering for Self-Adaptive Systems

Basil Becker

Modeling and Compositional Verification with Dynamic Collaborations

Correct Dynamic Service Oriented Architectures

Barbara König

This book constitutes the proceedings of the 7th International Conference on Graph Transformations, ICGT 2014, held in York, UK, in July 2014. The 17 papers and 1 invited paper presented were carefully reviewed and selected from numerous submissions. The papers are organized in topical sections on verification, meta-modelling and model transformations, rewriting and applications in biology, graph languages and graph transformation, and applications.

7th International Conference, ICGT 2014, Held as Part of STAF 2014, York, UK, July 22-24, 2014, Proceedings

Graph Transformation

Holger Giese

About

Books

Join the club