SENVA 2004 Workshop
Allevard-Les-Bains (Isère)

 

 


Workshop Programme


Monday June 21, 2004

15h30

Workshop Opening

15h30 – 16h45

Frédéric Lang (SENVA)

The EXP.OPEN 2.0 Tool

 

In this talk, I will present the most recent version of EXP.OPEN, an OPEN/CAESAR compiler dedicated to compositional verification.  As all other OPEN/CAESAR compilers, EXP.OPEN allows verification using any OPEN/CAESAR application, including interactive simulation (OCIS), state space generation (GENERATOR), temporal logic verification (EVALUATOR), on the fly comparison modulo various bisimulation relations (BISIMULATOR), etc. I will describe the features added to EXP.OPEN 2.0: its extended input language, which now includes — in addition to LOTOS operators — powerful operators taken from various languages (e.g., CSP, E-LOTOS, and mCRL), and several partial order reduction techniques. Finally, the performances of EXP.OPEN 2.0 (combined with various OPEN/CAESAR applications) will be compared to EXP.OPEN 1.0 and other tools with common functionalities, such as ALDEBARAN.

17h00 – 18h00

Judi Romijn (Eindhoven University of Technology) — joint work with Nicu Goga

Guiding Spin Simulation

 

We show how to guide simulations with Spin, by constructing a special guide process that limits the behaviour of the original system. We present a theoretical framework in which it is proven under some sufficient conditions that the adjusted system (with the added guide process) exhibits a subset of the behaviour of the original system, and has no new deadlocks. We have applied this technique to a Promela specification of the IEEE 1394.1 FireWire net update algorithm. The experiment shows that this technique increases the error detecting power of Spin in the sense that it found errors in the guided specification, which (because of the state space explosion) could not be discovered with Spin simulation and validation in the original specification.

18h00 – 18h45

David Champelovier (SENVA) — joint work with Hubert Garavel, Frédéric Lang, and Radu Mateescu

Compiler Construction using LOTOS NT

 

We present a technology for compiler generation based on the data part of LOTOS NT, a specification language for protocols and distributed systems. We used this technology for constructing five domain specific compilers, four of which are or will be  included in the CADP verification toolbox.

Tuesday June 22, 2004

9h30 10h00

Damien Bergamini (SENVA) — joint work with Hubert Garavel

The CAESAR net work model

 

This talk is a short introduction to the intermediate model used by the LOTOS compiler CAESAR. It shows how this intermediate model is generated for some very simple LOTOS operators. It also presents a small subset of all the optimizations that are implemented in the compiler. Finally, it gives some informations on the simulation algorithm of CAESAR.

10h00 11h00

Wendelin Serwe (SENVA) — joint work with Hubert Garavel

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 talk 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.

11h30 12h10

Bert Lisser (SENVA)

Reducing state spaces by transforming linear process equations 

 

Linear process equations are symbolic representatives of state spaces. Which transformations of linear process equations are applicable, such  that state spaces are generated faster from them or that generated state spaces have smaller state vectors or less states. There will be introduced four transformation algorithms, called constelm, parelm, sumelm, and structelm, which are implemented in the  muCRL toolset. An example will be given, which demonstrates the effect of cooperation of these algorithms.

12h10 12h30

Bert Lisser (SENVA)

Demonstration of the JSIM bfs simulator

 

Lunch

14h30 15h30

Frédéric Lang (SENVA) — joint work wih Hubert Garavel

NTIF: A General Symbolic Model for Communicating Sequential Processes with Data

 

One central problem in the computer-aided verification of concurrent systems consisting of communicating sequential processes with data is to find suitable symbolic models. Such models should provide a compact computer representation for control and data flows, and should be appropriate for mainstream verification techniques such as model checking and theorem proving.  A number of symbolic models have been proposed, many of which based on the guarded commands (also known as condition/action) paradigm. In this talk, we draw attention to the limitations of this paradigm and propose a better model named NTIF (New Technology Intermediate Form), which is well-adapted to  compiling high-level, concurrent languages (such as the ELOTOS standard).

