Studies on Verification of Wireless Sensor Networks and Abstraction Learning for System Inference

Faranak Heidarian Dehkordi

Promotor: Prof.dr. F.W. Vaandrager (RU)
Radboud Universiteit Nijmegen
Date: 5 July, 2012

Summary

Embedded systems are redefining how we perceive and interact with the physical world. While mission-critical embedded applications raise obvious reliability concerns, unexpected or premature failures in even noncritical applications such as game boxes and portable video players can erode a manufacturer’s reputation and greatly diminish acceptance of new devices. The design of reliable systems requires assuring that the system never moves through a dangerous state, and verification and validation (V & V) is the key. This dissertation approaches V & V of embedded systems from two different perspectives: in the first part, modeling and verification of a real-world case-study provided by the Chess eT International B.V. is described, whereas the second part investigates automata learning (automatic modeling of systems) using abstraction refinement.

In part one, the industrial case-study of Chess on wireless sensor networks is investigated. A wireless sensor network (WSN) is a collection of nodes organized into a cooperative network. Each node has a processing capability (one or more micro-controllers, CPUs or DSP chips), may contain multiple types of memory (program, data and flash memories), has a RF transceiver (usually with a single omnidirectional antenna), has a power source (e.g., batteries and solar cells), and accommodate various sensors and actuators. An effective protocol for wireless sensor networks must consume little power, avoid collisions, be implemented with a small code size and memory requirements, be efficient for a single application, and be tolerant to changing radio frequency and networking conditions.

Chess eT International B.V. has developed a WSN platform using a gossip (epidemic) communication model. In order to meet strict energy constraints, Chess used a Time Division Multiple Access (TDMA) protocol in which the nodes are active only in a limited period and for the remainder of the time, nodes switch to an energy saving mode. In the first part of this thesis, the model checker Uppaal is used for modeling and verification of two synchronization algorithms for wireless sensor networks. Indeed, Uppaal is used for extracting the error scenarios representing the situations where the network goes out of synch. The error scenarios are reproducible in reality. Based on such error scenarios, three conditions are introduced for a fully connected network to work correctly. The conditions are proved to be necessary and sufficient using invariant proof techniques. Isabelle/HOL supports the proofs.

Part two describes how counterexample-guided abstraction refinement(CEGAR) can be employed to infer models automatically through observations and test, that is, through black-box reverse engineering. State-of-the-art tools for active learning of state machines are able to learn state machines with at most in the order of 10.000 states. This is not enough for learning models of realistic software components which, due to the presence of program variables and data parameters in events, typically have much larger state spaces. Abstraction is the key when learning behavioral models of realistic systems. Hence, in most practical applications where automata learning is used to construct models of software components, researchers manually define abstractions which, depending on the history, map a large set of concrete events to a small set of abstract events that can be handled by automata learning tools. In the second part of this thesis, a full theory of abstraction for learning interface automata is presented. Moreover, it is shown how such abstractions can be constructed fully automatically for a class of extended finite state machines in which one can test for equality of data parameters, but no operations on data are allowed. This aim is reached through counterexample-guided abstraction refinement: whenever the current abstraction is too coarse and induces nondeterministic behavior in the learned model, the abstraction is refined automatically. Using a prototype implementation of the algorithm, models of several realistic software components, including the biometric passport and the SIP protocol were learned fully automatically.