joubert@lcc.uma.es
Last modification : 07/05/18 13:27:03
The new address of Christophe Joubert's home page is:
Most of the following 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) 2007
presentation: (pdf) 2007
(top)
The combination of static and dynamic software analysis, such as data flow analysis (DFA) and model checking, provides benefits for both disciplines. On the one hand, the information extracted by DFAs about program data may be utilized by model checkers to optimize the state space representation. On the other hand, the expressiveness of logic formulas allows us to consider model checkers as generic data flow analyzers. Following this second approach, we propose in this paper an algorithm to calculate DFAs using on-the-fly resolution of boolean equation systems (BESs). The overall framework includes the abstraction of the input program into an implicit labeled transition system (LTS), independent of the program specification language. Moreover, using BESs as an intermediate representation has allowed us to reformulate classic data flow analyses encountered in the literature, which were previously encoded in terms of mu-calculus formulas with forward and backward modalities. Our work has been implemented and integrated into the widespread verification platform CADP, and experimented on real examples.
paper: (pdf) 2006
presentation: (pdf) 2006
(top)
The well-known problem of state space explosion in model checking is even more critical when applying this technique to programming languages, mainly due to the presence of complex data structures. One recent and promising approach to deal with this problem is the construction of an abstract and correct representation of the global program state allowing to match visited states during program model exploration. In particular, one powerful method to implement abstract matching is to fill the state vector with a minimal amount of relevant variables for each program point. In this paper, we combine the on-the-fly model checking approach (incremental construction of the program state space) and the static analysis method called influence analysis (extraction of significant variables for each program point) in order to automatically construct an abstract matching function. Firstly, we describe the problem as an alternation-free value-based mu-calculus formula, whose validity can be checked on the program model expressed as a labeled transition system (LTS). Secondly, we translate the analysis into the local resolution of a parameterised boolean equation system (PBES), whose representation enables a more efficient construction of the resulting abstract matching function. Finally, we show how our proposal has been elegantly integrated into CADP, a generic framework for both the design and analysis of distributed systems and the development of verification tools.
paper: (pdf) 2006
presentation: (pdf) 2006
(top)
paper: (pdf) 2006
presentation: (pdf) 2006
(top)
The explicit-state analysis of concurrent systems must handle large state spaces, which correspond to realistic systems containing many parallel processes and complex data structures. In this paper, we combine the on-the-fly approach (incremental construction of the state space) and the distributed approach (state space exploration using several machines connected by a network) in order to increase the computing power of analysis tools. To achieve this, we propose MB-DSOLVE, a new algorithm for distributed on-the-fly resolution of multiple block, alternation-free boolean equation systems (BESs). First, we apply MB-DSOLVE to perform distributed on-the-fly model checking of alternation-free modal mu-calculus, using the standard encoding of the problem as a BES resolution. The speedup and memory consumption obtained on large state spaces improve over previously published approaches based on game graphs. Next, we propose an encoding of the conformance test case generation problem as a BES resolution from which a diagnostic representing the complete test graph (CTG) is built. By applying MB-DSOLVE, we obtain a distributed on-the-fly test case generator whose capabilities scale up smoothly w.r.t. well-established existing sequential tools.
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.
paper: (publications/Gallardo-Joubert-Merino-06-a.pdf) 2006
(top)
paper: (pdf) 2006
presentation: (pdf) 2006
(top)
paper: (pdf) 2005
presentation: (pdf (en),pdf (fr)) 2005
(top)
The verification of concurrent finite-state systems is confronted in practice with the state explosion problem (prohibitive size of the underlying state space), which occurs for realistic systems containing many parallel processes and complex data structures. Various techniques for fighting against state explosion have been proposed, such as on-the-fly verification, partial order reduction, and distributed verification. However, practical experience has shown that none of these techniques alone is always sufficient to handle large-scale systems.
In this thesis, we propose a combination of these approaches in order to scale up their capabilities. Our approach is based upon Boolean Equation Systems (BESs), which provide an elegant intermediate representation for verification problems defined on Labeled Transition Systems, such as equivalence checking, tau-confluence reduction, model checking of alternation-free mu-calculus, and test-case generation.
We propose DSolve and MB-DSolve, two new algorithms for distributed on-the-fly resolution of BESs (containing one, resp. several equation blocks), and employ them as computing engines for four on-the-fly verification tools developed within the CADP toolbox using the OPEN/CAESAR environment: the BISIMULATOR equivalence checker, the TAU_CONFLUENCE reductor, the EVALUATOR model checker, and the EXTRACTOR test-case generator. Experimental measures performed on clusters of machines show quasi-linear speedups and a good scalability of the distributed versions of these tools w.r.t. their sequential counterparts.
paper: (pdf) 2002
presentation: (pdf) 2002
(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) 2005
(top)
presentation: (pdf) 2005
(top)
presentation: (pdf) 2005
(top)
presentation: (pdf) 2005
(top)
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)
annexe: (pdf) 2005
(top)
annexe: (pdf) 2003
(top)