15h30 16h30

Aurore Collomb (SENVA) — joint work wih Hubert Garavel and Frédéric Lang

Sequential Processes with Data and Time: A Timed Extension of NTIF

 

Modeling of real-time systems follows two main approaches: automata based approaches (timed automata, timed Petri nets), and timed process algebras. However, it is confronted to a twofold problem: On the one hand, automata based approaches are not suitable to model specifications with lots of states and complex data handling.  On the other hand, process algebras with data and time could solve this problem, but too often their semantics is complex.  A consequence is the limited number of verification tools for process algebras with data and time. In this presentation, we propose a method to simplify the semantics of timed process algebras, by observing that properties inherent to time (namely time additivity, time determinism, and maximal progress) can be decoupled from the structural semantics definition.  To this aim, we define a time equivalence relation on TLTSs (Timed Labeled Transition Systems), a classical graph model for most timed process algebras, which includes orthogonal timed transitions and    action transitions. We illustrate this method by defining a timed extension of NTIF, an intermediate formalism inspired from process algebras, symbolic automata, and algorithmic languages. The simplicity of the rules combined with the power of the equivalence relation allows to verify easily  suitable semantic properties. This approach could be used to simplify the semantics of many process algebras.

Wednesday June 23, 2004

9h30 –10h45

Holger Hermanns (Saarland University)

Stochastic Modelling and Analysis

 

 In this talk, I give a gentle introduction into stochastic modelling, touching upon the issues of model construction and model analysis both from a historical and from a pragmatic perspective.

10h45 – 11h30

Hubert Garavel (SENVA) — joint work with Holger Hermanns and Christophe Joubert

On Combining Functional Verification and Performance Evaluation Using CADP

 

 

Considering functional correctness and performance evaluation in a common framework is desirable, both for scientific and economic reasons. In this presentation, we describe how the CADP toolbox, originally designed for verifying the functional correctness of LOTOS specifications, can also be used for performance evaluation. We describe the following set of analysis components recently added to the toolbox: BCG_STEADY, BCG_TRANSIENT, and DETERMINATOR. The approach taken fits well within the existing architecture of CADP, which doesn't need to be altered to enable performance evaluation. We illustrate the proposed approach with two case-studies: the performance study of the Hubble telescope flight stabilizers protocol.and the SCSI-2 bus arbitration protocol.

12h00 – 12h20

Holger Hermanns (Saarland University) — joint work with Christel Baier, Joost-Pieter Katoen, Boudewijn Haverkort, Markus Siegle, Joachim Meyer-Kayser and Sven Johr

Model Checking Markov Chains and Decision Processes

 

This talk introduces into the concepts of stochastic model checking. It first focusses on Markov Chain models. Then it delves into the challenges of model checking Markov models with nondeterminism, in  particular continuous-time Markov decision processes.

12h20 – 13h05

Sven Johr (Saarland University) — joint work with Holger Hermanns

Turning Interactive Markov Chains to Continuous-Time Markov Decision Processes

 

CTMDPs are generalisations of CTMCs where nondeterministic and stochastic behaviour coexist in this model. Intuitively, CTMDPs can be viewed as a common semantic model for various performance and dependability models, e.g., GSPNs, SANs, TIPP process algebra, IMCs. This talk aims to make this intuition more precise. A transformation procedure mapping IMCs on CTMDPs is discussed. The three main steps of this procedure are given and shown to be at least weak bisimulation preserving. Having discussed the transformation steps, some results on the size of the input IMC and output CTMDP are presented. The example used is the so called 'mutual exclusion with random times' algorithm.

 

Lunch

14h30 – 16h00

Holger Hermanns (Saarland University) — joint work with Pedro d'Argenio, Henrik Bohnenkamp, Joost-Pieter Katoen, and

