Séminaire CONVECS 2015
Charavines (Isère)

Mercredi 27 Mai 2015

12h30

Déjeuner et début du séminaire

14h20 – 15h35

Eric Jenn (IRT Saint-Exupéry / Thales Avionics)

The INGEQUIP Project and the TwIRTee demonstrator

L'Institut de Recherche Technologique Saint-Exupéry est l’un des huit Instituts de recherche technologiques labellisés par l’État dans le cadre des Investissements d’Avenir. Il associe des partenaires publics et privés pour réaliser des activités de recherche et de maturation technologique dans trois domaines clés : les matériaux multifonctionnels à haute performance, les technologies pour l’aéronef plus électrique et les systèmes embarqués.

Dans ce cadre, le projet INGEQUIP se propose de faire évoluer les processus, méthodes et outils d'ingénierie utilisés pour le développement des équipements embarqués critiques. Trois axes sont retenus : les pratiques de développement conjoint matériel/logiciel,  l'exploitation de "composants" réutilisables, l'introduction de techniques de vérification et validation formelles. Dans cette présentation, on se propose de donner un aperçu des problématiques traitées et des activités conduites dans le projet INGEQUIP au travers d'un cas d'étude : le robot mobile "TwIRTee".

15h35 – 16h20

Wendelin Serwe (joint work with the CONVECS team)

LNT : présentation et nouveautés

LNT est un langage de description de systèmes asynchrones basé sur les calculs de processus, mais avec uns syntaxe proche des langages de programmation classiques. Dans cet exposé, nous présenterons brièvement le langage LNT, en mettant l’accent sur les nouveautés des années 2014 et 2015.

Pause café

16h45 – 17h30

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

Distributed LNT Compiler : génération automatique d'une implémentation distribuée à partir d'une spécification LNT

Le nouveau langage formel LNT permet de spécifier un système concurrent dans une syntaxe proche des langages de programmation classiques. La boîte à outils CADP offre des outils pour manipuler une spécification LNT, dont des outils de vérification formelle. En s'appuyant sur CADP, nous avons mis au point le nouveau compilateur DLC (Distributed LNT Compiler) qui produit automatiquement une implémentation distribuée en C à partir d'une spécification formelle LNT. L'un des principaux challenges est l'implémentation distribuée de l'interaction inter-processus de LNT : le rendez-vous multiple avec échange de données entre processus non déterministes.

Dans cette présentation, nous présentons une vue d'ensemble de la génération de code distribué effectuée par DLC. Nous donnerons un aperçu des subtilités du protocole qui assure les rendez-vous multiples, et nous exposons comment nous avons vérifié formellement ce protocole. Enfin, nous illustrons sur plusieurs exemples les performances atteintes par les implémentations produites, dont un cas d'étude sur le protocole de consensus Raft.

Cette présentation sera suivie d’une démonstration de l’outil.

17h35 – 18h05

Frédéric Lang

SVL : présentation et nouveautés

SVL (Script Verification Language) est un langage de script inclus dans CADP et développé depuis près de 15 ans. Il permet à l'utilisateur de decrier aisément des scénarios de vérification utilisant les outils de CADP, en s'abstrayant de la syntaxe en ligne de commande. SVL offre des fonctionnalités qui facilitent l'utilisation de certaines techniques de vérification, comme la vérification à la volée ou la vérification compositionnelle. Un compilateur associé traduit les scripts vers du code shell qui s'exécute automatiquement. Cet exposé présentera le langage SVL, et plus particulièrement les nouveautés, ajoutées au langage et au compilateur en 2014-2015, permettant notamment une présentation plus structurée des propriétés à vérifier.

18h05 – 19h10

Hubert Garavel

NUPN: A New Approach to Petri Nets

Petri nets can express concurrency and nondeterminism but not hierarchy. This article presents an extension of Petri nets, in which places can be grouped into so-called “units” expressing sequential components. Units can be recursively nested to reflect the hierarchical nature of complex systems. This model called NUPN (Nested-Unit Petri Nets) was originally developed for translating process calculi to Petri nets, but later found also useful beyond this setting. It allows significant savings in the memory representation of markings for both explicit-state and symbolic verification. Six tools already implement the NUPN model, which is also part of the next edition of the Model Checking Contest.

