The new address of Christophe Joubert's home page is:
All articles are available from the VASY (Validation of Systems) project website of INRIA Rhône-Alpes research unit (The French National Institute for Research in Computer Science and Control).
If you cannot find them, send me a mail and you'll be enlightened.
paper: (pdf) 2005
presentation: (pdf) 2005
(top)
paper: (pdf) 2005
presentation: (pdf) 2005
(top)
Boolean Equation Systems (BESs) allow to represent various problems encountered in the area of propositional logic programming and verification of concurrent systems. Several sequential algorithms for global and local BES resolution have been proposed so far, mainly in the field of verification; however, these algorithms do not scale up satisfactorily as the size of BESs increases. In this paper, we propose a distributed algorithm, called DSOLVE, which performs the local resolution of a BES using a set of machines connected by a network. Our experiments for solving large BESs using clusters of PCs show linear speedups and a scalable behaviour of DSOLVE w.r.t. its sequential counterpart.
paper: (pdf) 2003
presentation: (pdf) 2003
(top)
This paper describes a set of analysis components that open the way to perform performance and dependability analysis with the CADP toolbox, originally designed for verifying the functional correctness of LOTOS specifications. Three new tools (named BCG_STEADY, BCG_TRANSIENT, and DETERMINATOR) have been added to the toolbox. The approach taken fits well within the existing architecture of CADP, which doesn't need to be altered to enable performance evaluation.
paper: (pdf) 2004
presentation: (pdf) 2004
(top)
On-the-fly equivalence checking consists in comparing two Labeled Transition Systems (LTSs) modulo a given equivalence relation by exploring them in a demand-driven way. Since it avoids the explicit construction of LTSs, this method is able to detect errors even in systems that are too large to fit in the memory of a computer. In this paper, we aim at further improving the performance of on-the-fly equivalence checking using several machines connected by a network. We propose DSOLVE, a new algorithm for distributed on-the-fly resolution of Boolean Equation Systems (BESs), which enables equivalence checking modulo various relations characterized in terms of BESs. DSOLVE serves as verification engine for the distributed version of BISIMULATOR, an on-the-fly equivalence checker developed within the CADP verification toolbox using the OPENCAESAR environment. Our experimental measures show quasi-linear speedups and a good scalability of the distributed version of BISIMULATOR w.r.t. its sequential version.
paper: (pdf) 2003
presentation: (pdf) 2003
(top)
Distributed Model Checking (DMC) is based on several distributed algorithms, which are often complex and error prone. In this paper, we consider one fundamental aspect of DMC design: message passing communication, the implementation of which presents hidden tradeoffs often dismissed in DMC related literature. We show that, due to such communication models, high level abstract DMC algorithms might face implicit pitfalls when implemented concretely. We illustrate our discussion with a generic distributed state space generation algorithm.
(top)
This master research work aimed at designing and implementing new algorithms for the massively parallel generation of large transition systems problem, in order to prepare distributed model checking. We gave a complete state of the art of research works on parallel generation of models. Then, we proposed a new algorithm for the parallel construction of models obtained from programs described with high level languages, such as LOTOS. One novel aspect of our approach is the distributed management of dynamic data structures (lists, trees, etc.) between several machines. We also specified our algorithm in LOTOS and verified its functional properties (absence of deadlock, termination detection, safety) by mean of the CADP toolbox. A prototype implementation of our algorithm has been implemented in DISTRIBUTOR tool of CADP. The experiments on a cluster of PCs confirmed the good behavior of our algorithm and showed important performance gain in memory and time execution.
presentation: (pdf) 2004
(top)
presentation: (pdf) 2004
(top)
presentation: (pdf) 2003
(top)
presentation: (pdf) 2003
(top)
presentation: (pdf) 2002
(top)
presentation: (pdf) 2002
(top)
(top)
(top)