Ric Klaren

MODEST: A Model Description Language for Stochastic Timed Systems

 

This talk presents a modelling language, called MoDeST, for describing the behaviour of discrete event systems.  The language combines conventional programming constructs -- such as iteration, alternatives, atomic statements, and exception handling -- with means  to describe complex systems in a compositional manner.  In addition, MoDeST incorporates means to describe important phenomena such as non-determinism, probabilistic branching, and hard real-time as well as soft real-time (i.e., stochastic) aspects. The talk covers (i) the language design and its features, (ii) the operational semantics and the resulting transition system model, (iii) tool development and (iv) recent case studies.

16h15 – 17h20

Jaco van de Pol (SENVA) — joint work with Miguel Valero Espada

Abstract Model Checking for Process Algebra

 

We show how the model checking problem on LTSs can be approximated by model checking on modal LTSs. A modal LTS has two types of transitions: may and must transitions, which form an over- and underapproximation of the original LTS.  Model checking on a modal LTS yields three kinds of results: the formula either holds necessarily, or it holds possibly, but not necessarily, or it doesn't possibly hold. In the first case, the property will hold for the original, in the last case it doesn't hold for the original. Only in the middle case the validity of the property on the original LTS is unknown, because the approximation lost essential information.  We implemented this approach for process algebra, by transforming any LPE (linear process equation) to a modal LPE. The transformation can use user-defined abstractions, and has an automatic mode as well.  Modal LPEs can be represented as normal LPEs. By this we can reuse the mCRL and CADP tool sets for abstract model checking.  As a result, we were able to verify safety and liveness properties for some parameterized and infinite state systems.

17h30 – 18h00

Radu Mateescu (SENVA)

The CAESAR_SOLVE_1 library

 

 Boolean Equation Systems are a useful formalism for modeling various verification problems of finite-state concurrent systems, in particular the equivalence checking and the model checking problems. These problems can be solved on-the-fly (i.e., without constructing explicitly the state space of the system under analysis) by using a demand-driven construction and resolution of the corresponding boolean equation system. In this report, we present a generic software library dedicated to on-the-fly resolution of alternation-free boolean equation systems. Four resolution algorithms are currently provided by the library: A1 and A2 are general algorithms, the latter being optimized to produce small-depth diagnostics, whereas A3 and A4 are specialized algorithms for handling acyclic and disjunctive/conjunctive boolean equation systems in a memory-efficient way. The library is developed within the CADP verification toolbox and is used for both on-the-fly equivalence checking (five widely-used equivalence relations are supported) and for on-the-fly model checking of alternation-free modal mu-calculus.

18h00 – 18h45

Radu Mateescu (SENVA) — joint work with Damien Bergamini and Nicolas Descoubes

BISIMULATOR: A Tool for On-the-Fly Equivalence Checking

 

Equivalence checking is a well-known verification technique consisting to compare the Labelled Transition System (LTS) representing the behaviour of a system (e.g., a protocol) with the LTS representing its desired external behaviour (e.g., a service) modulo a suitable equivalence relation. There are basically two approaches for equivalence checking: the global approach, which requires to build the two LTSs before verification, and the on-the-fly approach, which allows to explore the LTSs incrementally during verification. The latter approach enables to detect errors even when the LTSs are too large to be constructed explicitly.  We present the on-the-fly equivalence checker BISIMULATOR, built within the CADP toolbox using the OPEN/CAESAR environment. BISIMULATOR implements five widely-used equivalence relations (strong, branching, observational, tau*.a, and safety) over LTSs. The verification method consists in translating each equivalence relation into a Boolean Equation System (BES), which is solved on-the-fly using the CAESAR_SOLVE library of CADP. If the equivalence check yields a negative answer, BISIMULATOR provides small-sized diagnostics (counterexamples) illustrating the non equivalence of the two LTSs. An extensive set of experiments carried out using LTSs from the CADP release and the VLTS benchmark suite assessed the efficiency of BISIMULATOR w.r.t. other tools implementing on-the-fly equivalence checking algorithms.

