Practical application of probabilistic model checking to communication protocols
In Formal methods for industrial critical systems: A survey of applications
Abstract
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.
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.
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.
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.
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.
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.
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.