Foothill Project: Model-checking for Ubiquity

Marta Kwiatkowska

Wireless sensor networks and body sensor networks already exist, or are planned, for many purposes. Such systems must deal with continuous streams of data, analogue and digital, ans must be adaptive, fault-tolerant, dependable, context-aware and energy efficient. Above all, especially in a safety-critical situation, they must work correctly; for example, a failure to identify a dangerous pattern during heart-monitoring may lead to patient death.

Model checking is an automatic technique that can establish, via exhaustive analysis of the model of a system, whether its behaviour is correct with respect to a given specification. It relies on logics or calculi that define the state space; hence its development must be closely linked to those logics and calculi. These themselves have to be developed, as part of the theoretical goal of the challenge.

Following major successes in detecting genuine errors in standardised protocols, model checking techniques are now widely used in industry, e.g. for hardware verification at Intel and source code compliance checking at Microsoft. However, sensor networks raise new scientific challenges:

• Sensor networks are dynamic, adaptive and context-aware. What model checking techniques are appropriate for these infinite-state systems?
• Sensor networks are often decentralised, communication failures are frequent, and techniques such as randomisation are used for their coordination. Probabilistic model checking techniques are needed to accommodate these features.
• In a healthcare monitoring scenario patients are mobile, and this affects both power usage and reliability of communication. Stochastic models of social behaviours must be developed to analyse the effectiveness such systems.
• Monitoring scenarios involve streams of data, requiring fast analysis and response. How can we ensure the correctness of such responses?
• Quantitative model checking techniques are needed to predict the power usage of sensor networks over time and to select the best network configuration given some constraints.
• How can we ensure that the methods are scalable to realistic systems? Compositionality, abstraction and component-based techniques for ubiquity are needed.

Success in meeting these challenges will depend on working closely with designers of sensor networks, to gain an understanding of the key issues and to secure acceptance of the techniques. Some current projects are:

• Design, Implementation and Adaptation of Sensor Networks through Multi-dimensional Co-design
• NICTA funded programme (NICTA is National ICT Australia, Australia's new ICT Research Centre of Excellence).