Pervasive Services Verification Using Model Checking

Context-dependent information is a very important feature for pervasive services to enhance their flexibility and adaptability to changing conditions and dynamic environments. However, context-awareness capabilities in service interfaces introduce additional challenges to the software engineer, such as real-time requirements, a highly dynamic nature, quality of context information and automation. Thus, rigorous specification and verification of pervasive services design is highly desirable to ensure the correctness of such services against desired system properties. This paper proposes a novel, systematic, architecture-centric approach for specification and verification of pervasive services using model checking to assure the quality of pervasive services design. The approach is explored using a real-world case study in intelligent transport.