Thomas Hérault

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.

Evaluating complex MAC protocols for sensor networks with APMC

By Michaël Cadilhac, Thomas Hérault, Richard Lassaigne, Sylvain Peyronnet, Sébastien Tixeuil

2006-07-27

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.

Probabilistic verification of sensor networks

By Akim Demaille, Sylvain Peyronnet, Thomas Hérault

2006-02-01

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.

Distribution, approximation and probabilistic model checking

By Guillaume Guirado, Thomas Hérault, Richard Lassaigne, Sylvain Peyronnet

2005-05-23

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.

APMC 3.0: Approximate verification of discrete and continuous time Markov chains

Evaluating complex MAC protocols for sensor networks with APMC

Probabilistic verification of sensor networks

Distribution, approximation and probabilistic model checking

Search

Tags