SENVA 2004
Workshop 

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, ELOTOS, 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
Dataflow 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 welladapted to imperative languages, it
is not directly applicable to valuepassing process algebras, in which
variables cannot be reset explicitly due to the singleassignment constraints
of the functional programming style. This talk addresses this problem by performing dataflow
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 readonly 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 computeraided 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 welladapted to compiling highlevel, 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 realtime 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
casestudies: the performance study of the Hubble telescope flight
stabilizers protocol.and the SCSI2 bus arbitration protocol. 
12h00 – 12h20 
Holger Hermanns
(Saarland University) — joint work with Christel Baier, JoostPieter
Katoen, Boudewijn Haverkort, Markus Siegle, Joachim MeyerKayser 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 continuoustime Markov decision
processes. 
12h20 – 13h05 
Sven Johr (Saarland University) — joint work with Holger Hermanns Turning Interactive Markov Chains to ContinuousTime 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, JoostPieter 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 nondeterminism, probabilistic
branching, and hard realtime as well as soft realtime (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
userdefined 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 finitestate concurrent systems, in particular the equivalence checking and the model checking problems. These problems can be solved onthefly (i.e., without constructing explicitly the state space of the system under analysis) by using a demanddriven construction and resolution of the corresponding boolean equation system. In this report, we present a generic software library dedicated to onthefly resolution of alternationfree boolean equation systems. Four resolution algorithms are currently provided by the library: A1 and A2 are general algorithms, the latter being optimized to produce smalldepth diagnostics, whereas A3 and A4 are specialized algorithms for handling acyclic and disjunctive/conjunctive boolean equation systems in a memoryefficient way. The library is developed within the CADP verification toolbox and is used for both onthefly equivalence checking (five widelyused equivalence relations are supported) and for onthefly model checking of alternationfree modal mucalculus. 
18h00 – 18h45 
Radu Mateescu
(SENVA) — joint work with Damien Bergamini and Nicolas Descoubes BISIMULATOR: A Tool for OntheFly Equivalence Checking Equivalence checking is a wellknown
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 onthefly 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 onthefly equivalence
checker BISIMULATOR, built within the CADP toolbox using the OPEN/CAESAR
environment. BISIMULATOR implements five widelyused 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 onthefly using the
CAESAR_SOLVE library of CADP. If the equivalence check yields a negative
answer, BISIMULATOR provides smallsized 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 onthefly 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 OntheFly
Equivalence Checking Onthefly equivalence checking consists in
comparing two Labeled Transition Systems (LTSs) modulo an equivalence
relation by exploring them in a demanddriven 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 onthefly equivalence checking using several
machines connected by a network. We
propose DSOLVE, a new algorithm for distributed onthefly 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 onthefly equivalence checker
developed within the CADP verification toolbox using the OPEN/CAESAR
environment. Our experimental measures
show quasilinear 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
onebit 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 