Séminaire VASY 2008
Monthieux (Ain)

Mardi 10 Juin 2008

9h30

Accueil et café

10h35 – 11h25

Sylvain Rampacek (Université de Bourgogne)

Formal Modeling and Discrete-Time Analysis of BPEL Web Services

(joint work with Radu Mateescu)

Web services are increasingly used for building enterprise information systems according to the Service Oriented Architecture (SOA) paradigm. We propose in this paper a tool-equipped methodology allowing the formal modeling and analysis of Web services described in the BPEL language. The discrete-time transition systems modeling the behavior of BPEL descriptions are obtained by an exhaustive simulation based on a formalization of BPEL semantics using the Algebra of Timed Processes (ATP). These models are then analyzed by model checking value-based temporal logic properties using the CADP toolbox. The approach is illustrated with the design of a Web service for GPS navigation.

11h25  – 12h25

Valentin Cristea (University Polytehnica of Bucharest)

Resource management in distributed systems

First, we present  the Polytechnic University of Bucharest and its organization of teaching and research.

Then we give an overview of recent research projects, in particular scheduling challenges in grids. We address the (NP complete) problem of assigning a group of different task to resources so as to ensure successful completion of tasks and efficient resource usage.

Déjeuner

14h30 – 15h10

Damien Thivolle (joint work with Hubert Garavel)

Sam2Lotos

On présente un schéma de traduction du langage graphique SAM d'Airbus vers LOTOS dans le but de vérifier formellement une spécification écrite en SAM. L’exposé se termine par une courte démonstration.

15h10 – 16h00

Frédéric Lang

Enhancements of the Projector tool and report on experiments in compositional verification

Compositional verification is a way to avoid state explosion for the enumerative verification of complex concurrent systems. This approach assumes that the concurrent system under study can be expressed as a collection of communicating sequential processes, the behaviors of which are modeled as labeled transition systems (LTSs, for short). The sequential processes are composed in parallel, either in a flat or hierarchical manner. Compositional verification consists in replacing each sequential process by a minimized LTS, possibly restricted using interface constraints, in a way that preserves the properties to be verified on the whole system. In this talk, I will present the main tools contributing to compositional verification in CADP, with an emphasis on some of their recent improvements.

16h03 – 16h40

Radu Mateescu (joint work with Emilie Oudot)

Improved On-the-Fly Equivalence Checking using Boolean Equation Systems

Equivalence checking is a classical verification method for ensuring the compatibility of a finite-state concurrent system (protocol) with its desired external behavior (service) by comparing their underlying labeled transition systems (LTSs) modulo an appropriate equivalence relation.

The local (or on-the-fly) approach for equivalence checking combats state explosion by exploring the synchronous product of the LTSs incrementally, thus allowing an efficient detection of errors in complex systems. However, when the two LTSs being compared are equivalent, the on-the-fly approach is outperformed by the global one, which completely builds the LTSs and computes the equivalence classes between states using partition refinement.

In this paper, we consider the approach based on translating the on-the-fly equivalence checking problem in terms of the local resolution of a boolean equation system (BES). We propose two enhancements of the approach in the case of equivalent LTSs: a new, faster encoding of equivalence relations in terms of BESs, and a new local BES resolution algorithm with a better average complexity.

These enhancements were incorporated into the BISIMULATOR 2.0 equivalence checker of the CADP toolbox, and they led to significant performance improvements w.r.t. existing on-the-fly equivalence checking algorithms.

Pause café

17h05 – 17h45

Anton Wijs (joint work with Radu Mateescu)

Hierarchical Adaptive State Space Caching

In the past, several attempts have been made to deal with the state space explosion problem by equipping a depth-first search algorithm with a state cache, or by avoiding collision detection, thereby keeping the state hash table at a fixed size.

