SENVA
Meeting on Clusters and Grids for Verification and Performance Evaluation 
Scientific Programme
Wednesday November 16, 2005 Clusters: Where we are 

8h45 
Welcome and Opening Hubert Garavel and Jaco van de Pol (SENVA team leaders) 

Session 1: Performance Evaluation using Clusters Chair: Hubert Garavel 
9h00 – 9h50 
Marta Kwiatkowska (University of Birmingham) Parallel and Distributed Methods in the Probabilistic Model Checker PRISM
In this talk, we will give an overview of the probabilistic model checker PRISM, in particular highlighting the parallel, distributed and outofcore methods. 

Tool demonstration. 
9h50 – 10h30 
Boudewijn Haverkort (University of Twente) Experiences with ClusterBased ModelChecking of Stochastic Systems
In this talk, we will share with you some experiences (positive and negative) we recently gathered with evaluating very large Markovian models (as they arise in model checking CSL or CSRL) on a cluster of workstations. I will briefly point forward to our plans to perform this type of analysis on grids. 

Special session 
10h30 – 11h00 
François Brown de Colstoun (Director, European and International Relations, INRIA) Tools for International Collaboration at INRIA 

Coffee Break 

Session 2: Model Checking using Clusters (Part I) Chair: Radu Mateescu 
11h20 – 12h10 
Lubos Brim (Masaryk University Brno) – joint work with Jiri Barnat and Ivana Cerna Distributed LTL Model Checking
We survey most of the known distributed enumerative LTL model checking algorithms, compare them both theoretically and experimentally, discuss their advantages and disadvantages, and determine cases in which individual algorithms are more appropriate than the others. 
12h10 – 12h45 
Jiri Barnat (Masaryk University Brno) – joint work with Lubos Brim, Ivana Cerna, and Pavel Simecek
We introduce the Distributed Verification Environment (DiVinE), which is meant to support the development of distributed enumerative model checking algorithms, to enable a unified and credible comparison of these algorithms, and to make the distributed verification available for public use in a form of a distributed verification tool. We present DiVinE from both the users's and programmer's points of view, and we uncover a few plans to be realized in the future. 

Lunch 

Session 3: State Space Generation and Minimization using Clusters Chair: Lubos Brim 
14h15 – 14h45 
Stefan Blom (Innsbruck University) Batch Oriented State Space Generation
A very simple fact of life on clusters is that jobs using few CPUs for a short time are much easier to schedule and can be scheduled much more efficiently than jobs which require a large number of CPUs for a long time. We present a method for distributed state space generation, which works by presenting a large number of small jobs to the batch scheduler of the cluster rather than a single huge job. 
14h45 –15h15 
Jaco van de Pol (SENVA) – joint work with Stefan Blom, Bert Lisser, and Simona Orzan Distributed State Space Generation and Minimization
This talk provides an overview of the current distributed verification tools constructed at CWI. The tools are part of the muCRL project. Our current verification philosophy is as follows: Step 1. Generate the state space on a cluster of PCs, and store it permanently on disk. Step 2. Minimize the state space modulo equivalences by distributed algorithms. Step 3. Check properties of the reduced state space (on a sequential machine). The state space generation algorithm is a variant of breadthfirst search. Clearly, the gain is an increase in speed, as well as an increase of the state spaces that can be generated. Simple safety properties can be checked onthefly. A distinguishing feature is the ability to abort the generation, and resume it at a later moment, or after a crash of some PCs. The resulting state space is permanently stored, either on the local disk of the PCs, but typically on a separate file server. File formats have been defined in collaboration with INRIA RhôneAlpes in the joint SENVA project. The next step is to reduce the state space modulo an equivalence relation. We have implemented distributed algorithms for strong bisimulation reduction and for branching bisimulation reduction. We also implemented a distributed taucycle elimination tool, which can be used as a preprocessor of branching bisimulation reduction. In many cases, the reduced state space fits in the memory of one computer, so sequential model checking algorithms can be used. A distributed implementation for an explicit state mucalculus checker is planned. We observed that for a highlevel specification language, generating the state space is relatively labourintensive. Note that – opposed to purely onthefly methods – by permanently storing the graph, it is possible to generate the state space once, and repeat steps 2 and 3 for different properties, with their corresponding hide sets. 
15h15 – 15h50 
Hubert Garavel (SENVA) – joint work with Radu Mateescu, Christophe Joubert, and al. Distributor and Bcg_Merge: Tools for Distributed State Space Generation
The verification of complex finitestate systems, whose underlying state spaces may be prohibitively large, requires an important amount of memory and computation time. A natural way of scaling up the capabilities of verification tools is by exploiting the computing resources (memory and processors) of massively parallel machines, such as clusters and grids. This talk describes Distributor, a tool for generating state spaces in a distributed manner using a set of machines connected by a network. Each machine is responsible for generating and storing a part of the state space. Upon termination of the distributed generation, all parts generated by the machines are combined together using the Bcg_Merge tool in order to obtain the complete state space. Distributor was developed within the CADP verification toolbox using the generic Open/Caesar environment for onthefly graph exploration. It exhibits good speedups compared to sequential tools, implements onthefly reductions of the state space, and provides graphical features for monitoring the distributed state space generation in real time. 

