Tool Support for the Rapid Composition, Analysis and Implementation of Reactive Services

Frank Alexander Kraemer, Vidar Slåtten, and Peter Herrmann

Journal of Systems and Software, Volume 82, Issue 12, December 2009, Pages 2068-2080, 2009.

Abstract. We present the integrated set of tools Arctis for the rapid development of reactive services. In our method, services are composed of collaborative building blocks that encapsulate behavioral patterns expressed as UML 2.0 collaborations and activities. Due to our underlying semantics in temporal logic, building blocks as well as their compositions can be transformed into formulas and model checked incrementally in order to guarantee that important system properties are kept. The process of model checking is fully automated. Error traces are presented to the users as easily understandable animations, so that no expertise in temporal logic is needed. In addition, the results of model checking are analyzed, so that in some cases automated diagnoses and fixes can be provided as well. The formal semantics also enables the correct, automatic synthesis of the activities to state machines which form the input of our code generators. Thus, the collaborative models can be fully automatically transformed into executable Java code. We present the development of a mobile treasure hunt system to exemplify the method and the tools.


An initial (and slightly shorter) version of this article was included in my Ph.D. thesis and is available here.

Author = {Frank Alexander Kraemer and Vidar Sl{\aa}tten and Peter Herrmann},
Journal = {Journal of Systems and Software},
Month = {December},
Number = {12},
Pages = {2068-2080},
Title = {{Tool Support for the Rapid Composition, Analysis and Implementation of Reactive Services}},
Volume = {82},
Year = {2009}}