Séminaire CONVECS 2012
Pont-en-Royans (Isère)

Lundi 5 Novembre 2012

 12h30

Déjeuner

14h00 – 14h45

Jérémy Buisson (Université de Bretagne Sud / VALORIA et Ecoles de St-Cyr Coëtquidan)

Vers un futur pi-ADL reconfigurable

Reconfigurer dynamiquement consiste à modifier un programme sans perdre le fil de son exécution tout en conservant le bénéfice de ce qu'il a déjà réalisé. Pour faire cela « en bon ordre » on trouve dans l'état de l'art deux grandes familles d'approches : se donner la capacité de traiter correctement l'état d'exécution ; ou bien trouver le bon moment (lorsque l'état est peu important) pour restructurer le programme. Dans mon exposé, je me concentrerai sur la première approche et je présenterai comment elle se transpose pour un langage comme pi-ADL. Il s'agit essentiellement de définir des opérateurs permettant l'introspection, à granularité fine, d'un état d'exécution qui aurait été capturé. Ce travail en cours ouvre plusieurs perspectives. Le langage pi-ADL couvre à la fois les aspects structurels et comportementaux. On peut donc espérer réconcilier les approches de reconfigurations structurelles et centrées état (comportementales). De plus, pi-ADL ayant fait l'objet de travaux sur l'expression et la vérification de propriétés, on peut espérer que cet héritage sera un pas supplémentaire en direction de reconfigurations vérifiées.

14h45 – 15h30

Frédéric Lang (joint work with the CONVECS team)

Le langage LNT

De type tutoriel, cet exposé cible principalement les utilisateurs potentiels du langage LNT, développé collectivement et progressivement depuis plus d'une décennie au sein des équipes-projets Inria VASY (2000-2011) puis CONVECS (2012-). Nous aborderons les trois grandes parties du langage LNT, qui sont les modules, les données (types et fonctions) et les processus. Enfin, nous donnerons quelques éléments concernant la sémantique formelle

et le compilateur.

Pause café

16h00 – 17h00

Gwen Salaün (joint work with Tevfik Bultan, Alexandre Dumont, Gregor Goessler, Matthias Güdemann, Meriem Ouederni, Pascal Poizat, and Nima Roohi)

Verification of Contract-based Communicating Systems

Choreographies are contracts specifying interactions among a set of services from a global point of view. These contracts serve as reference for the further development steps of the distributed system. Therefore their specification and analysis is crucial to avoid issues (e.g., deadlocks) that may induce delays and additional costs if identified lately in the design and development process. In this talk, we present a modular framework for performing automatically a number of crucial verification tasks on choreography specifications. Our framework accepts as input various interaction-based choreography description languages (e.g., BPMN 2.0 choreographies). In order to favour extensibility and reusability of our framework, we propose an intermediate format for representing choreography description languages. Another advantage of such an intermediate format is that it makes possible to use jointly several formal verification tools and techniques as back-end, provided that a connection to those tools exist. We have already developed a connection to the CADP verification toolbox via a translation from our intermediate format to the LNT process algebra, which is one of the CADP input specification languages. This enables the automated verification of some key analysis tasks (repairability, synchronizability, realizability, conformance, and control) using model and equivalence checking techniques.

17h00 – 17h45

Lina Ye

Pattern Diagnosability and Joint Diagnosability of Distributed Discrete Event Systems

Diagnosability is an important system property that determines at design stage how accurate any diagnostic reasoning can be on a partially observed system. A fault in a discrete-event system is diagnosable if and only if its occurrence can always be deduced from enough observations. It is well known that centralized diagnosability approaches lead to combinatorial explosion of the search space since they assume the existence of a monolithic model of the system. This is why very recently the distributed approaches for diagnosability began to be investigated, relying on local objects. On the other hand, diagnosis objectives are generalized from fault event to fault pattern that can represent multiple faults, repeating fault, sequences of significant events, repair of faults, etc. For pattern case, most existing approaches are centralized.  Thus we propose a new distributed framework for pattern diagnosability. We first show how to incrementally recognize patterns through extending subsystems. Then we propose a structure called regional pattern verifier that is constructed from the subsystem where the pattern is completely recognized before showing how to abstract just the necessary and sufficient diagnosability information to further save the search space. Then the global consistency checking is analyzed to verify pattern diagnosability. In this way, we avoid constructing global objects both for pattern recognition and for pattern diagnosability. The correctness of our distributed algorithm is theoretically proved and its efficiency experimentally demonstrated by the results of the implementation. Up to now, we assume that observations are centralized in distributed systems. Then we develop another approach for joint diagnosability for what we called self-observed distributed systems, where observable events can only be observed by its own component.  For this first we prove the undecidability of joint diagnosability with unobservable communication events by reducing Post's Correspondence Problem to an observation problem. Then we propose an algorithm to check a sufficient but not necessary condition of joint diagnosability.

Pause

18h00 – 18h30

Radu Mateescu (joint work with Gwen Salaün)

An Applied Pi-Calculus and its Translation to LNT

The pi-calculus is a formalism proposed by Milner and Parrow two decades ago for describing the behaviour of concurrent mobile processes. Despite numerous theoretical developments, relatively few attempts have been made to provide tools for analyzing pi-calculus specifications automatically. In this talk, we present PIC, an extension of (the finite control fragment of) the original pi-calculus with data types and functions described in the LNT language of CADP. For analyzing PIC specifications, we propose a translation from PIC to LNT, which encodes mobile communication using the static channels and value-passing synchronization features of LNT. This translation is automated by the PIC2LNT tool, which allows to analyze PIC specifications using all verification functionalities of CADP.

 19h30

Dîner

Mardi 6 Novembre 2012

9h00 – 10h00

Sophie Dupuy-Chessa (LIG)

Qualité des interfaces homme-machine plastiques

Avec l'informatique ambiante, la notion d'ordinateur disparaît. Les Interfaces Homme-Machine (IHM) s'exécutent sur des plates-formes diverses allant des grands murs aux objets augmentés en passant par les plus classiques smartphones. Dès lors, les IHM peuvent s'adapter à leur contexte d'usage ; elles deviennent plastiques. Cette plasticité doit s'accompagner du respect de leur qualité. Mais les critères d'ergonomie utilisés actuellement pour évaluer la qualité des IHM sont généraux : ils n'ont pas été pensés pour les IHM douées d'adaptation. Dans ce cadre, comment définir, vérifier et améliorer la qualité des IHM plastiques ?

Cet exposé introduira le concept de plasticité des IHM et la problématique de la qualité de ces interfaces. Il présentera les approches que nous mettons en oeuvre actuellement pour améliorer ces IHM. Il abordera aussi nos travaux précédents pour la vérification d'interfaces non adaptables au contexte d'usage.

10h00 – 10h30

Eric Léo (joint work with Frédéric Lang)

Introduction au contrôleur logique MIllenium

Cet exposé est une introduction au monde des contrôleurs logiques à travers l’exemple concret du contrôleur Millenium. Après avoir abordé les principales caractéristiques de ces automates programmables, l’exposé focalise sur leur programmation et, plus particulièrement, sur le langage des boîtes fonctionnelles, aussi appelé FBD (Function Block Diagram). Finalement, une piste pour la modélisation formelle de ces composants est présentée à travers une description en langage LNT.

Pause café

11h00 – 11h45

Massimo Zendri (STMicroelectronics)

Circuit Level Formal Verification in Industrial Environment

Hardware verification is an important task in the industrial design flow because errors in chip design are very costly to correct and must therefore be detected as early as possible. In this talk we present an overview of the verification of circuits in industry and of the main verification techniques employed, with a focus on model checking.

11h45 – 12h30

Wendelin Serwe (joint work with Hubert Garavel and Radu Mateescu)

Large-Scale Distributed Verification using CADP: Beyond Clusters to Grids

Distributed verification uses the resources of several computers to speed up the verification and, even more importantly, access large amounts of memory beyond the capabilities of a single computer. In this paper, we describe the distributed verification tools provided by the CADP (Construction and Analysis of Distributed Processes) toolbox, especially focusing on its most recent tools for management, inspection, and on-the-fly exploration of distributed state spaces. We also report on large-scale experiments carried out using these tools on Grid'5000 using up to 512 distributed processes.

Déjeuner

14h00 – 15h00

Radu Mateescu

Overview of MCL, a Data-Based Model Checking Language

For analyzing the dynamic behaviour of concurrent value-passing systems, classical temporal logics must be extended with data-handling primitives. Since the early days of formal verification, many such extensions were proposed, both in the linear/branching time and the state/action based settings. We present here MCL (Model Checking Language), an extension of the alternation-free modal mu-calculus with data-handling features, generalized regular expressions over transition sequences, and fairness operators. MCL was designed to allow a versatile and succinct formulation of temporal properties interpreted on labeled transition systems (LTSs) containing data values. We illustrate the usage of MCL by means of classical examples of properties (safety, liveness, fairness). We also describe the implementation of MCL provided by the EVALUATOR 4.0 model checker of the CADP verification toolbox, which evaluates an MCL formula on-the-fly on an LTS and also produces full diagnostics (witnesses and counterexamples), i.e., subgraphs of the LTS illustrating the truth value of the formula. We discuss the expressiveness and evaluation complexity of MCL, and we outline several directions of future work.

 15h30

Visite des Grottes de Choranche (prévoir des vêtements chauds)

18h00 – 19h00

Démonstration de CADP

 19h30

Dîner

Mercredi 7 Novembre 2012

09h00 – 09h45

Abderahman Kriouile (joint work with Wendelin Serwe)

Formal Modeling and Verification of an ACE Compliant Cache Coherent Interconnect

The complexity of systems on chip continues to increase, so that their architectures integrate now a significant number of computing units. Unfortunately, with current simulation-based validation techniques, the validation effort grows exponentially with the complexity of systems. Thus, a formal verification approach might be an alternative solution.

In this talk, we focus on system-level coherency, a major challenge faced in current architectures. We first present a formal LNT model of a cache coherent interconnect supporting ACE (AXI Coherency Extensions) protocol, a system-level coherency protocol proposed by ARM. Then we report about the use of CADP tools to simulate the behavior and to verify several properties.

09h45 – 10h15

Wendelin Serwe

How to Use Grid’5000

This talk briefly presents Grid’5000, a French national testbed for experimenting with cluster and grid computing. A particular focus is given to a tutorial on how to use Grid’5000 as an execution platform for the distributed verification tools of CADP.

Pause café

10h45 – 11h45

Hubert Garavel

An Early Feedback on Using PRISM

I will report about the use of the PRISM tool (Oxford University) for analyzing probabilistic and stochastic systems. I will discuss some design choices for the PRISM modelling language and will try to figure out how PRISM functionalities may be combined with those of CADP.

11h45 – 12h30

Hugues Evrard (joint work with Frédéric Lang)

Formal Verification of Multiway Synchronization Protocols

Correct design and implementation of distributed software systems is hard, particularly asynchronous systems, where communicating processes execute at independent speeds. To find bugs as early as possible in the software development cycle, formal models are advised, since they can be verified formally. Yet, there may still remain a semantic gap between a formal model and the actual distributed implementation, which is generally hand-written. To fill this gap, tools generating distributed code (or at least code prototypes) automatically from the formal model would be extremely useful.

In this paper, we consider models written in a subset of the language LNT, where processes interact using rendezvous on gates. Such interactions are in general nondeterministic, as each process may be simultaneously ready for interactions on several gates. Generating distributed code automatically thus requires an elaborate protocol that implements rendezvous semantics. We survey several protocols proposed in the literature and select three of them according to requirements about the nature of the code that we wish to generate. Since synchronization protocols are complex, we need guarantees on their correctness before starting to implement a code generator in the future. For each of these protocols, we thus propose a formal model written in the language LNT itself, and we verify the protocol correctness by model checking and equivalence checking using the CADP (Construction and Analysis of Distributed Processes) toolbox. This allows us to detect and fix one subtle bug in one of the studied protocols. We also discuss possible extensions of these protocols to handle the general parallel composition operator of LNT.

Déjeuner