Thomas Hérault

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

By Thomas Hérault, Richard Lassaigne, Sylvain Peyronnet

2006-09-01

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.

Continue reading

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.

Continue reading

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. 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.

Continue reading

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.

Continue reading

Search

Tags