|
SENVA Meeting on Parallel and Distributed Verification in collaboration with the Dutch VeriGEM project |
Scientific Programme
|
Monday April 3, 2006 |
|
|
9h30 |
Welcome – Coffee |
|
9h55 |
Opening Jaco van de Pol (SENVA team co-leader) |
|
|
Session 1: Distributed Model Checking Chair: Jaco van de Pol |
|
10h00 – 10h45 |
Radu Mateescu (SENVA) – Joint work with Christophe Joubert Sequential and Distributed Test Generation using Boolean Equation Systems
Conformance test generation based on verification techniques as implemented in the TGV tool proved its practical usefulness for analysing industrial systems. However, the underlying state space exploration algorithms are based upon depth-first search traversals and therefore unsuitable for distribution. We propose an encoding of the test generation problem as the local resolution with diagnostic of a boolean equation system (BES). This enables to use transparently the sequential and distributed BES resolution algorithms provided by the CAESAR_SOLVE library of CADP for generating conformance test cases on the fly. This method was implemented in a prototype tool named EXTRACTOR, and preliminary experiments show that this approach compares favourably with TGV in terms of memory consumption. |
|
10h45 – 11h20 |
Ivana Cerna (Masaryk University Brno) – joint work with Jiri Barnat and Lubos Brim Distributed LTL Model Checking of Probabilistic Systems
A technique for cluster-based LTL model-checking of finite Markov decision processes is presented. The approach builds on the detection of presence of accepting ergodic sets using reversed OWCTY state elimination technique. |
|
|
Coffee Break |
|
|
Session 2: Mu-calculus and Boolean Equation Systems Chair: Lubos Brim |
|
11h35 – 12h30 |
Martin Leucker (Technical University of Muenchen) – joint work with Orna Grumberg, Martin Lange, and Sharon Shoham Don't know in the mu-calculus
This work presents a novel game-based approach to abstraction-refinement for the full mu-calculus, interpreted over 3-valued semantics. A novel notion of non-losing strategy is introduced and exploited for refinement. Previous works on refinement in the context of 3-valued semantics require a direct algorithm for solving a 3-valued model checking game. This was necessary in order to have the information needed for refinement available on one game board. In contrast, while still considering a 3-valued model checking game, here we reduce the problem of solving the game to solving two 2-valued model checking (parity) games. In case the result is indefinite (don't know), the corresponding non-losing strategies, when combined, hold all the information needed for refinement. This approach is beneficial since it can use any solver for 2-valued parity games. Thus, it can take advantage of newly developed such algorithms with improved complexity or by distributed model checkers. |
|
12h30 – 13h10 |
Jan Friso Groote (Technical University of Eindhoven) – joint work with Kaļs Klaļ A framework for parameterised Boolean equations
Boolean Equation Systems (BESs) have gained popularity as it is a very natural system to which model checking questions can be translated. The question of whether a modal formula holds on a transition system reduces to the question whether a boolean variable in a BES has the value true. We are modelling and analysing real systems. In order to do so, we absolutely need data types. Within the process domain we do the large part of the analysis of the behaviour of processes in the data domain. When encountering modal formulas in the domain of real systems, we cannot do without data. But this means that our Boolean Equation Systems also need data. So, following Mateescu (1998) we are looking at Parameterised Boolean Equation Systems (PBESs). In this presentation we show that PBESs can be solved by data manipulation and we explain that we are currently working on a toolset that assists in helping solving PBESs with data manipulations. |
|
|
Lunch |
|
|
Session 3: State Space Reduction Chair: Jan Friso Groote |
|
14h15 – 15h00 |
Hubert Garavel (SENVA) – joint work with Wendelin Serwe State Space Reduction for Process Algebra Specifications
Data-flow analysis to identify ``dead'' variables and reset them to an ``undefined'' value is an effective technique for fighting state explosion in the enumerative verification of concurrent systems. Although this technique is well-adapted to imperative languages, it is not directly applicable to value-passing process algebras, in which variables cannot be reset explicitly due to the single-assignment constraints of the functional programming style. This paper addresses this problem by performing data-flow analysis on an intermediate model (Petri nets extended with state variables) into which process algebra specifications can be translated automatically. It also addresses important issues, such as avoiding the introduction of useless reset operations and handling shared read-only variables that children processes inherit from their parents. |
|
15h00 –15h30 |
Michael Weber (SENVA) Static Analyses for State Space Reduction
The state space explosion problem is still the limiting factor for the applicability of model-checking tools. The problem is somewhat reduced by on-the-fly state-space reduction methods, among which Partial-Order Reduction (POR) is one of the most effective. POR yields as result a state-space which is smaller, but indistinguishable under a temporal logic specification from the unreduced one. However, POR techniques so far are highly language dependant, and usually tightly integrated with state-space generators. Additionally, they do not work equally well in all settings, for example in distributed state space generation. To counter these restrictions, we present an extended version of a static analysis called Path Reduction by Yorav and Grumberg, which is only dependant on an intermediate representation, and does not require changes in the state-space generator, nor the compiler generating the intermediate representation. The reduction preserves CTL*-X properties, and performs well in practice. |
|
|
Coffee Break |
|
|
Session 4: Position Statements on Future Project Chair: Jaco van de Pol |
|
16h00 – … |
Grenoble – Hubert Garavel (SENVA) |
|
… |
Brno – Lubos Brim (Masaryk University Brno) |
|
… |
Eindhoven – Jan Friso Groote (Technical University of Eindhoven) |
|
… |
Muenchen – Martin Leucker (Technical University of Muenchen) |
|
… |
Twente – Matthias Kuntz (University of Twente) |
|
… |
Aalborg – Gerd Behrmann (University of Aalborg) |
|
… – 18h00 |
Amsterdam – Jaco van de Pol (SENVA) |
|
19h15 |
Dinner |
|
Tuesday April 4, 2006 |
|
|
|
Session 5: Grids Chair: Radu Mateescu |
|
9h30 – 10h30 |
Henri Bal (Vrije Universiteit Amsterdam) Distributed supercomputing on DAS, GridLab, and Grid'5000
The Distributed ASCI Supercomputer (DAS) is an infrastructure for experimental computer science research on distributed systems and grids. Two DAS systems have been built so far, each consisting of multiple Myrinet clusters located at 4-5 different universities of the ASCI research school. (A third system, DAS-3, is under way.) This talk first summarizes the history of DAS and describes its impact on Dutch computer science research. Next, it discusses distributed supercomputing experiments on DAS-2, mainly using the Ibis Java-centric middleware developed at the Vrije Universiteit. Next, the talk describes more recent experiments on a European testbed (GridLab) consisting of DAS-2 and other clusters, and on the French Grid'5000 system. |
|
|
Short Coffee Break |
|
10h40 – 11h05 |
Open discussion with Henri Bal |
|
11h05 – 11h30 |
Josva Kleist (Aalborg University)
Abstract to be provided |
|
11h30 – 12h00 |
Gerd Behrmann (Aalborg University) Distributed Timed Automata Reachability
Abstract to be provided |
|
12h00 |
Lunch |
|
|
Session 6: Workshop |
|
13h15 – 15h00 |
Draft of Future Project
Panel discussion |
|
15h00 – 17h00 |
Technical discussions |
|
17h00 |
Closing |