Practical application of probabilistic model checking to communication protocols
In Formal methods for industrial critical systems: A survey of applications
Modeling of sensor networks using XRM
In Proceedings of the 2nd international symposium on leveraging applications of formal methods, verification and validation (ISoLA’06)
Abstract
Sensor networks are composed of small electronic devices that embed processors, sensors, batteries, memory and communication capabilities. One of the main goal in the design of such systems is the handling of the inherent complexity of the nodes, strengthened by the huge number of nodes in the network. For these reasons, it becomes very difficult to model and verify such systems. In this paper, we investigate the main characteristics of sensor nodes, discuss about the use of a language derived from Reactive Modules for their modeling and propose a language (and a tool set) that ease the modeling of this kind of systems.
APMC 3.0: Approximate verification of discrete and continuous time Markov chains
In Proceedings of QEST 2006
Abstract
In this paper, we give a brief overview of APMC (Approximate Probabilistic Model Checker). APMC is a model checker that implements approximate probabilistic verification of probabilistic systems. It is based on Monte-Carlo method and the theory of randomized approximation schemes and allows to verify extremely large models without explicitly representing the global transition system. To avoid the state-space explosion phenomenon, APMC gives an accurate approximation of the satisfaction probability of the property instead of the exact value, but using only a very small amount of memory. The version of APMC we present in this paper can now handle efficiently both discrete and continuous time probabilistic systems.
Approximate probabilistic model checking for programs
In Proceedings of the IEEE 2nd international conference on intelligent computer communication and processing (ICCP’06)
Abstract
In this paper we deal with the problem of applying model checking to real programs. We verify a program without constructing the whole transition system using a technique based on Monte-Carlo sampling, also called “approximate model checking”. This technique combines model checking and randomized approximation. Thus, it avoids the so called state space explosion phenomenon. We propose a prototype implementation that works directly on C source code. It means that, contrary to others approaches, we do not need to use a specific language nor specific data structures in order to describe the system we wish to verify. Finally, we present experimental results that show the effectiveness of the approach applied to finding bugs in real programs.
Evaluating complex MAC protocols for sensor networks with APMC
In Proceedings of the 6th international workshop on automated verification of critical systems (AVoCS)
Abstract
In this paper we present an analysis of a MAC (Medium Access Control) protocol for wireless sensor networks. The purpose of this protocol is to manage wireless media access by constructing a Time Division Media Access (TDMA) schedule. APMC (Approximate Probabilistic Model Checker) is a tool that uses approximation-based verification techniques in order to analyse the behavior of complex probabilistic systems. Using APMC, we approximately computed the probabilities of several properties of the MAC protocol being studied, thus giving some insights about its performance.
Uniform random sampling of traces in very large models
In Proceedings of the 1st international workshop on random testing 2006 (RT06)
Abstract
This paper presents some first results on how to perform uniform random walks (where every trace has the same probability to occur) in very large models. The models considered here are described in a succinct way as a set of communicating reactive modules. The method relies upon techniques for counting and drawing uniformly at random words in regular languages. Each module is considered as an automaton defining such a language. It is shown how it is possible to combine local uniform drawings of traces, and to obtain some global uniform random sampling, without construction of the global model.
Probabilistic verification of sensor networks
In Proceedings of the fourth international conference on computer sciences, research, innovation and vision for the future (RIVF’06)
Abstract
Sensor networks are networks consisting of miniature and low-cost systems with limited computation power and energy. Thanks to the low cost of the devices, one can spread a huge number of sensors into a given area to monitor, for example, physical change of the environment. Typical applications are in defense, environment, and design of ad-hoc networks areas. In this paper, we address the problem of verifying the correctness of such networks through a case study. We modelize a simple sensor network whose aim is to detect the apparition of an event in a bounded area (such as a fire in a forest). The behaviour of the network is probabilistic, so we use APMC, a tool that allows to approximately check the correctness of extremely large probabilistic systems, to verify it.
Probabilistic abstraction for model checking: An approach based on property testing
In ACM Transactions on Computational Logic
Abstract
The goal of model checking is to verify the correctness of a given program, on all its inputs. The main obstacle, in many cases, is the intractably large size of the program’s transition system. Property testing is a randomized method to verify whether some fixed property holds on individual inputs, by looking at a small random part of that input. We join the strengths of both approaches by introducing a new notion of probabilistic abstraction, and by extending the framework of model checking to include the use of these abstractions. Our abstractions map transition systems associated with large graphs to small transition systems associated with small random subgraphs. This reduces the original transition system to a family of small, even constant-size, transition systems. We prove that with high probability, “sufficiently” incorrect programs will be rejected ($\eps$-robustness). We also prove that under a certain condition (exactness), correct programs will never be rejected (soundness). Our work applies to programs for graph properties such as bipartiteness, $k$-colorability, or any $\exists\forall$ first order graph properties. Our main contribution is to show how to apply the ideas of property testing to syntactic programs for such properties. We give a concrete example of an abstraction for a program for bipartiteness. Finally, we show that the relaxation of the test alone does not yield transition systems small enough to use the standard model checking method. More specifically, we prove, using methods from communication complexity, that the OBDD size remains exponential for approximate bipartiteness.
A vectorial self-dual morphological filter based on total variation minimization
In Proceedings of the first international conference on visual computing
Abstract
We present a vectorial self dual morphological filter. Contrary to many methods, our approach does not require the use of an ordering on vectors. It relies on the minimization of the total variation with $L^1$ norm as data fidelity on each channel. We further constraint this minimization in order not to create new values. It is shown that this minimization yields a self-dual and contrast invariant filter. Although the above minimization is not a convex problem, we propose an algorithm which computes a global minimizer. This algorithm relies on minimum cost cut-based optimizations.
Distribution, approximation and probabilistic model checking
In Proceedings of the 4th international workshop on parallel and distributed model checking (PDMC)
Abstract
APMC is a model checker dedicated to the quantitative verification of fully probabilistic systems against LTL formulas. Using a Monte-Carlo method in order to efficiently approximate the verification of probabilistic specifications, it could be used naturally in a distributed framework. We present here the tool and his distribution scheme, together with extensive performance evaluation, showing the scalability of the method, even on clusters containing 500+ heterogeneous workstations.