SENVA 2005 Workshop
Saint Pierre de Chartreuse (Isère)

Monday May 30, 2005

9h30

Workshop Opening

10h00 – 10h50

Jeff Kramer (Imperial College, London) — joint work with Jeff Magee, Sebastian Uchitel, and Robert Chatley

System Architecture: the Context for Scenario-based Model Synthesis

Constructing rigorous models for analysing the behaviour of concurrent and distributed systems is a complex task. Our aim is to facilitate model construction. In this talk we combine a scenario synthesis approach with an architecture description language (ADL) to provide automated support for model construction. Scenarios provide simple, intuitive, example based descriptions of the behaviour of component instances in the context of a simplified architecture instance. Software architecture descriptions give the necessary contextual information so that component instance behaviour can be generalised to component type behaviour. Furthermore, ADLs can then be used to describe the complex architectures in which the generalised behaviours need to be instantiated. Thus, architectural information used in conjunction with scenario-based model synthesis can support both model construction and elaboration, where the behaviour derived from simple architecture fragments can be instantiated in more complex ones.

10h50 – 12h00

Frédéric Lang (SENVA)

Compositional Verification of Networks of Processes using Refined Interface Generation 

The compositional verification approach of Graf & Steffen aims at avoiding state space explosion for individual processes of a concurrent system; it relies on interfaces that express the behavioural constraints imposed on each process by synchronization with the other processes, thus preventing the exploration of states and transitions that would not be reachable in the global state space. Krim & Mounier, and Cheung & Kramer proposed two techniques to generate such interfaces automatically. In this talk, we propose a refined interface generation technique, in which the interface of each process is derived automatically from the examination of (a subset of) concurrent processes. This technique is applicable to formalisms in which concurrent processes are composed either using synchronization vectors or process algebra parallel composition operators (including those of CCS, CSP, MCRL, LOTOS, and ELOTOS), for which we have developed a tool. Experiments indicate state space reductions by one or two orders of magnitude for the largest processes.

Coffee Break

12h05 – 12h45

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

Accelerated must-transitions to get more progress

Abstractions yield small approximations of large state spaces. A common approach is to have both an over-approximation by may-steps (to prove safety properties) and an under-approximation by must-steps (to prove progress properties). However, due to the loss of information by approximation, this often yields less must-steps than required, blocking the proof of interesting progress properties.

In this talk, accelerated must-steps will be introduced. These are must-steps labeled by a regular expression, rather than a single action. They express that there must exist a path with a certain property. A prototypical example is a timer: usually, there is no must-step "decrement" from state "positive" to "zero", but there is a "decrement+" step, expressing that "zero" is certainly reached after a finite number of steps. So from the initial state we can prove <decrement+.timeout>True.

I will introduce the new model of LTS with accelerated must-transitions, prove soundness of the new abstraction, and sketch a new model checking algorithm for these LTS's.

Lunch

14h30 – 15h30

Jeff Magee (Imperial College, London) — joint work with Jeff Kramer and Dimitra Giannakopoulou

Fluent LTL for Event-Based Systems

In labeled transition system descriptions of event-based systems, states are not characterized by state variables, but rather by the behavior that  originates in these states, in terms of actions. In this context, it is natural for temporal formulas to be built from atomic propositions that are predicates on the occurrence of actions. The talk identifies limitations in this approach and introduces "fluent" propositions that permit formulas to naturally express properties that combine state and action. A fluent is a property of the world that holds after it is initiated by an action and ceases to hold when terminated by another action. The talk describes an approach to model checking fluent-based linear-temporal logic properties, with its implementation, application and subsequent development in the LTSA tool.

15h30 – 16h15

Wendelin Serwe (SENVA) — joint work with Gwen Salaün

Translating Hardware Process Algebra into Standard Process Algebra: Illustration with CHP and LOTOS

A promising approach to deal with the increasing complexity of highly integrated micro-electronic devices are asynchronous circuits and architectures. They can be described at a high level using process algebras with particular operators responding to the need of hardware designers to exploit lower level features.  In order to enable the use of verification tools developed in the process algebra community, hardware process algebras need to be translated into standard process algebras.

