Transformations-Assisted Engineering of Pervasive Services

Context information is characterized by several qualities that make pervasive services challenging compared to conventional services, such as a highly dynamic nature, real-time requirements, quality of context information and automation. Thus, the additional complexities associated with pervasive services require special development technologies and validation methods. This paper discusses a novel approach based on model driven development and aspect-oriented modeling paradigms for representing complex crosscutting context-dependent functionality in service interfaces in a modular manner and automating the generation of state machine based adaptable behavior using model transformations to facilitate pervasive services engineering. Using model transformations we ensure the correct separation of concerns of the crosscutting context-dependent information at both UML modeling and formal behavioural specification levels. A custom prototype tool applying an effective pipeline of model-to-model and model-to-text transformations has been built and successfully applied to a real-world case study in intelligent transport. The generated context-dependent adaptable behavior and the core service behavior for the pervasive services are rigorously verified using formal model checking against desired system properties.