Richard Lassaigne

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

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. Finally, we present experimental results that show the effectiveness of the approach applied to finding bugs in real programs.

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

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

Continue reading

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

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

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. The second objective is to focus on complexity of these methods and to answer the question: can probabilistic verification be efficiently approximated? In general, the answer is negative. However, in many applications, the specification formulas can be expressed in some positive fragment of linear time temporal logic. In this paper, we show how some simple randomized approximation algorithms can improve the efficiency of the verification of such probabilistic specifications.

Continue reading

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. This is done by way of a randomized exponential backoff process. In this paper, we analyse the correctness of the CSMA/CD protocol, using techniques from probabilistic model checking and approximate probabilistic model checking. The tools that we use are PRISM and APMC. Moreover, we provide a quantitative analysis of some CSMA/CD properties.

Continue reading

Search

Tags