Richard Lassaigne

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

By Jérôme Darbon, Richard Lassaigne, Sylvain Peyronnet

2006-07-27

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

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.

Uniform random sampling of traces in very large models

By Alain Denise, Marie-Claude Gaudel, Sandrine-Dominique Gouraud, Richard Lassaigne, Sylvain Peyronnet

2006-05-30

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 abstraction for model checking: An approach based on property testing

By Sophie Laplante, Richard Lassaigne, Frédéric Magniez, Sylvain Peyronnet, Michel de Rougemont

2005-11-21

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.

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.

Probabilistic verification and approximation

By Richard Lassaigne, Sylvain Peyronnet

2005-04-11

In Proceedings of 12th workshop on logic, language, information and computation (WoLLIC)

Abstract Model checking is an algorithmic method allowing to automatically verify if a system which is represented as a Kripke model satisfies a given specification. Specifications are usually expressed by formulas of temporal logic. The first objective of this paper is to give an overview of methods able to verify probabilistic systems. Models of such systems are labelled discrete time Markov chains and specifications are expressed in extensions of temporal logic by probabilistic operators.

Probabilistic model checking of the CSMA/CD, protocol using PRISM and APMC

By Marie Duflot, Laurent Fribourg, Thomas Herault, Richard Lassaigne, Frédéric Magniette, Stephane Messika, Sylvain Peyronnet, Claudine Picaronny

2004-09-01

In Proceedings of the 4th international workshop on automated verification of critical systems (AVoCS)

Abstract Carrier Sense Multiple Access/Collision Detection (CSMA/CD) is the protocol for carrier transmission access in Ethernet networks (international standard IEEE 802.3). On Ethernet, any Network Interface Card (NIC) can try to send a packet in a channel at any time. If another NIC tries to send a packet at the same time, a collision is said to occur and the packets are discarded. The CSMA/CD protocol was designed to avoid this problem, more precisely to allow a NIC to send its packet without collision.

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

Approximate probabilistic model checking for programs

Evaluating complex MAC protocols for sensor networks with APMC

Uniform random sampling of traces in very large models

Probabilistic abstraction for model checking: An approach based on property testing

Distribution, approximation and probabilistic model checking

Probabilistic verification and approximation

Probabilistic model checking of the CSMA/CD, protocol using PRISM and APMC

Search

Tags