Most of these attempts are tailored specifically for depth-first search, and are often not guaranteed to terminate and/or to exhaustively visit all the states. In this paper, we propose a general framework of hierarchical caches which can also be used by breadth-first searches. We show under which circumstances termination of an exhaustive breadth-first search (which traverses all transitions of the state space) is still guaranteed.

We define several (static or adaptive) configurations of hierarchical caches and we study experimentally their effectiveness on benchmark examples of state spaces, using a generic implementation of the cache framework that we developed within the CADP toolbox.

17h45 – 18h30

Damien Thivolle (joint work with Radu Mateescu)

Evaluator 4

Le langage d'entrée de l'outil Evaluator 4 qui est une extension du langage d'entrée d’Evaluator 3.5 avec de nouvelles constructions qui permettent de manipuler des données dans les formules de logique temporelle. En fin d'exposé, il y aura une courte démonstration.

Diner

Mercredi 11 Juin 2008

9h00 – 10h10

Etienne Lantreibecq (STMicroelectronics)

Validation of the xSTream communication paradigm using CADP

In this talk, we present:

-      xSTream queues specificities and modeling

-      A potential problem with queue extension in memory

-      A problem with queues splitted over a shared communication medium

-      Network on chip modeling.

Pause café

10h35 – 11h20

Olivier Ponsini (joint work with Claude Helmstetter and Wendelin Serwe)

On the translation of SystemC/TLM into LOTOS

Transaction-Level Models (TLM) written in SystemC are used as reference models for embedded software validation and for hardware verification. There exists no authoritative semantics for these models, thus the SystemC simulation semantics is often used as a basis by formal approaches. In this presentation, we will discuss the definition in LOTOS of a semantics for SystemC/TLM that goes beyond the SystemC simulation semantics limits.

11h20 – 12h15

Wendelin Serwe (joint work with Hubert Garavel, Gwen Salaün, Yvain Thonnart, and Pascal Vivet)

Formal Verification of CHP Specifications with CADP – Illustration on an Asynchronous Network-on-Chip

Few formal verification techniques are currently available for asynchronous designs. In this paper, we describe a new approach for the formal verification of asynchronous architectures described in the high-level language CHP, by using model checking techniques provided by the CADP toolbox.

Our proposal is based on an automatic translation from CHP into LOTOS, the process algebra used in CADP. A translator has been implemented, which handles full CHP including the specific probe operator. The CADP toolbox capabilities allow the designer to verify properties such as deadlock-freedom or protocol correctness on substantial systems.

Our approach has been successfully applied to formally verify two complex designs.  In this paper, we illustrate our technique on an asynchronous Network-on-Chip architecture. Its formal verification highlights the need to carefully design systems exhibiting non-deterministic behavior.

Déjeuner

14h00 – 14h25

Yves Guerte

Software testing considerations

Quality analysis can be handled in practical point of view by combining rules of good behavior and systematic software testing and measurements.

14h25 – 15h15

Sylvain Robert (joint work with Hubert Garavel)

An overview of the VASY test framework

In an industrial context, VASY software components need to be intensively tested in order to ensure high quality requirements. This led to develop a test framework aiming to check non-regression and functional properties on CADP tools. In this presentation, we will describe the various kinds of tests that take place through the VASY test process.

Excursion à Pérouges et diner

Moments musicaux

22h10 – 24h00

Wendelin Serwe

Le basson

Présentation de l'instrument, de son histoire et de son rôle au sein de l’orchestre.

Jeudi 12 Juin 2008

9h00 – 10h10

Holger Hermanns (Saarland University and INRIA)

Probabilistic CEGAR

(joint work with Bjoern Wachter and Lijun Zhang)

Counterexample-guided abstraction-refinement (CEGAR) has been en vogue for the automatic verification of very large systems in the past years. When trying to apply CEGAR to the verification of probabilistic systems, various foundational questions and practical tradeoffs arise. This paper explores them in the context of predicate abstraction.

Pause café

10h30 – 11h30

Meriem Zidouni (Bull and INRIA)