In this talk, we propose a compositional operational semantics for the hardware process algebra CHP. The advocated semantics generalises existing semantics based on a lower level encoding of CHP into Petri nets, and does not require the expansion of communication according to handshake protocols.  In a second step, we use our semantics as basis for the formal definition of a translation from CHP into the standard process algebra LOTOS. A prototype translator has been successfully used for the compositional verification of a real asynchronous circuit using the verification toolbox CADP.

Coffee Break

16h30 – 17h25

Gwen Salaün (SENVA) — joint work with Daniela Berardi, Lucas Bordeaux, Antonella Chirichiello, Andrea Ferrara, Massimo Mecella, and Marco Schaerf

Describing and Reasoning on Web Services using Process Algebra

Web services are network-based software components deployed and accessed through the Internet using standard interface description languages and uniform communication protocols. Each service solves a precise task, and may communicate with possible mates by exchanging messages.

Formal methods, and in particular process algebra, provide an adequate framework to tackle different issues raised in the web services area. First, they provide an abstract way to describe services (or their interfaces). Hence, composition of interacting services can be formalised as well. In addition, process algebras are   often equipped with automated reasoning tools which are useful to ensure the correct development of services or to check their compatibility. All these issues will be illustrated through examples of e-business services.

17h25 – 18h20

Anton Wijs (SENVA) — joint work with Jaco van de Pol and Elena Bortnik

Solving Scheduling Problems by Untimed Model Checking - The Clinical Chemical Analyser Case Study

We show how scheduling problems can be modelled in untimed process algebra, by using special tick-actions. As a result, we can use efficient, distributed state space generators to solve scheduling problems. Also, we can use more flexible data specifications than timed model checkers usually provide. We propose a variant on breadth-first search, which visits the states per time slice between ticks. We applied our approach to find optimal schedules for test batches of a realistic clinical chemical analyser, which performs several kinds of tests on patient samples.

Tuesday May 31, 2005

10h30 – 11h15

Wan Fokkink (SENVA) — joint work with Jun Pang and Anton Wijs

Is Timed Branching Bisimilarity an Equivalence Indeed?

It is shown that timed branching bisimilarity as defined by van der Zwaag (2001) and Baeten & Middelburg (2002) is not an equivalence relation, in case of a dense time domain. An adaptation based on van der Zwaag's definition is proposed, and it is proved that the resulting timed branching bisimilarity is an equivalence indeed. In case of a discrete time domain, van der Zwaag's definition and our adaptation coincide.

11h15 – 12h30

A. H. J. Mathijssen (Eindhoven University of Technology) — joint work with Jan-Friso Groote and Muck van Weerdenburg

mCRL2: Towards a Practical Formal Specification Language

mCRL2 is a process algebra with data which tries to overcome a number of problems with the mCRL language, the most important one being practical use. In order to be suitable as a target language for translations of hierarchical Petri Nets, the process algebraic language is extended with true concurrency and local communication. To simplify the specification of data types and higher-order constructs, the data language is changed to higher-order algebraic specification extended with concrete data types. Finally, the intermediate format of linear process equations (LPEs) is extended with multi-actions, time and don't care values.

In parallel with the language, a toolset is being developed which uses the new LPE format. The additional goal of the toolset is to lower the threshold for new users. We try to achieve this by offering a graphical user interface that simplifies the process of analysing specifications.

Lunch

14h15 – 15h00

Mihaela Sighireanu (University of Paris 7) — joint work with Ahmed Bouajjani and Aurore Collomb

Open TReX: an open tool for symbolic reachability analysis

TREX is a tool for automatic analysis of automata-based models equipped with variables belonging to different infinite/finite domains and with parameters. These models are, at the present time, parametric (continuous-time) timed automata, extended with integer counters and finite-domain variables, and communicating through unbounded lossy FIFO channels and shared variables. From 1999, TREX has been applied with sucess to many case studies issued from telecommunications and scheduling.

However, its lack of flexibility and the interest of external researcher on specific technology implemented in TREX motivated the rebuilding of the TREX architecture in order to open it to external word.

This talk presents the theoretical basis and the implementation issues of the new architecture of TREX. This architecture makes room for further developments of TREX: analyse new models, use of external libraries for symbolic representation of configurations, new algorithms for acceleration of termination, and abstract/refine analysis. This work is currently done in the context of the national ACI Persee projet.

15h00 – 16h30

Radu Mateescu (SENVA)