20h00

Dîner

Jeudi 28 Mai 2015

9h00 – 9h45

Fatma Jebali (joint work with Frédéric Lang)

The GRL framework for formal modeling and verification of GALS systems

The GALS (Globally Asynchronous, Locally Synchronous) paradigm is a prevalent approach to design distributed synchronous subsystems that communicate with each other asynchronously. The design of GALS systems is tedious and error-prone due to the complexity of architectures and high synchronous and asynchronous concurrency involved.

In this talk, we propose a model-based approach to formally verify such systems. Specifications are written in GRL (GALS Representation Language), dedicated to model GALS systems with homogeneous syntax and formal semantics. A translation from GRL to LNT makes possible the analysis of GRL specifications using the CADP toolbox.

9h45 – 10h35

Jingyan Jourdan-Lu (joint work with Radu Mateescu)

Equivalence checking for GALS systems

To employ equivalence checking to verify a system under design (SUD) corresponds to its specification, we must consider three issues: a sound equivalence relation, reasonable extraction of the external behavior from the model of the SUD, and well-qualified description of the desired system. In this talk, we present how these problems are handled for equivalence checking of globally asynchronous and locally synchronous (GALS) systems by using CADP. To be enough precise, we perform the equivalence checking modulo branching equivalence, which, however, is a challenge to the extraction of the external behavior as both the asynchronous and the synchronous features of the SUD are present in our model. To solve this problem, we show how and why external actions can be classified as visible and invisible and the invisible actions turn out to be real system delay. Another contribution of our work is the guidelines to describe properly the specification as an LNT model. To further illustrate our method, we give examples on how equivalence checking can be carried out to verify the designs of a network with reliable and non-reliable communication buffers.

Pause café

10h50 – 11h30

Eric Léo

Exemple d'application du langage GRL

Cet exposé propose un exemple d'utilisation du langage GRL. De la modélisation à la vérification avec CADP, il montre la mise en œuvre de la chaîne d'outil associée au langage GRL à travers un exemple complet de gestion de parking. Il explique comment cet exemple est traduit vers le langage LNT avant d'être vérifié en utilisant d'une part la logique temporelle via MCL et d'autre part la vérification par équivalence via un service.

11h30 – 12h00

Radu Mateescu

Recent Developments in MCL and EVALUATOR

MCL (Model Checking Language) is a temporal logic formalism designed for expressing properties of value-passing concurrent systems. MCL is an extension of the alternation-free modal mu-calculus with data-handling features, generalized regular expressions over transition sequences, and fairness operators. The language is equipped with EVALUATOR, an on-the-fly model checker operating on labelled transition systems (LTSs) represented implicitly using the OPEN/CAESAR graph exploration API of CADP.

We first give a brief introduction to MCL and its model checker, focusing on usability aspects. Then, we present some recent developments made in the MCL libraries and in the model checker, which aim at improving the performance of verification by reducing the LTS modulo a given property, and optimizing the memory consumption when checking properties on (large) execution traces.

12h00

Déjeuner

13h35 – 14h00

José Ignacio Requeno (joint work with Hubert Garavel and Radu Mateescu)

Model Checking for Probabilistic CTL and ACTL using XTL

Probabilistic temporal logics, such as PCTL (Probabilistic CTL), were designed for describing quantitative properties of concurrent system represented as Discrete-Time Markov Chains (DTMCs). PCTL is able to express properties concerning discrete time and probabilities, such as "the probability that an alarm is triggered at most 10 steps after the occurrence of an error is at least 95%".

XTL (eXecutable Temporal Language) is a functional-like graph exploration language designed for querying labeled transition systems (LTSs) represented in the BCG (Binary Coded Graphs) format of CADP. XTL allows the manipulation of states, transitions, and labels of the LTS, and also of the data values contained in labels. Temporal logic operators can be defined as recursive functions over state sets, and grouped into reusable libraries.

Recently, we defined two new XTL libraries encoding the PCTL and PACTL (Probabilistic Action-based CTL) temporal logics. These logics are interpreted over DTMCs extended with actions and data represented in the BCG format. Their operators can be freely mixed with other XTL constructs, yielding properties over data, actions, discrete time, and probabilities. Probabilistic temporal operators are defined using the LTS manipulation features of XTL, and underlying numerical computations (e.g., resolution of linear equations) are implemented externally in C. We illustrate the usage of these new XTL libraries for the quantitative analysis of the Philips' Bounded Retransmission Protocol described in LNT.