Performance Evaluation of MPI Benchmarks on CC-DSM multiprocessor Architecture

(joint work with Ghassan Chehaibar, and Radu Mateescu)

The performance of a supercomputer depends on its hardware architecture as well as on the software implementation of the primitives needed for parallel programming. Therefore, in order to predict the performance of the MPI (Message Passing Interface) library on a multiprocessor architecture of type CC-DSM (Cache-Coherent Distributed Shared Memory) one must take into account the topology of processor interconnection, the cache coherency protocol, and the algorithms underlying the primitives of the library.

This paper presents the results of evaluating the performances of the ping-pong benchmark of MPI by using the theory of IMCs (Interactive Markov Chains) and one of its implementations available in the CADP verification toolbox.

The approach consists of the following steps: construction of a LOTOS model of the relevant hardware and software aspects of the system; functional verification of this model by means of bisimulation checking and model checking; and performance evaluation after extending the model with Markovian delays at appropriate places.

Using this approach, we were able to analyze the impact of various hardware and software parameters on the system behavior, and also to predict the performance of the MPI benchmark consistently w.r.t. the experimental measures.

11h30 – 12h20

Nicolas Coste (STMicroelectronics and INRIA)

Computing latencies in a probabilistic graph

(joint work with Holger Hermanns, Etienne Lantreibecq, and Wendelin Serwe)

This talk addresses the following questions:

-     How to generate a probabilistic graph from a LOTOS model (introduction of discrete time delays, new parallel composition operator for probabilistic transitions, new branching reduction operation, maximal progress algorithm in order to identify relevant equivalence classes).

-     How to compute latencies in such a graph.

Déjeuner

14h05 – 15h15

Radu Mateescu (joint work with Pedro Monteiro, Estelle Dumas, and Hidde de Jong)

Computation Tree Regular Logic for Genetic Regulatory Networks

Model checking has proven to be a useful analysis technique not only for concurrent systems, but also for the genetic regulatory networks (GRNs) that govern the functioning of living cells. The applications of model checking in systems biology have revealed that temporal logics should be able to capture both branching-time and fairness properties (needed for specifying multistability and oscillation properties, respectively).

At the same time, they should have a user-friendly syntax easy to employ by non-experts. In this report, we define Computation Tree Regular Logic (CTRL), an extension of CTL with regular expressions and fairness operators that attempts to match these criteria. CTRL subsumes both CTL and LTL, and has a reduced set of temporal operators indexed by regular expressions, inspired from the modalities of Propositional Dynamic Logic (PDL). We also develop a translation of CTRL into Hennessy-Milner Logic with Recursion (HMLR), an equational variant of the modal μ-calculus. This has allowed us to obtain an on-the-fly model checker with diagnostic for CTRL by directly reusing the verification technology available in the CADP toolbox.

We illustrate the application of the CTRL model checker by analyzing the GRN controlling the carbon starvation response of Escherischia coli.

Excursion et diner

Moments musicaux

22h00 – 24h00

Hubert Garavel

Les maîtres chanteurs de Nuremberg

Présentation d’une œuvre maîtresse de l’art allemand et notamment de l’ouverture de cet opéra de Richard Wagner.

Vendredi 13 Juin 2008

9h00 – 10h00

Frédéric Lang (joint work with Gwen Salaün, Rémi Hérilier, Jeff Kramer, and Jeff Magee)

Translating FSP into LOTOS and Networks of Automata

Many process calculi have been proposed since Robin Milner and Tony Hoare opened the way more than 25 years ago. Although these process calculi are based on the same kernel of operators, most of them are incompatible in practice. We aim at reducing the gap between process calculi, and especially making possible the joint use of underlying tool support. FSP is a widely-used calculus equipped with LTSA, a graphical and user-friendly tool. LOTOS is the only process calculus that has led to an international standard; It is supported by the CADP verification toolbox. We propose a translation of FSP sequential processes into LOTOS. Since FSP composite processes (i.e., parallel compositions of processes) are hard to encode directly in LOTOS, they are translated into networks of automata which are another input language accepted by CADP. Hence, it is possible to use jointly LTSA and CADP to validate FSP specifications. We implemented this approach in an automated translator tool.