Tool demonstration. 

Coffee Break 

Session 4: Model Checking using Clusters (Part II) Chair: Jaco van de Pol 
16h20 – 16h50 
Michael Weber (RWTH Aachen University) – joint work with Martin Leucker, Vojtech Forejt, and Jiri Barnat DivSPIN: A SPIN Compatible Distributed Model Checker
We describe the design and implementation ideas of an extension of the parallel and distributed model checker DiVinE to a SPIN compatible distributed model checker DivSPIN. The goal of DivSPIN is to serve as userfriendly, readytouse system that takes up the recent theoretical and practical developments in the area of distributed model checkers and combines them with well settled operational procedures of sequential model checkers to show the benefits of parallel model checking for typical verification tasks. 
16h50 – 17h20 
Simona Orzan (Technical University of Eindhoven) – joint work with Jaco van de Pol (SENVA) Detecting Strongly Connected Components in Large Distributed State Spaces
Finding strongly connected components (SCCs) in state spaces is useful, for instance, as preprocessing step in branching bisimulation reduction algorithms. Although very efficient SCC detection algorithms exist, they are inherently sequential and transforming them into efficient parallel algorithms is not straightforward. We present a collection of distributed state space transformations that lead to the decomposition of very large distributed state spaces into SCCs. The transformations can be used as building blocks for custom algorithms. We also describe two example algorithms and show that they perform well on practical case studies. 
17h20 – 18h00 
Christophe Joubert (SENVA) – joint work with Radu Mateescu Distributed OntheFly Resolution of Boolean Equation Systems
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, sequential implementations do not scale up satisfactorily as the size of BESs increases. In this talk, we propose a distributed algorithm, called DSolve, which performs the local resolution of a singleblock 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. 
18h00 – 18h30 
Radu Mateescu (SENVA) – joint work with Christophe Joubert Distributed Onthefly Equivalence Checking and TauConfluence Reduction
The verification of concurrent finitestate systems is confronted in practice with the state explosion problem (prohibitive size of the underlying state spaces), 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 onthefly verification, partialorder reduction, and distributed verification. However, practical experience has shown that none of these techniques alone is always sufficient to handle largescale systems. In this talk, we propose a combination of these techniques in order to scale up their capabilities. Our approach is based upon Boolean Equation Systems (BESs), which provide an elegant intermediate representation for equivalence checking and tauconfluence reduction problems defined on Labeled Transition Systems (LTSs). We illustrate the use of DSolve, a new algorithm for distributed onthefly resolution of singleblock BESs, as computing engine for two onthefly verification tools developed within the CADP toolbox using the Open/Caesar environment: the Bisimulator equivalence checker and the Tau_Confluence reductor. We also show experimental measures obtained on PC clusters that underline the performance gains brought to these tools by distribution. 

Tool demonstration. 
20h00 
Dinner 
Thursday November 17, 2005 Grids: Where we go 


Session 1: Verification and Performance Evaluation using Grids Chair: Stefan Blom 
9h00 – 9h30 
William Knottenbelt (Imperial College London) Gridbased Performance Analysis using Continuous Stochastic Logics: the GRAIL Project
In this talk we will introduce and discuss the aims of our latest EPSRCfunded stochastic modelchecking research grant. 
9h30 –10h40 
Gerd Behrmann and Josva Kleist (Aalborg University) NorduGrid – Grid Activities in the Nordic Countries
NorduGrid is a production grid consisting of approximately 50 sites with 4500 CPU's and 60 TB of storage. In this talk we describe the NorduGrid Advanced Resource Collector  the middleware running NorduGrid. 

Coffee Break 

Session 2: Panel Discussions on Verification and Grid Computing 
11h00 – 11h45 
Martin Leucker (Technical University of Muenchen) Requirements for a Model Checking Grid
Panel discussion 
11h45 – 12h30 
Jaco van de Pol (SENVA) Grid Computing for Verification
Panel discussion 

Lunch 

Session 3: Prospective Discussions (Part I) 
14h00 – 15h00 

15h00 – 15h30 
Hidde de Jong (HELIX, INRIA)
Motivation: The modeling and simulation of genetic regulatory networks has created the need for tools for model validation. The main challenges of model validation are the achievement of a match between the precision of model redictions and experimental observations, as well as the efficient and reliable comparison of the predictions and observations. Results: We present an approach towards the validation of models of genetic regulatory networks addressing the above challenges. It combines a method for qualitative modeling and simulation with techniques for model checking, and is supported by a new version of the computer tool GNA. The modelvalidation approach has been applied to the analysis of the network controlling the nutritional stress response in Escherichia coli. 

Coffee Break 

Session 4: Prospective Discussions (Part II) 
16h30 – 18h30 

20h00 
Dinner 