14h00 – 14h45

Abderahman Kriouile (joint work with Wendelin Serwe)

Using a Formal Model to Improve Verification of a Cache-Coherent System-on-Chip

In this talk we report about a case study on the functional verification of a System-on-Chip (SoC) with a formal model. Our approach improves industrial simulation-based verification techniques in two aspects. First, we suggest to use the formal model to assess the sanity of an interface verification unit. Second, we present a two-step approach to generate clever semi-directed test cases from temporal logic properties: model-based testing tools of the CADP toolbox generate system-level abstract test cases, which are then refined with a commercial Coverage-Directed Test Generation Tool into interface-level concrete test cases that can be executed at RTL level.

Applied to an AMBA 4 ACE-based cache-coherent SoC, we found that our approach helps in the transition from interface-level to system-level verification, facilitates the validation of system-level properties, and enables early detection of bugs in both the SoC and the commercial test-bench.

15h30

Balade autour du lac de Paladru

20h00

Dîner

Vendredi 29 Mai 2015

9h00 – 9h50

Alexandre Hamez (IRT Saint-Exupéry)

CAESAR.BDDSDD

CADP fournit caesar.bdd, un outil permettant d'analyser des propriétés structurelles et comportementales des Nested-Unit Petri Nets, en employant des techniques de model checking. Pour pallier les problèmes inhérents à cette technique, un portage de cet outil vers les SDD, une version améliorée des BDD, a été entrepris. Nous présenterons les techniques propres aux SDD mises en œuvre pour optimiser le processus de model checking, ainsi que les optimisations que le format NUPN permet.

9h50 – 10h35

Raquel Oliveira (joint work with Sophie Dupuy-Chessa, Gaëlle Calvary, Frédéric Lang, and Hubert Garavel, LIG)

Equivalence Checking for Comparing User Interfaces

Plastic User Interfaces (UIs) have the capacity to adapt to changes in their context of use while preserving usability.  This exposes users to different versions of UIs that can diverge from each other at several levels, which may cause loss of consistency. This raises the question of similarity between UIs. This paper proposes an approach to comparing UIs by measuring to what extent UIs have the same interaction capabilities and appearance. We use the equivalence checking formal method. The approach verifies whether two UI models are equivalent or not. When they are not equivalent, the UI divergences are listed, thus providing the possibility of leaving them out of the analysis. In this case, the two UIs are said equivalent modulo such divergences. Furthermore, the approach shows that one UI can contain at least all interaction capabilities of another. We apply the approach to a case study in the nuclear power plant domain in which several UI versions are analyzed, and the equivalence and inclusion relations are demonstrated.

Pause café

11h00 – 11h35

Lakhdar Akroun (joint work with Gwen Salaün)

Stability of Communicating Automata: Proofs and Undecidability

Recent software is mostly constructed by reusing and composing existing components. Software components are usually stateful and therefore described using behavioral models such as finite state machines. Asynchronous communication is a classic interaction mechanism used for such software systems. However, analyzing communicating systems interacting asynchronously via FIFO buffers is an undecidable problem, due to the unbounded buffers. In this talk we focus on the stability property. This property ensures that if the system is stable at a specific bound, then the behavior of the system remains the same for any larger bound. We will present in this talk the proof of stability and the proof of undecidability of the stability problem. The proof of undecidability is achieved by reduction from the halting problem of a Turing machine.

11h35 – 12h50

Gwen Salaün and Rim Abid

Reliable Deployment, Reconfiguration, and Control of Cloud Applications

Cloud applications consist of a set of interconnected software components distributed over several virtual machines. Setting up, (re)configuring, and monitoring these applications are difficult tasks, and involve complex management protocols. In this talk, we will first present two protocols for deploying and dynamically reconfiguring cloud applications, respectively. We will also present synthesis techniques for generating controllers in charge of coordinating autonomic managers and cloud applications. These approaches have been devised with the support of formal techniques and tools.

13h00

Déjeuner et fin du séminaire