The work on the project progressed in two main strands: case studies, which guided the theoretical development and implementation of prototypes, and theoretical underpinning (models, property specifications, model checking algorithms) for a range of features typical in ad hoc network protocols and scenarios. Below we summarise the main achievements in relation to each of the stated project objectives.
Modelling formalisms for node mobility, dynamic environments and continuous state spaces have been developed. These substantially extend the capabilities of languages and models supported by PRISM.
Node Mobility.
The modelling of node mobility and network reconfigurability is central to any formal model of ad hoc network protocols, and the pi-calculus was identified in the proposal as the leading candidate. We have considered a probabilistic extension of the pi-calculus and, based on symbolic semantics and the Mobility Model Checker MMC, developed a model checking approach via translation into PRISM [NPPW07] (with Palamidessi and Wu).
Spatial Mobility.
A novel probabilistic extension of the mobile ambients formalism has been proposed, along with a corresponding spatial logic for property specifications [KNPV06]. This model combines the ability of ambients to represent dynamic, mobile systems, with support for probabilistic behaviour and nondeterminism, as required to accurately model failures and concurrency inherent in ad hoc networks. This work has opened up the possibility to apply such formalisms in modelling of biological systems, and is continuing in collaboration with Heath (Biosciences, Birmingham).
Continuous state spaces.
The modelling of geographical locations and movement calls for continuous system trajectories. In collaboration with Segala, a probabilistic model with continuous state spaces, general distributions and non-determinism has been studied that extends previous work. We identify the notion of measurability as fundamental for sound modelling of behaviours, without which the resulting models are intractable. In [CSKN05] the measurability issues are addressed for the first time, with the measurable behaviour also shown to be preserved under parallel composition.
Reward structures.
The logics supported by PRISM have been enhanced with support for costs/rewards and expectation operators. Two types of `instantaneous' properties (transient and long-run) and two types of `cumulative' properties (time-bound and reachability based) can be analysed. This permits expression and analysis of a wide range of quantitative performance metrics, for example, power consumption, retransmissions before a packet is successfully sent, link failures with a given interval of time and functioning routes at a particular time instance.
Model checking is known to suffer from state-space explosion, and our preliminary ad hoc network protocol case studies, such as on demand and probabilistic routing, have demonstrated that this problem is much more pronounced in the probabilistic context. The research therefore concentrated on developing scalable quantitative symbolic model checking algorithms and verification methodologies. The progress made in each of these areas was fundamental in meeting objective 3 (see below).
Probabilistic real-time model checking.
As identified in the proposal, real-time and probability are essential to model aspects such as timeouts and failures. Probabilistic timed automata arise naturally as models of a variety of ad hoc network protocols. This project contributed a symbolic framework, based on zones (polyhedra), for verifying probabilistic timed automata (PTAs) through backwards [KNSW04,KNSW07] and forwards reachability [DKN04,WK05]. The backwards method is the only practical algorithm for verifying PTAs against PTCTL (Probabilistic Timed Computation Tree Logic). The forwards method, although limited to estimating a subset of PTCTL, is based on simpler `zone operations', and therefore more efficient in practice.
For a large class of PTAs, we have also developed an approach using digital clocks, based on a translation to an equivalent finite-state representation [KNPS03,KNPS06]. This was the first solution for the computation of cost and reward based metrics for PTAs and is still the only technique available to calculate expected costs and rewards. The digital clocks approach enabled the direct application of PRISM to several ad hoc network protocols.
In collaboration with Pacheco, model checking for systems allowing general distributions has also been investigated and extended to cost and rewards [KNP06e].
Verification Methodologies.
A range of state-of-the-art methodologies for model reduction and approximate analysis were developed that, in conjunction with proof-style reasoning, enhance the scalability of probabilistic model checking.
Abstraction. A novel abstraction technique for probabilistic systems has been developed, based on a conversion to stochastic 2-player games, and its effectiveness demonstrated through a study of the Zeroconf ad hoc network protocol [KNP06b]. This represents a crucial component of a new research direction for Kwiatkowska's group (quantitative verification of software with predicate abstraction) supported by a new EPSRC grant (EP/D07956X).
Model reduction. A technique for model checking symmetric probabilistic systems was developed and a novel, symbolic implementation devised and applied to a P2P protocol [KNP06a]. Results were a significant increase in efficiency: near-factorial state space reductions and orders-of-magnitude decrease in solution time. In collaboration with Baier, Ciesinski and Groesser, techniques for partial order reduction were extended to cost and reward structures [GNB+06].
Assume-guarantee style reasoning. Promising recent work on algorithms for quantitative multi-objective optimisation in MDPs in collaboration with Etessami, Vardi and Yannakakis [EKVY07] provides a basis for a compositional analysis of probabilistic systems. This is to be pursued further.
Statistical probabilistic model checking. Statistical probabilistic model checking enables approximate measures to be calculated for large systems by applying hypothesis testing to discrete-event simulation traces. In collaboration with Younes, a comparative study with conventional, numerical solution based techniques (as implemented in PRISM) was carried out [YKNP04,YKNP06].
Distributed implementation. The research was aimed at improving scalability of analysis and focused on two distinct parallel architectures: small-scale, shared memory and PC clusters. Novel, symbolic techniques were developed with impressive speed-ups on a range of benchmarks [KPZM04,ZPK05a,ZPK05b].
Reward structures are included the public release of PRISM [HKNP06] and have been employed on many protocol case studies. A PRISM engine for discrete-event simulation has been developed [Hin05], adding approximate Monte-Carlo model checking capabilities. As a result, the use of is feasible on much larger models than for conventional, exact techniques. Additional tool enhancements for efficiency improvements and data structures were implemented [KPZM04,KNP04b]. These enhancements have been distributed in a free and open source fashion, with two major public releases (versions 2.0 and 3.0) of PRISM and corresponding tool papers [KNP04d,HKNP06].
In collaboration with Daws the symbolic forwards method for PTAs has been implemented using KRONOS and PRISM [DKN04], combining real-time and probabilistic model checking tools for the first time. More recently, the use of symbolic data structures to improve efficiency has also been investigated [Wan07].
Throughout the duration of the project, ad hoc network protocols have been used for benchmarking. Below we summarise the key case studies.
The device discovery protocol of the wireless communication standard Bluetooth was analysed in [DKNP04,DKNP06]. As the timing aspects use discrete clock `ticks', the protocol was modelled directly in PRISM and best and worst-case expected time and power consumption were calculated exactly for the first time. The verification of such a complex protocol (there are over 17,179,869,184 initial configurations) was a major undertaking and required a number of model-based reduction techniques.
Dynamic power management is vital in mobile devices due to limited battery life. In collaboration with Shukla and Gupta, probabilistic model checking is proposed as a framework for analysing dynamic power management strategies [NPK+05], allowing performance measures to be obtained without expensive simulations and, using [KNP06e], for non-Markovian arrivals, e.g. Pareto.
The collision avoidance mechanism of the IEEE 802.3 standard has been studied through a prototype implementation of symbolic model checking for PTAs [KNSW04,KNSW07]. The analysis was aimed at finding the best- and worst-case probability that a packet is successfully sent within a time bound in the case when two nodes initially collide. This has since been used to demonstrate the pros and cons of the statistical and numerical probabilistic model checking approaches [DKN+06], and as a benchmark in the development of the symmetry reduction techniques [KNP06a].
The ZeroConf dynamic configuration protocol of IPv4 has been analysed through the digital clocks approach [KNPS03,KNPS06]. Our experiments focused on how parameter variations influenced the probability of correct configuration and the time and cost of configuration. This was the first PTA case study employing cost and reward structures and has since demonstrated the utility of our abstraction technique [KNP06b].
The contention resolution protocol of the IEEE 802.11 wireless local area network standard case study was the first to employ both refinement and time-scale abstraction techniques in the analysis of PTAs [KNPS06]. Metrics including collision probabilities, probability of delivery before a time bound and expected power consumption were computed via PRISM and the digital clocks approach.
Two separately funded PhD theses contributed further important case studies to this project. The Ad hoc On-Demand Distance Vector Routing protocol (AODV) was studied in [CK05b] using UPPAAL and highlighted a dependency of the lifetime of routes on network size. Probabilistic routing for ad hoc networks has been investigated [LKC04,LKC05c,LKC06], resulting in a self-organising biologically-inspired routing algorithm with QoS provisioning via cross-layer optimisation. This protocol was studied using simulation with ns-2, adding to the breadth of the activities and informing the model checking research.
Additional case studies used to validate methods and prototypes include the contention protocol of the IEEE 1394 FireWire standard [DKN04,WK05], a peer-to-peer protocol based on Bit-Torrent [KNP06a], probabilistic contract signing protocols [NS06], fault-tolerant architectures [NPKS04,NPKS05], dynamic voltage scaling [KNP05c] and control systems [KNP04c,KNP06c].
The similarity between mobile ad hoc networks and biological networks (cellular or signalling) has given impetus to a new research direction, probabilistic model checking of biological systems, initiated during the lifetime of this project [HKN+06,KNP+06] and funded separately by Microsoft Research Cambridge and EPSRC Integrative Biology project.