Séminaire CONVECS 2014
Herbelon (Isère)

Lundi 23 Juin 2014

 12h30

Déjeuner

14h15 – 15h30

Laurence Pierre (TIMA, Grenoble)

Verification of Correctness and Safety Requirements for SoC Models

With the increasing complexity of modern Systems on Chip (SoC’s), the tendency has been to increase the level of abstraction at which the hardware is specified, and Electronic System Level (ESL) methodologies have emerged. SystemC TLM (Transaction-Level Modeling) is widely being adopted. TLM specifications tend to become golden reference models, hence the need for methodologies for guaranteeing their correctness is compelling.

In the assertion-based verification (ABV) framework, logic and temporal assertions written in languages like the IEEE standard PSL are used to capture the design intent. These requirements can be related to correctness or to safety/security issues. We propose an overview of ABV and we illustrate the capabilities of our ABV tool for complex hardware/software SoC's with industrial examples developed in recent projects: functional requirements (Astrium, Thales), safety-oriented requirements (Airbus).

15h30 – 16h15

Radu Mateescu (joint work with Anton Wijs, Technical University Eindhoven)

Mu-Calculus Fragments Adequate with Divergence-Sensitive Branching Bisimilarity

When analyzing the behavior of finite-state concurrent systems by model checking, one way of fighting state space explosion is to reduce the model as much as possible whilst preserving the properties under verification. We consider the framework of action-based systems, whose behaviors can be represented by labeled transition systems (LTSs), and whose temporal properties of interest can be formulated in modal mu-calculus (Lmu). First, we determine, for any Lmu formula, the maximal set of actions that can be hidden in the LTS without changing the interpretation of the formula. Then, we define Lmu-dsbr, a fragment of Lmu adequate w.r.t. divergence-sensitive branching bisimilarity. This enables one to apply the maximal hiding and to reduce the LTS modulo this relation when verifying any formula of Lmu-dsbr. We show that this fragment is equally expressive to mu-ACTL\X, the action-based counterpart of CTL extended with fixed point operators. The experiments that we performed on various examples of communication protocols and distributed systems show that this reduction approach can significantly improve the performance of verification.

Pause café

16h30 – 17h40

Hubert Garavel

Revisiting Sequential Composition in Process Calculi

Process calculi, such as CCS, CSP, LOTOS, ACP, etc., have been used for modeling complex, realistic applications, despite Robin Milner thought that process calculi such as CCS should be primarily used for proofs and theoretical studies, whereas programming languages with mutable variables and algorithmic control structures (such as the M language proposed by Milner in his "Communication and Concurrency" book) would be preferable for describing real-life systems. In this lecture, we present the design principles of LNT, which combines process calculi operators with algorithmic control structures in one single language, thus avoiding the duality between "calculi" and "languages" advocated by Milner.

17h40 – 18h30

Frédéric Lang (joint work with Hubert Garavel and Wendelin Serwe)

Le langage LNT

Dans cet exposé, je présenterai le langage LNT, ainsi que les vérifications statiques de code LNT ajoutées récemment dans le compilateur LNT2LOTOS.

18h30 – 19h10

Hugues Evrard

Distributed LNT Compiler (DLC): Automatic Distributed-Code Generation from Formal Models of Asynchronous Concurrent Systems

Formal models of asynchronous concurrent systems are useful for verification purposes: for instance, a system can be modeled in LNT and verified using CADP tools. However, a hand-written implementation based on the model can contain semantic gaps with the formal model, hence ruining the verification effort. In this talk we present DLC (Distributed LNT Compiler), a tool which automatically generates a distributed implementation from a LNT model of a distributed system. After an overview of DLC, we focus on the hook functions which gives the final user a way to make the program generated by DLC interact with external software.

19h10 – 19h25

Hugues Evrard

An Overview of the RAFT Protocol

Les protocoles de consensus sont une des clés de voute pour construire des systèmes distribués résistants aux pannes. Le protocole Paxos (Lamport, 1989) a longtemps fait office de solution de référence, malgré sa complexité notoire. RAFT (Ongaro, Ousterhout, 2014) est un nouveau protocole de consensus conçu pour être simple à comprendre, ce qui est non négligeable pour obtenir des implémentations correcte. Nous utilisons RAFT comme cas d'étude : nous modélisons d'abord formellement RAFT en LNT, puis nous utilisons DLC pour obtenir une implémentation distribuée. Nous nous servons des fonctions crochets (hook functions) pour pouvoir interagir avec des programmes externes. Cette étude de cas permet enfin d'avoir un aperçu des performances atteignable par les implémentations produites par DLC..