10h00 – 10h40

Xavier Clerc (joint work with David Champelovier, Hubert Garavel, Frédéric Lang, and Wendelin Serwe)

Lnt2Lotos

LOTOS NT intends to be a user-friendly language for specifying communication protocols and asynchronous systems. We present the main features of this language and give an account of the current development status of Lnt2Lotos, a translator from LOTOS NT to LOTOS.

Pause café

11h05 – 12h25

Jan Stöcker (joint work with Frédéric Lang and Hubert Garavel)

Parallel Processes with Real-Time and Data: the ATLANTIF Intermediate Format

On the one hand, the modeling of real-life critical systems could benefit from high-level languages allowing to express and to manipulate complex data, many forms of concurrency, and real-time constraints. On the other hand, the verification of timed systems has been successfully applied on simple models, such as timed extensions of automata or Petri nets.

In order to bridge the gap between high-level languages allowing concise modeling of systems and low-level models on which efficient algorithms and tools have been designed, intermediate models are needed.

In this talk, the ATLANTIF intermediate model is presented, an extension with real-time and concurrency of the NTIF model proposed in 2002 by Garavel and Lang. After this, a tool implementation to translate from ATLANTIF into Timed Automata is described, allowing verification using the Uppaal tool, which underlines the usefulness of this intermediate format.

Déjeuner

14h05 – 14h30

Xavier Clerc (joint work with Frédéric Lang and Hubert Garavel)

The Fiacre language and its translation into LOTOS

The talk will begin with an overview of the Fiacre language presenting its three levels: types, processes, and components. Then, the translation from Fiacre into LOTOS will be discussed along both abstract (i.e. mapping of control structures) and concrete (i.e. compiler architecture) axes. Finally, a short demonstration will show how Fiacre allows to easily model imperative programs to be checked using the CADP toolbox.

14h30 – 15h00

Rémi Hérilier

Libmangle or how to preserve identifiers in translation processes

In translation processes, identifiers are an important part of the semantic. Keeping them unchanged may not be easy when there are important differences between the two languages. Libmangle introduces a generic way to solve this problem of identifiers preservation.

15h00 – 16h00

Romain Lacroix (joint work with Hubert Garavel, Rémi Hérilier, Marie Vidal, and the ATOLL/ALPAGE team of INRIA)

Porting the Syntax software to 64-bit computers

The Syntax software is used extensively to build compilers and translators by the Vasy team. Thus, it was necessary for Syntax to become 64-bit compliant and to generate 64-bit compliant code. During my presentation, I will discuss the techniques involved in porting Syntax to 64-bit computers, reporting about the various problems that had to be solved.

16h00 – 16h40

Damien Thivolle

Ruby

Nous présentons, dans ses grandes lignes, la syntaxe et les concepts de base du langage Ruby.

16h40

Clôture

exposé différé par manque de temps

Hubert Garavel (joint work with the VASY team)

Integrating Formal Methods within a Process Calculi Framework

The integration of different formal methods raises many issues. In this talk, I will review what has been achieved for the CADP (Construction and Analysis of Distributed  Processes) toolbox. Three levels of integration will be discussed: semantic models, at the lower level, and user interfaces and languages, at the higher level.

exposé différé par manque de temps

Wendelin Serwe

Object-Oriented Modeling: Overview of UML

UML (Unified Modeling Language) has been introduced as a support for object-oriented modeling and design in software engineering.  UML provides thirteen different kinds of diagrams allowing the description of a system from different points of views.  This overview talk presents commonly used diagrams (use case, class, object, activity, sequence, and state-transition diagrams), and OCL (Object Constraint Language), which allows to express constraints that cannot be represented directly in UML.