Model Checking Aspectual Pervasive Software Services

Abstract—Context-dependent information is tightly coupling or crosscutting the core functionality of a service at the service interface level. This results in a complex design, which is difficult to implement and maintain. The crosscutting context-dependent functionality of interacting pervasive services can be modeled as aspect-oriented models in UML. However, this has two challenges: the semi-formal nature of UML notations, and the expressive power of aspects. This paper explores model checking as a solution for modeling aspectual perva-sive software services and their compositions, and rigorously verifying the process behavior of these models against specified system properties. Model checking is applied, first to check the behavior of the individual pervasive aspects and components, and second to verify the overall behavior of the woven model even if no errors are found in the individual pervasive aspects and components. These verification stages have been used to gain confidence before the complex pervasive services are actually implemented. The approach is explored using a real-world case study in intelligent transport with more than 30 properties formalized to provide a comprehensive coverage of the system requirements. An evaluation framework has been established to validate the main methods and tools employed in the study. Keywords-pervasive services; model checking; aspect-oriented modeling; model-driven development; I