Pause

19h30 – 20h00

Soraya Arias

An Introduction to the GIT Environment

We present briefly the history of the GIT environment for collaborative development, its main functionalities, and its interaction with other work environments.

 20h15

Dîner

 21h30

Hubert Garavel

Chaconnes et Passacailles

Un exposé sur l’histoire de la musique.

Mardi 24 Juin 2014

9h00 – 10h15

Matthias Güdemann (Systerel, Aix-en-Provence)

Industrial Formal Methods

The application of formal methods in industry has a lot of potential, and Systerel successfully applies formal methods in different domains, using different approaches.

One currently ongoing development is a state-of-the-art model checker based on SAT solving, which allows for verification of real-world systems, supporting C, Ada and SCADE. Using such a tool in SIL4 development imposes additional, different requirements than for model checkers in general.

A very important part of software and systems engineering is the correctness of requirements. This avoids many problems already in early phases of the development, eliminating costly fixing of errors in later phases of the development. The Rodin platform and the Event-B formal method are well adapted to support formal analyses on system level and allow for validation of functional correctness.

10h15 – 10h45

Raquel Oliveira (joint work with Hubert Garavel and Frédéric Lang)

Formal Verification of User Interfaces Using the Power of a Recent Tool Suite

This talk presents an approach to verify the quality of user interfaces in the context of a critical system for nuclear power plants. The technique uses formal methods to perform verification. The user interfaces are described by means of a formal language called LNT and ergonomic properties are formally defined using temporal logics written in MCL language. Our approach moves towards the powerfulness of formal verification of user interfaces, thanks to recent tools to support the process.

Pause café

11h00 – 11h50

Gwen Salaün (joint work with Lina Ye)

Stability of Asynchronously Communicating Systems

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. A typical approach is to check whether the system is bounded, and if not, the corresponding state space can be made finite by limiting the presence of communication cycles in behavioral models or by fixing buffer sizes. In this paper, we focus on infinite systems and we do not restrict the system by imposing any arbitrary bounds. We introduce a notion of stability and prove that once the system is stable for a specific buffer bound, it remains stable whatever larger bounds are chosen for buffers. This enables us to check certain properties on the system for that bound and to ensure that the system will preserve them whatever larger bounds are used for buffers. We also prove that computing this bound is undecidable but show how we succeed in computing these bounds for many examples using heuristics and equivalence checking.

11h50 – 12h23

Lina Ye (joint work with Radu Mateescu and Gwen Salaün)

Quantifying the Parallelism in BPMN Processes using Model Checking

A business process is a set of structured, related activities that aims at fulfilling a specific organizational goal for a customer or market. An important metric when developing a business process is its degree of parallelism, i.e., the maximum number of tasks that are executable in parallel in that process. The degree of parallelism determines the peak demand on tasks, providing a valuable guide for the problem of resource allocation in business processes. In this work, we investigate how to automatically measure the degree of parallelism for business processes, described using the BPMN standard notation. We first present a formal model for BPMN processes in terms of Labelled Transition Systems, which are obtained through process algebra encodings. We then propose an approach for automatically computing the degree of parallelism by using model checking techniques and dichotomic search. We implemented a tool for automating this check and we applied it successfully to more than one hundred BPMN processes.

12h23 – 13h10

Rim Abid

Formal Design of Dynamic Reconfiguration Protocol for Cloud Applications

Cloud applications are complex applications composed of a set of interconnected software components running on different virtual machines, hosted on remote physical servers. Deploying and reconfiguring this kind of applications are very complicated tasks especially when one or multiple virtual machines fail when achieving these tasks. Hence, there is a need for protocols that can dynamically reconfigure and manage running distributed applications. In this presentation, we present a novel protocol, which aims at reconfiguring cloud applications. This protocol is able to ensure communication between virtual machines and resolve dependencies by exchanging messages, (dis)connecting, and starting/stopping components in a specific order. The interaction between machines is assured via a publish-subscribe messaging system. Each machine reconfigures itself in a decentralized way. The protocol supports virtual machine failures, and the reconfiguration always terminates successfully even in the presence of a finite number of failures. Due to the high degree of parallelism inherent to these applications, the protocol was specified using the LNT value-passing process algebra and verified using the model checking tools available in the CADP toolbox. The use of formal specification languages and tools helped to detect several bugs and to improve the protocol.

 13h10

Déjeuner

