CONVECS Seminar 2013
Col de Porte (Isère)

Monday, November 18, 2013

12:30

Lunch

14:00

Welcome

14:05 – 15:05

Jérôme Hugues (Institute for Space and Aeronautics Engineering, Toulouse)

Model-Based, Model checking: the missing bits

MDE provides an appealing framework for supporting engineering activities, from early design phases to acceptance tests; going through refinement, architectural and functional design down to code generation and V&V efforts. In this context, AADL – Architecture Analysis and Design Language – proposes a comprehensive framework for the modeling and analysis of complex embedded systems, with a large variety of tool support.  We note architectural models federate many concerns, some of which are highly interleaved. Therefore, one can no longer consider model-checking as the only V&V path.

In this talk, I'll illustrate several shortcomings and potential solutions in the application of verification techniques at large on AADL models. I'll present current discussion part of the AADL standardization committee to enrich Architecture Description Language with a Constraint language. The objective is to increase the coupling between modeling and verification. By making the verification part of extended semantics rules of an ADL, we control the patterns used to describe the system, ensuring designers respect process requirements, but also integrate V&V as part of the modeling effort. Thus, it provides a lean approach to V&V through MBSE.

15:05 – 15:40

Wendelin Serwe (joint work with the CONVECS team)

LNT : overview and summary of recent enhancements

In this talk, we present an overview of LNT (or LOTOS NT), the principal modeling language of the CADP toolbox. An particular focus is given to the enhancements and bug fixes brought over the last year.

15:40 – 16:05

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

GRL: a Formal Language for the Description of Globally Asynchronous Locally Synchronous Systems

A GALS (Globally Asynchronous, Locally Synchronous) system consists of synchronous components that evolve concurrently and interact with each other using asynchronous communication. Most formalisms and design tools support either the synchronous paradigm or the asynchronous paradigm but rarely combine both, thus requiring ad hoc and intricate modeling of GALS systems. In this talk, we present a new language, called GRL (GALS Representation Language) designed to efficiently model GALS systems for the purpose of formal verification. As such, GRL has a formal semantics. It combines the synchronous reactive model inspired by data flow languages and the asynchronous model inspired by process algebras. We present the basic concepts and the main constructs of the language together with some illustrative examples.

16:05

Coffee break

16:30 – 17:00

Lina Ye (joint work with Gwen Salaün)

Coverage Analysis of LNT

Designing and developing distributed and concurrent applications has always been a tedious and error-prone task. In this context, formal techniques and tools are of great help in order to specify such concurrent systems and detect bugs in the corresponding models. LNT is a recent specification language designed for formally modeling concurrent systems. LNT specifications can be analyzed using CADP model and equivalence checking tools. However, debugging such specifications is a real burden, in particular for non-experts. Indeed, beyond counterexamples provided as diagnostic by model checkers, there is no other technique for analyzing and refining LNT specifications. In this paper, we propose a new approach for coverage analysis of LNT. We define several coverage notions before showing how to instrument the specification without affecting original behaviors by proving their equivalence. Our approach helps one to find dead code, ill-formed conditional structures, and other errors in the specification, but also to improve the quality of a dataset of examples used for validation purposes. We have implemented a tool, CAL, for automating the verification of coverage analysis, and we applied it to several real-world case studies in different application areas.

17:00 – 17:25

Hugues Evrard

From a High Level Formal Model to a Distributed Implementation

My thesis consists in designing a tool which automatically generates, from a high-level formal model expressed in LNT, a distributed implementation which runs on separate machines while preserving the semantics of the formal model. I will present my ongoing work, focusing on the prototype tool under developpement. The main architecture of the prototype will be described, along with the working features. I will discuss how the remaining features can be added, and which set of features I consider reachable until the end of the thesis. Finally, related work on the same kind of tools will be briefly presented.

17:25 – 18:35

Gwen Salaün (joint work with Tevfik Bultan, Alexandre Dumont, Matthias Güdemann, Kaoutar Hafdi, Radu Mateescu, Meriem Ouederni, Pascal Poizat, and Lina Ye)

New Results on the Verification of Choreography-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 the following recent results:

·         We will first present a refinement of the synchronizability property which identifies systems for which interaction behavior remains the same when asynchronous communication is replaced with synchronous communication. We will also show how these results can be used for checking the compatibility of a set of asynchronously communicating components.

·         Second, we will introduce sufficient conditions for checking the repairability property, which indicates whether realizability can be enforced for choreography-based communicating systems using distributed controllers.

·         Third, we will present an approach for computing the degree of parallelism of BPMN processes using model checking techniques.

·         Last but not least, we will introduce and make a short demo of the VerChor plateform, which aims at assembling all the tools supporting the analysis and verification of choreography specifications.

19:30

Dinner

Tuesday, November 19, 2013

09:00 – 09:50

Loïg Jezequel (Technical University of Munich, Germany)

Computation of Summaries Using Net Unfoldings

We study the following summarization problem: given a parallel composition A = A1||...||An of labelled transition systems communicating with the environment through a distinguished component Ai, efficiently compute a summary Si such that E||A and E||Si are trace-equivalent for every environment E. While Si can be computed using elementary automata theory, the resulting algorithm suffers from the state-explosion problem. We present a new, simple but subtle algorithm based on net unfoldings, a partial-order semantics, give some experimental results using an implementation on top of MOLE, and show that our algorithm can handle divergences and compute weighted summaries with minor modifications.

10:00

Coffee break

10:30 – 11:15

Abderahman Kriouile (joint work with Radu Mateescu, Wendelin Serwe from Inria and Guilhem Barthes, Massimo Zendri from STMicroelectronics)

