Engineering Reactive Systems

A Compositional and Model-Driven Method Based on Collaborative Building Blocks

Frank Alexander Kraemer

Ph.D. Thesis, Norwegian University of Science and Technology, August 2008.

PDF available here

Abstract. This thesis introduces SPACE, an engineering method for reactive systems which enables the rapid composition of services from reusable building blocks. In contrast to traditional approaches which often focus on reuse of separate system components, we use collaborations as the main specification units and building blocks. Collaborations are distributed, stateful functions related to a certain task. They span across several components and describe both the local behavior of all participating components as well as the necessary interactions in an explicit form. We express collaborations by a combination of UML 2.0 collaborations and activities. To encapsulate their internals, we use a special form of UML state machines to describe their externally visible behavior, so that building blocks can be composed without understanding inner details. This opens up new possibilities for the reuse of specifications, since solutions to specific tasks that incorporate several components can be encapsulated within self-contained building blocks. We describe how collaborative building blocks can be composed by means of UML activities. There may be arbitrary composition levels, and development may follow a top-down or bottom-up approach. In the end, a complete system specification is obtained. To implement this specification, we have developed an automated model transformation that synthesizes executable state machines from the collaborations, which are implemented by code generation.

As a semantic foundation to reason about the correctness of our approach, we use temporal logic, and in particular the compositional Temporal Logic of Actions, cTLA. Since we formalize collaborations as cTLA processes which are composed by joint actions, the property of superposition holds for them. This means that properties of a collaborative building block are also maintained by a system composed from it. This makes the incremental verification of systems possible: during the analysis of a collaboration composed from others, we only use the abstract external description of the sub-collaborations. This reduces the state space during model checking, and we only need to check one composition level at a time, that is, each collaboration separately. In addition, since we also formalized the executable state machines for the execution, the model transformation from collaborations to components corresponds to a formal refinement step, so that the correctness of the transformation is ensured as well.

The method is supported by a set of tools. Besides the quick composition of systems in a drag-and-drop like manner, the tools create the state machines and provide the automated analysis of collaborations and their composition on the basis of incremental model checking.

Part I - Introduction and Overview

The chapters of part II are available within the original PDF file or as individual web pages, linked in the following.

Part II - Included Publications

Part III - Appendices

  1. Tool Support for the Rapid Composition, Analysis and Implementation of Reactive Services
    This article has been published in an extended version at the Elsevier Journal of Systems and Software in 2009.
  2. Refinement Proof
  3. UML Profile for Service Engineering
  4. Building Blocks and Patterns for UML Collaborations and Activities
  5. UML Profile for Executable State Machines

PDF available here

@phdthesis{Krae:PHD08,
  Author = {Frank Alexander Kraemer},
  Month = {August},
  School = {Norwegian University of Science and Technology},
  Title = {Engineering Reactive Systems: 
A Compositional and Model-Driven Method Based on Collaborative Building Blocks},
  Year = {2008}}