SENVA 2005 Meeting

SENVA Meeting on Clusters and Grids for Verification and Performance Evaluation
INRIA Rhône-Alpes - Montbonnot (Isère)

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 out-of-core methods.
	Tool demonstration.
9h50 – 10h30	Boudewijn Haverkort (University of Twente) Experiences with Cluster-Based Model-Checking 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 DiVinE and DiVinE within 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 breadth-first 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 on-the-fly. 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ône-Alpes 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 tau-cycle 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 mu-calculus checker is planned. We observed that for a high-level specification language, generating the state space is relatively labour-intensive. Note that – opposed to purely on-the-fly 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 finite-state 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 on-the-fly graph exploration. It exhibits good speedups compared to sequential tools, implements on-the-fly 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 user-friendly, ready-to-use 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 On-the-Fly 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 single-block 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 On-the-fly Equivalence Checking and Tau-Confluence Reduction The verification of concurrent finite-state 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 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 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 tau-confluence reduction problems defined on Labeled Transition Systems (LTSs). We illustrate the use of DSolve, a new algorithm for distributed on-the-fly resolution of single-block BESs, as computing engine for two on-the-fly 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) Grid-based Performance Analysis using Continuous Stochastic Logics: the GRAIL Project In this talk we will introduce and discuss the aims of our latest EPSRC-funded stochastic model-checking 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) Validation of Qualitative Models of Genetic Regulatory Networks by Model Checking: Nutritional Stress Response in E. coli 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 model-validation 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