Introduction of Formal High level Modeling into SoC Validation: Illustration on ACE compliant Cache Coherence

System-on-Chip (SoC) architectures integrate now many different components, such as processors, accelerators, memory, and I/O blocks, some but not all of which may have caches. Because the validation effort with simulation-based validation techniques, as currently used in industry, grows exponentially with the complexity of the SoC, we investigate the use of formal verification techniques. More precisely, we use the CADP toolbox to develop and validate a generic formal model of an SoC compliant with the recent ACE specification proposed by ARM to implement system-level coherency.

This talk will present the work published in FMICS'2013 about formal analysis of the ACE Specification for Cache Coherent SoC and will also present the ongoing work on using the formal model to generate tests for the industrial test bench of the SoC.

11:15 – 12:10

Hubert Garavel

25 Years of Compositionality Issues in CADP: An Overview

CADP (Construction and Analysis of Distributed Processes – http://cadp.inria.fr) is a software toolbox that makes available many salient results of concurrency theory, such as process calculi, labeled transition systems, bisimulations, and modal mu-calculus. This talk discusses various compositionality issues faced when developing CADP and gives an account of the technical solutions found to address these issues.

12:10 – 12:17

Lina Ye

Demonstration of the VerChor tool

12:30

Lunch

14:06 – 15:00

Xavier Etchevers (Orange Labs, joint work with Gwen Salaün)

VAMP : self-deployment of arbitrary applications in the cloud

VAMP is an ALM solution dedicated to the efficient and reliable self-deployment of any virtual application on multiple clouds. It is based on a decentralized algorithm in charge of post-configuring and activating the elements that make up the application. This protocol has been verified within a collaboration between the Convecs team and Orange, in the context of OpenCloudware research project. This talk consists of a presentation of VAMP and the results of this collaboration.

15:05 – 15:12

Gwen Salaün

Verification of a Reliable Self-Deployment Protocol for Cloud Applications

15:15

Coffee break and walk in the mountains

18:02 – 18:39

Jingyan Jourdan-Lu

An Informal Introduction to CUDA C

CUDA is a parallel computing platform invented by NVIDIA for the software development on their graphics processing units (GPUs), which supports industry-standard programming languages, such as C, C++, and Fortran. In this presentation, we will explain the single instruction multiple threads (SIMT) programming model and, by detailing several basic examples written in CUDA C, we will focus on how the semantics of C language is extended to express the parallelism that can be exposed from GPU architecture.

18:40 – 19:10

 Hugues Evrard
Demonstration of the DLC (Distributed LNT Compiler) tool

19:10 – 19:30

Eric Léo
Overview of CADP Testing Tools

19:30 – 19:40

Soraya Arias
Web Maps for CADP Locations

19:40

Dinner

Wednesday, November 20, 2013

09:00 – 10:20

Fabrice Kordon (joint work with the LIP6/MoVe team)

Verification Approaches for Distributed Systems in LIP6/MoVe

This presentation will focus on some techniques dedicated to distributed systems and developped at LIP6/MoVe. We will provide a survey of these techniques together with experimentation results when available.

10:20

Coffee break

10:39 – 11:20

Frédéric Lang

Computing Labelled Transition System Equivalences with CADP

Graph equivalences are of key importance in explicit-state verification, where models are labeled transition systems.  These equivalences can be used to compare a model with respect to another one, or to reduce a model in order to decrease the verification cost. In this talk, I will consider graph equivalences in the context of CADP. I will present the equivalence relations available in CADP, as well as the tools that can be used to compute such equivalences. At last, I will present a few results about the latest developments in the Bcg_Min graph reduction tool.

11:20 – 11:55

Zhen Zhang (University of Utah, USA, joint work with Wendelin Serwe)

Modeling a Fault-Tolerant Wormhole Routing Algorithm using Lotos NT

Cyber-physical systems (CPS) pose a demanding verification challenge due to their concurrent nature. One interesting CPS example is an on-chip network that connects electronic control units in a modern vehicle. In this talk, I will present some experiences acquired from the modeling and verification of a fault-tolerant routing algorithm for a two-dimensional asynchronous network-on-chip (NoC) architecture using the LOTOS NT (LNT) modeling language. Several distinct features in LNT makes it possible to accurately model asynchronous handshakes and arbitrations in the NoC architecture. State space generation for the said NoC model is challenging due to large number of possible interleavings of concurrent transitions in the model. Techniques such as data abstraction and compositional aggregation have been experimented to successfully alleviate this problem.

11:55 – 12:27

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

Nuclear Safety: a formal verification case study

Safety is a non-negligible challenge in the nuclear domain. A field where a failure can have disastrous consequences, computer systems used in this domain (called critical systems) are expected to be more and more bug-free. It is with this goal that formal verification can complement classical testing, to ensure the quality of such systems. In this work, we study a sub-part of a nuclear power plant system's prototype, whose goal is to support the surveillance activity of operators in the control room. In order to support the formal verification of this prototype, the language LNT is used to model the behavior of the user interfaces, its interactions with the user, and part of the reactor core. The main goal is to verify properties in the system (using CADP toolbox), both at the core level and the user interface level, properties that are going to be expressed in temporal logics.

12:27 – 13:10

Radu Mateescu

Expressing fairness properties in MCL

MCL is a property description language for value-passing concurrent systems. It extends the alternation-free fragment of the modal mu-calculus with data-handling features, generalized regular expressions on transition sequences, and fairness operators. We briefly describe the language and the procedure for on-the-fly evaluation of MCL formulas on labelled transition systems, and we outline the link between the fairness operators of MCL and generalized transition-based Büchi automata.

 13:10

Lunch