Verification and Configuration of Smart Space Applications
Fuyuki Ishikawa, Shinichi Honiden · 2016
Smart space applications have a direct impact on human and social activities, which not only enhance attractive features but also increase the complexity of systems as well as demand for dependability. This chapter discusses the issues in tackling this challenge in smart space applications. Traditionally, model checking techniques have been considered effective for problems regarding various possibilities of state transitions, which include potential conflicts that come to the surface only in specific situations. The chapter discusses the conflicts in smart space applications and describes the proposed framework for verifying and configuring smart space applications. It focuses on event-driven control actions of smart spaces as one of the most essential features. The chapter considers a wider space of states including environments and users, as well as an instantiation as a model checking framework. It describes a case study that illustrates the use of the framework for verifying and debugging event condition action (ECA) rules.