Model Checking Aspectual Pervasive Software Services

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 pervasive 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.