Applying model checking to pervasive computing systems

Abstract:

Pervasive computing systems are `aware' of and self-adaptive to its environment changes. Many successes have been achieved in laboratories especially for activity monitoring. However, such systems are not widely deployed due to, not only scalability and a lack of guarantees for correctness and reliability, but also the fact that those systems are designed for demonstration purpose with well controlled scenarios in a specific lab environment. Existing approaches such as software testing and simulation are laborious and not sufficient since only partial system behaviours are explored. Formal methods, especially model checking techniques are needed to model and reason the real environment. In this thesis, we propose to apply model checking techniques to systematically analyze pervasive computing systems.

First, a formal modelling framework is proposed with general modelling patterns for both the system design such as concurrent communications, context reasoning behaviours etc. and the environment including the human behaviours. Critical requirements concerned by stakeholders are specified as assertions which are verifiable against the system model. Secondly, we present a systematic rule anomaly detection approach. A tool is developed to automatically translate Drools Rules to CSP# modelling languages. Rule anomalies can then be detected automatically by reusing existing verification algorithms. Thirdly, MDP-based probabilistic model checking techniques are applied to perform reliability analysis. We target at three questions: 1) reliability prediction- "What is the overall reliability of the system based on known component reliability"; 2) reliability distribution- "To reach a certain overall system reliability, how reliable should the sensors/networks be?"; 3) sensitivity analysis- "Which node (could be a sensor or network device) has the most critical impact to the overall reliability?". Last but not the least, case studies on a real-world pervasive computing system AMUPADH, demonstrate the usefulness of our approaches. AMUPADH is designed for monitoring and assisting elderly with dementia to live independently and is deployed in a Singapore based nursing home. Existing model checkers such as PAT and RaPid are adopted for carrying out verification experiments. Unexpected bugs and system flaws are exposed which are confirmed by system engineers.