SENVA 2005
Workshop 

Workshop Programme
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 Scenariobased 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 scenariobased 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 musttransitions to get more progress
Abstractions yield small approximations of large state spaces. A common approach is to have both an overapproximation by maysteps (to prove safety properties) and an underapproximation by muststeps (to prove progress properties). However, due to the loss of information by approximation, this often yields less muststeps than required, blocking the proof of interesting progress properties. In this talk, accelerated muststeps will be introduced. These are muststeps 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 muststep "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 musttransitions, 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 EventBased Systems
In labeled transition system descriptions of eventbased 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 fluentbased lineartemporal 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 microelectronic 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 networkbased 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 ebusiness 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 tickactions. 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 breadthfirst 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 JanFriso 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 higherorder constructs, the data language is changed to higherorder algebraic specification extended with concrete data types. Finally, the intermediate format of linear process equations (LPEs) is extended with multiactions, 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 automatabased models equipped with variables belonging to different infinite/finite domains and with parameters. These models are, at the present time, parametric (continuoustime) timed automata, extended with integer counters and finitedomain 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) OntheFly State Space Reductions for Weak Equivalences
Onthefly verification of concurrent finitestate systems consists in constructing and analysing their underlying state spaces in a demanddriven 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 onthefly reductions of Labeled Transition Systems (LTSs), which preserve weak equivalence relations: taucompression (collapsing of strongly connected components made of tautransitions), tauclosure (transitive reflexive closure over tautransitions), and tauconfluence (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 onthefly verification tool compatible with the underlying reduction. Our experiments show that these reductors can improve significantly the performance of onthefly LTS generation, model checking, and equivalence checking. 

Coffee Break 
16h45 – 18h15 
Hubert Garavel (SENVA) Revisiting Sequential Composition in ValuePassing 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 userfriendliness. We review sequential composition operators in various process algebras so as to make explicit the tradeoffs that remain hidden under wellknown semantic definitions. We push forward unconventional ideas, which have been partly implemented in the ELOTOS 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 ModelChecking
A major problem with modelchecking is memory explosion. Several techniques exist to address this problem, but the statespace 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 mucalculus. Our algorithms are based on characterizations of the model checking problem in terms of twoplayer 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 onthefly verification of finitestate systems
The verification of concurrent finitestate 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 onthefly verification, partial order reduction, and distributed verification. However, practical experience has shown that none of these techniques alone is always sufficient to handle largescale 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, tauconfluence reduction, model checking of alternationfree mucalculus, and testcase generation. We describe DSolve, a new algorithm for distributed onthefly resolution of BESs, and explain how we employ it as computing engine for two onthefly 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 quasilinear 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 statebased 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 machinebased approach for state space generation. We address its advantages especially for parallel model checking tools. 
13h00 
Workshop Closing 

Lunch 
Some participants to the SENVA 2005 Workshop. From left to right: Frédéric Lang, Jeff Kramer, Hubert Garavel, David Champelovier, Jeff Magee, Gwen Salaün, Wendelin Serwe, Radu Mateescu, Wan Fokkink, Christophe Joubert, Michael Weber, Anton Wijs, Aad Mathijssen, and Jaco van de Pol.