With the proliferation of ubiquitous computing devices and mobile internet, it is envisaged that future pervasive services will be increasingly large-scale and operate at an inter-organizational level. Designing and implementing pervasive services will therefore become a more complex and challenging task. Signi cant interest exists within the pervasive computing community for representing pervasive services at di erent stages of the software life cycle. While most of these e orts have focused on the detailed design or implementation of pervasive services little work has been done at the software architectural level. In this research, we propose a novel approach based on behavioral modeling and analysis techniques for representing pervasive software services and their compositions and verifying the process behavior of these models against speci ed system properties. This systematic, architecture-centric approach combines the bene ts of principles such as UML, model transformation of Model Driven Architecture, and formal behavioral modeling and analysis techniques through model-checking, for engineering pervasive software services. In order to illustrate the validity and practical feasibility of the proposed approach we use an existing case study in transport and logistics. The approach will be evaluated to demonstrate the e ectiveness of model-checking as a technique for verifying pervasive software services.
Mark Weiser's vision of ubiquitous computing has been the impetus behind the
introduction of a new service-oriented computing paradigm known as pervasive
services or context-aware services. Ubiquitous environments facilitate the
collection of information from various data sources in order to aggregate the context
of entities, such as users, places or objects. The context obtained from these
sources can be used to automatically adapt a service's behavior or the content
it processes to the context of one or several parameters of a target entity in
a transparent way, resulting in pervasive services [
The use of models has been a popular approach for engineers when
constructing complex systems. Behavior modeling and analysis have been successfully used
by software engineers to uncover errors of concurrent and distributed systems at
design time. In this research, we propose a novel approach based on behavioral
modeling and analysis techniques for modeling pervasive software services and
their compositions and verifying the process behavior of these models against
speci ed system properties. This systematic, architecture-centric approach
combines the bene ts of principles such as UML, model transformation techniques of
Model Driven Architecture (MDA), and formal behavioral modeling and
analysis techniques using model-checking, for engineering pervasive services (research
objectives: Fig. 1a). Context-handling information is considered to be tightly
coupling or crosscutting the core functionality of a service at service interface
level [
Preliminary results of this research have been published in [
Previous approaches to the development of pervasive services have largely been
at the detailed design or implementation stages [
In this section, we provide an overview of the research methodology applied
for engineering pervasive software services. Next we present the model
transformation tool implemented using IBM Rational Software Architect, and further
research directions established on model veri cation and validation, as part of
the research methodology. The research approach is explored using a real-world
case study in intelligent tagging for transport and logistics called the ParcelCall
project [
The overall pervasive service-oriented development process is divided into
three main stages (Fig. 1b). First, using the case study subset, a service
speci cation for the system under consideration is de ned. For this purpose, the
relevant use cases for the case study subset are determined and the services
that realize the identi ed use cases are speci ed. The identi ed use cases and
their relationships are expressed using an UML use case diagram. As de ned
by Kruger et al. [
Second, the architecture for the system under consideration is de ned. To
this end, rst a component con guration that implements the extracted services
is de ned using an UML deployment diagram. The component con guration of
the approach is based on a distributed version of the Observer pattern called
the Event-Control-Action architecture pattern [
Third, the architecture model synthesized in the previous step is modularized
by applying separation of concerns. Context-handling information is considered
to be crosscutting the core functionality of a service at service interface level,
which results in a complex design that is hard to implement and maintain.
Therefore, a custom UML pro le is proposed from which a UML model template
and aspect-oriented models in UML (contextual-FSP or c-FSP aspects) [
The custom prototype tool has been built using the Java Emitter Templates
(JET) transformation authoring feature of IBM Rational Software Architect
(7.0) [
This section presents a discussion on the proposed future work of this research. For model veri cation (Fig. 2b), rst the generated FSP for the c-FSP aspects need to be woven with their base state machines using an explicit weaving mechanism. This can be modeled as the parallel composition of the aspectual and base state machines in FSP. Synchronization events can be introduced to control the coordination and weaving order between the base program and aspects. Concurrency and distributed notions will be added to the interacting pervasive software services and their compositions, such as shared objects, message passing and concurrent architectures. In addition, proper abstraction mechanisms need to be enforced on the models as part of preparation for veri cation. Formal modelchecking techniques provided by the LTSA, such as safety, progress and absence of deadlocks, will be used to verify the process behavior of the services against system properties speci ed to extensively cover the system requirements. The LTSA checks for property violations and if any violations are found it produces a trace to the violation known as a counterexample, which can be used to improve the state models or the system properties for the pervasive services. Validation of the models will be performed using the simulation and animation features of the LTSA. The research approach will be evaluated to demonstrate the e ectiveness of model-checking as a technique for verifying pervasive software service speci cations. Potential defects can be injected to the service speci cation and results can be compared with the defect free service speci cation. To summarize, the primary objective of this research is a systematic, architecturecentric approach for engineering pervasive services based on the principles of UML, model transformation techniques and formal model-checking. Building software architectural models of pervasive services provide engineers a better understanding of how these complex services inter-operate. Also, it helps to uncover any errors during the early stages of the software life cycle before the services are actually implemented, thus contributing to the Web services community. Future work involves model veri cation and validation as discussed previously.