CONVECS Seminar 2013 
Scientific Program
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) ModelBased, 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 modelchecking 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 errorprone 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 nonexperts. 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, illformed 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 realworld 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 highlevel 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 Choreographybased 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 choreographybased 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 EA and ESi are traceequivalent for every environment E. While Si can be computed using elementary automata theory, the resulting algorithm suffers from the stateexplosion problem. We present a new, simple but subtle algorithm based on net unfoldings, a partialorder 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
SystemonChip (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 simulationbased 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 systemlevel 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 mucalculus. 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 : selfdeployment of arbitrary applications in the cloud
VAMP is an ALM solution dedicated to the efficient and reliable selfdeployment of any virtual application on multiple clouds. It is based on a decentralized algorithm in charge of postconfiguring 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 SelfDeployment Protocol for Cloud Applications 
15:15 
Coffee break and walk in the mountains 
18:02 – 18:39 
Jingyan JourdanLu 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 industrystandard 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 
19:10 – 19:30 
Eric
Léo 
19:30 – 19:40 
Soraya
Arias 
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 explicitstate 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 FaultTolerant Wormhole Routing Algorithm using Lotos NT
Cyberphysical systems (CPS) pose a demanding verification challenge due to their concurrent nature. One interesting CPS example is an onchip 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 faulttolerant routing algorithm for a twodimensional asynchronous networkonchip (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 DupuyChessa, Hubert Garavel, and Frédéric Lang) Nuclear Safety: a formal verification case study
Safety is a nonnegligible 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 bugfree. 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 subpart 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 valuepassing concurrent systems. It extends the alternationfree fragment of the modal mucalculus with datahandling features, generalized regular expressions on transition sequences, and fairness operators. We briefly describe the language and the procedure for onthefly evaluation of MCL formulas on labelled transition systems, and we outline the link between the fairness operators of MCL and generalized transitionbased Büchi automata. 
13:10 
Lunch 
Participants to the CONVECS seminar 2013. From left to right: Zhen Zhang, Frédéric Lang, Eric Léo, Xavier Etchevers, Radu Mateescu, Wendelin Serwe, Loïg Jezequel, Lina Ye, Jérôme Hugues, Fatma Jebali, Gwen Salaün, Fabrice Kordon, Jingyan JourdanLu, Abderahman Kriouile, Soraya Arias, Hugues Evrard, Raquel Oliveira, and Hubert Garavel.