Thursday June 24, 2004

9h30 – 10h00

Nicolas Descoubes (SENVA)

CAESAR_NETWORK, a Library for Distributed Model Checking

 

In the domain of verification, the memory limitations imposed by the hardware are often reached, which reduces the size of solvable problems.  A common solution consists in distributing algorithms so that they can be run on several machines, offering a much bigger computation power and much more memory. When implementing such algorithms, the problem of the communication between the nodes appears systematically. The CAESAR NETWORK library provides a set of primitives to handle the configuration and the exchange of messages, so that it becomes easier to implement distributed algorithms. This presentation aims at showing the features and the working of this library. Some applications will be presented.

10h00 – 10h45

Christophe Joubert (SENVA) — joint work with Radu Mateescu and Nicolas Decoubes

Distributed On-the-Fly Equivalence Checking

 

On-the-fly equivalence checking consists in comparing two Labeled Transition Systems (LTSs) modulo an equivalence relation by exploring them in a demand-driven way, which allows to detect errors in LTSs too large to be constructed explicitly.  In this presentation, 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 ascverification engine for the distributed version of BISIMULATOR, an on-the-fly equivalence checker developed within the CADP verification toolbox using the OPEN/CAESAR environment.  Our experimental measures show quasi-linear speedups and a good scalability of the distributed version of BISIMULATOR w.r.t. its sequential version.

11h15 – 12h10

Stefan Blom (SENVA) — joint work with Simona Orzan

Bisimulation Reduction Using Signature Based Partition Refinement

 

A signature of a state with respect to a partition of the set of states is the set of moves the state can make to the various equivalence classes in the partition. A signature definition gives rise to a bisimulation relation. In this talk, we will give signature definitions for strong bisimulation, branching bisimulation, tau*a equivalence and weak bisimulation.  Next, we will explain the basic signature refinement algorithm, which is a naive brute force algorithm. We will give and overview of the distributed implementation of the algorithm and of the various tweaks made to sequential versions.

12h20 – 13h10

Wan Fokkink (SENVA) — joint work with Bahareh Badban, Jan Friso Groote, Jun Pang,  and Jaco van de Pol

Verification of a Sliding Window Protocol in mCRL

 

Within the process algebraic community, much effort has been spent on analyzing sliding window protocols. Aart Middeldorp (1986) and Jacob Brunekreef (1993) gave specifications in ACP and PSF, respectively. Frits Vaandrager (1986), Richard Groenveld (1987), Jos van Wamel (1992) and Marc Bezem and Jan Friso Groote (1994) manually verified one-bit sliding window protocols, in which the size of the sending and receiving window is one. Starting in 1990, we attempted to prove the most co mplex sliding window protocol (not taking into account additional features such as duplex message passing and piggybacking) from Tanenbaum's "Communication Protocols" correct using mCRL. This turned out to be unexpectedly hard, which is shown by the 13 years it took to complete this work.

 

Lunch

14h30 – 15h40

Judi Romijn (Eindhoven University of Technology) — joint work with Nicu Goga, Izak van Langevelde, Arjan Mooij, and Wieger Wesselink

Correcting IEEE 1394.1 FireWire Net Update

 

The new IEEE 1394.1 FireWire draft standard, which will be finalised this year, contains a new protocol for constructing and maintaining spanning trees in the network topology, called net update. This protocol is complex and merits formal specification and analysis.  I give an overview of the work done on this protocol in the scope of our IQPS Project. Through Promela prototyping (Spin simulation and model checking), PVS protocol derivation and manual proof, we have discovered and corrected many errors, omissions and inconsistencies, and we have determined the correctness properties of the protocol which have been added to the standard description.  .

15h45

Workshop Closing and Departure