14h15 – 14h50

Hubert Garavel (joint work with Alexander Graf-Brill and Holger Hermanns)

A Model-Based Certification Framework for the EnergyBus Standard

The EnergyBus is an upcoming industrial standard for electric power transmission and management, based on the CANopen field bus. This paper reviews the particularities of the EnergyBus architecture and reports on the application of formal methods and protocol engineering tools to build a model-based conformance testing framework that is considered to become part of the certification process for EnergyBus-compliant products.

14h50 – 15h30

Wendelin Serwe (joint work with Zhen Zhang, Wendelin Serwe, Jian Wu, Tomohiro Yoneda, Hao Zheng, and Chris Myers)

Formal Analysis of a Fault-Tolerant Routing Algorithm for a Network-on-Chip

A fault-tolerant routing algorithm in Network-on-Chip (NoC) architectures provides adaptivity for on-chip communications. This paper proposes an extension to the multiflit wormhole routing algorithm for the link-fault tolerant NoC architecture. Adding fault-tolerance adaptivity to a routing algorithm increases its design complexity and makes it prone to deadlock and other problems if improperly implemented. Formal verification techniques are needed to check the correctness of the design. We describe several lessons learned during the process of constructing a formal model of this routing architecture. Using the CADP toolbox, we are able to verify deadlock freedom and the property of single link-fault tolerance of the routing algorithm on a two-by-two mesh.

15h30 – 16h20

Abderahman Kriouile (joint work with Wendelin Serwe)

Model-Based Testing of SoCs: from theory to practice

Functional verification is a major bottleneck in current System-on-Chip (SoC) design methodologies. Model-based testing is one of the promising technologies to meet the challenges imposed on functional verification. In model-based testing, a design under verification (DUV) is tested for compliance with a formal model of the DUV's required behavior. Because such a model is a good basis for the automatic and reproducible generation of large volumes of high-quality test cases, this enables effective test automation beyond the simple automatic execution of manually crafted test scripts, which is the current state of practice.

We will present model-based testing theory for non-deterministic state-based systems, where models are expressed as labelled transition systems, and compliance between the DUV and the model is defined with the `ioco' implementation relation.

We also present the benefits of applying model-based testing to an ACE-based cache coherent SoC. Using a previously developed formal model, we verify global properties of the system using model checking, and generate abstract tests using counter-examples provided by the model checker. We found that our approach significantly improves the test coverage, and enables to detect bugs in earlier development stages.

Pause café

 16h00

Balade autour du lac de Monteynard et sur la passerelle de l’Ebron (prévoir des chaussures de marche, coupe-vent et bouteille d’eau)

 19h00

Dîner

Mercredi 25 Juin 2014

09h10 – 10h25

Lom Messan Hillah (LIP6, Paris)

Formal Methods in Model-Driven Development and Model-Driven Development in Formal Methods: Practice makes a Better Bridge

In this talk I will present the progress and the challenges that we have been experiencing in designing formal concepts for model-driven development, and in harnessing formal methods to support model-driven development. To illustrate these approaches, this talk will feature two important case studies that have been carried out over the past few years, and are still subject to investigation. One is about the ISO/IEC SC7 WG19 standardization effort on Petri nets, and the other about automated test generation for Service Oriented Architectures in the cloud, in the MIDAS European project. This is a joint work with ISO/IEC SC7 WG19, Simple Engineering France and UPMC.

Pause café

11h15 – 12h00

Fatma Jebali

GRL: A step towards automatic verification framework for GALS systems

A wide range of industrial applications represent instances of GALS (Globally Asynchronous, Locally Synchronous) systems composed of several synchronous systems that execute concurrently and communicate asynchronously. The use of formal methods in the design process helps designers to master the complexity of their systems and to build strong confidence in their correctness.

GRL is a new formal language to specify GALS systems for the purpose of formal verification intended to enhance design process of GALS systems with efficiency and correctness. This talk deals with the main syntactic and semantic concepts of GRL together with some insights into its translation to LNT.

12h00 – 12h30

Eric Léo (joint work with Fatma Jebali)

Application du langage GRL

Cet exposé présente la chaîne d'outils conduisant de la spécification d'un réseau de contrôleurs logiques à sa validation grâce aux outils de CADP. Il montre particulièrement l'intégration et l'utilisation du langage GRL dans cette chaîne. Par ailleurs, la modélisation via ce langage et la traduction vers le langage cible LNT sont traitées à travers un exemple détaillé.

 12h30

Déjeuner et fin du séminaire