On-the-Fly State Space Reductions for Weak Equivalences

On-the-fly verification of concurrent finite-state systems consists in constructing and analysing their underlying state spaces in a demand-driven way. This technique is able to detect errors effectively in large systems; however, its performance can still be increased by reducing the state spaces incrementally in a way compatible with the verification problem. In this talk, we present algorithms for three on-the-fly reductions of Labeled Transition Systems (LTSs), which preserve weak equivalence relations: tau-compression (collapsing of strongly connected components made of tau-transitions), tau-closure (transitive reflexive closure over tau-transitions), and tau-confluence (a form of partial order reduction). Each algorithm is described as a reductor module taking as input the successor function of an LTS and returning the successor function of the reduced LTS. The three reductors were implemented within the CADP toolbox using the generic OPEN/CAESAR environment, which makes them directly available for any on-the-fly verification tool compatible with the underlying reduction. Our experiments show that these reductors can improve significantly the performance of on-the-fly LTS generation, model checking, and equivalence checking.

Coffee Break

16h45 – 18h15

Hubert Garavel (SENVA)

Revisiting Sequential Composition in Value-Passing Process Algebras

Sequential composition seems to be the most obvious concept in process algebras. However, the various solutions adopted to model sequential composition in many existing process algebras leave to desire in terms of expressiveness and user-friendliness. We review sequential composition operators in various process algebras so as to make explicit the tradeoffs that remain hidden under well-known semantic definitions. We push forward unconventional ideas, which have been partly implemented in the E-LOTOS standard.

Dinner

21h15 – 22h15

Radu Mateescu and Frédéric Lang (SENVA)

Demonstration of the CADP toolbox

Wednesday June 1, 2005

9h00 – 9h45

David Champelovier (SENVA) — joint work with Adrian Curic, Nicolas Descoubes, Hubert Garavel, Christophe Joubert, Radu Mateescu, Irina Smarandache, and Gilles Stragier

Distributor: Parallel State Space Construction for Model-Checking

A major problem with model-checking is memory explosion. Several techniques exist to address this problem, but the state-space generation of large systems is still often limited by the amount of memory available. One solution is to design distributed algorithms that can be run on several machines, so as to take advantage of much more memory and computation power. In this talk, we present the Distributor tool which implements such a distributed algorithm.

9h45 – 10h35

Michael Weber (RWTH Aachen University) — joint work with Benedikt Bollig, Martin Leucker, Rafal Somla, Marcus Lindström, and Fredrik Holmen

Parallel Model Checking

We give a general introduction to parallel model checking, and describe its ingredients by example of algorithms for fragments of the mu-calculus. Our algorithms are based on characterizations of the model checking problem in terms of two-player games. In order to determine the winner of a game, we exploit the special structure of game boards for formulas with zero or just one level of alternation. Our algorithms are designed for easy and scalable distribution among several processors, to increase capacity of model checkers.

Coffee Break

11h00 – 12h05

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

Distributed on-the-fly verification of finite-state systems

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 present a combination of the above techniques in order to scale up their capabilities. The approach we adopt is based upon Boolean Equation Systems (BESs), which provide an elegant intermediate representation for verification problems defined on Labeled Transition Systems (LTSs), such as equivalence checking, tau-confluence reduction, model checking of alternation-free mu-calculus, and test-case generation. We describe DSolve, a new algorithm for distributed on-the-fly resolution of BESs, and explain how we employ it as computing engine for two on-the-fly verification tools developed within CADP using the OPEN/CAESAR environment: the equivalence checker BISIMULATOR and the partial order reductor TAU_CONFLUENCE. Experimental measures performed on clusters of machines show quasi-linear speedups and a good scalability of the distributed versions of these tools w.r.t. their sequential counterparts.

12h05 – 13h00

Michael Weber (RWTH Aachen University) — joint work with Stefan Schürmans

State Space Generation Revisited

We review approaches to state space generation and their suitability for a parallel setting. State space generators transform concise formal descriptions of models into transition systems suitable as input for state-based model checkers. The place near the core of their host tools places a number of requirements on these interpreters which we will highlight.

We investigate existing tools in this regard and then propose a virtual machine-based approach for state space generation. We address its advantages especially for parallel model checking tools.

13h00

Workshop Closing

Lunch