|
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, 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 |