Séminaire CONVECS 2018
Dullin (Savoie)




Programme scientifique

Mardi 10 Juillet 2018

12h00 – 14h00

Déjeuner et début du séminaire

14h00 – 15h00

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

The CAPHCA Project, or How to Be Fast and Reasonable


CAPHCA (Critical Applications on Predictable High-Performance Computing Architectures) is a collaborative project led by IRT Saint Exupéry, with the general objective of providing methods and tools to achieve performance and determinism on using modern, high-performance, multi-core, and FPGA-enabled Systems-on-Chip. We present the objectives and current activities of the project, with a focus on three topics: FlexPRET and ForeC, analysis of WCET (Worst-Case Execution Time), and analysis of interferences.

15h00 – 16h00

Hubert Garavel

The 4th Rewrite Engines Competition


Many specification and programming languages have adopted term rewriting and pattern matching as a key feature. However, implementation techniques and observed performance greatly vary across languages and tools. To provide for an objective comparison, we developed an open, experimental platform based upon the ideas of the three Rewrite Engines Competitions (2006, 2008, and 2010), which we significantly enhanced, extended, and automated. We used this platform to benchmark interpreters and compilers for a number of algebraic, functional, and object-oriented languages, and we report about the results obtained for CafeOBJ, Clean, Haskell, LNT, LOTOS, Maude, mCRL2, OCaml, Opal, Rascal, Scala, SML (MLton and SML-NJ), Stratego/XT, and Tom.

16h00 – 16h30

Pause café

16h30 – 17h00

Lina Marsso

An Autonomous Car Model for the Illustration of a GALS Testing Approach


GALS (Globally Asynchronous, Locally Synchronous) systems are increasingly spreading with the development of the Internet of Things (IoT). GALS systems are intrinsically complex, because the simultaneous presence of synchronous and asynchronous aspects makes their development and debugging difficult. To ensure the reliability and functional safety of a GALS system, it is therefore necessary to adopt rigorous design methodologies, based on formal methods assisted by efficient validation tools.


In this talk, we present ongoing work on formal modeling of a GALS system, describing the interactions between an autonomous car and its environment. Our aim is to come up with a realistic example to illustrate a testing approach for GALS systems, we are currently designing, combining techniques from asynchronous and synchronous model based testing. We follow an asynchronous approach to generate conformance test cases for the complete GALS system, and then use these test cases to improve the unitary tests of the synchronous blocks composing the GALS system.

17h00 – 17h30

Ajay Muroor-Nadumane

Trustworthy Composition and Deployment of IoT Applications


The Internet of Things (IoT) has gained tremendous momentum in the recent years - large scale deployments are becoming increasingly common. The talk proposes mechanisms for reliable IoT service composition and deployment. Users can connect or combine various IoT objects to build an IoT service composition. A composition needs to be compatible, for a service to function optimally. To achieve this, we model the IoT objects using an interface description model. Further, we propose compatibility notions to check the validity of the composition. Finally, the validated composition is deployed respecting the dependencies among the objects on a Software-Defined-Networking platform, thereby ensuring correct and reliable composition and deployment of an IoT service.

17h30 – 18h00

Umar Ozeer

Resilience of Stateful IoT Applications in the Fog


Fog computing provides computing, storage and network resources at the edge of the network, near the physical world. Subsequently, end devices nearing the physical world can have interesting properties such as short delays, responsiveness, optimized communications or privacy. However, these end devices have low stability and are prone to failures. There is consequently a need for fault-tolerant management protocols for IoT applications in the Fog. The design of such solutions is complicated due to the specificities of the environment, i.e.,

        1. High heterogeneity in terms of functions, communication models, network, processing and storage capabilities
        2. Dynamic infrastructure where entities join and leave without synchronization

        3. Cyber-physical interactions which introduce non-deterministic and physical world's space and time dependent events.
A fault tolerance approach taking into account these three characteristics of the Fog-IoT environment is proposed. Fault tolerance is achieved by saving the state of the application in an uncoordinated way. When a failure is detected, notifications are propagated to limit the impact of failures and dynamically reconfigure the application. Data saved during the state saving process are used for recovery, taking into account consistency with respect to the physical world. The approach is experimented on a smart home platform.



Mercredi 11 Juillet 2018

09h00 – 10h15

Yliès Falcone (CORSE project-team, Inria and LIG)

Some Recent Work on the Runtime Monitoring of Systems 


In this talk, I will present some recent contributions to the definition of runtime monitoring techniques. First, I will overview a line of work on the definition of runtime enforcement monitors for timed properties, that is monitors that ensure the correctness of an execution with respect to a property described by a timed automaton. Second, I will present work on defining runtime verification for decentralized systems and its recent application to the monitoring of a smart-home environment. Finally, if time permits, I will present the recently introduced interactive runtime verification that combines runtime verification and interactive debugging so as to facilitate the discovery and explanation of bugs.

10h15 – 10h45

Pause café

10h45 – 11h30

Gwen Salaün

Quantifying the Similarity of Non-bisimilar LTSs


Designing and developing distributed software has always been a tedious and error-prone task, and the ever increasing software complexity is making matters even worse. Although we are still far from proposing techniques and tools avoiding the existence of bugs in a software under development, we know how to automatically chase and find bugs that would be very difficult, if not impossible, to detect manually.


Model checking is an established technique for automatically verifying that a model (Labelled Transition System), obtained from higher-level specification languages such as process algebra, satisfies a given temporal property. Equivalence checking is an alternative solution to model checking and is very helpful to check that two models (requirements and implementation for instance) are equivalent from the point of view of an external observer. When these models are not equivalent, the checker returns a Boolean result with a counterexample, which is a sequence of actions leading to a state where the equivalence relation is not satisfied. However, this counterexample does not give any indication of how far the two LTSs are one from another. One can wonder whether they are almost identical or totally different, which is quite different from a design or debugging point of view.


The objective of this work is to provide a set of metrics for measuring the difference / distance between two LTS models. This measure takes as starting point the notion of bisimulation defined by Milner and focuses on non-bisimilar states. In this presentation, I will first present the different notions we use for defining a notion of similarity between two LTSs. In a second step, I will present a prototype implementation and several examples to illustrate the results automatically computed by this approach.

11h30 – 12h05

Wendelin Serwe (joint work with Lina Marsso and Radu Mateescu)

TESTOR: A Modular Tool for On-the-Fly Conformance Test Case Generation


We present TESTOR, a tool for on-the-fly conformance test case generation, guided by test purposes. Concretely, given a formal specification of a system and a test purpose, TESTOR automatically generates test cases, which assess using black box testing techniques the conformance to the specification of a system under test. In this context, a test purpose describes the goal states to be reached by the test and enables one to indicate parts of the specification that should be ignored during the testing process. Compared to the existing tool TGV, TESTOR has a more modular architecture, based on generic graph transformation components , is capable of extracting a test case completely on the fly, and enables a more flexible expression of test purposes, taking advantage of the multiway rendezvous. TESTOR has been implemented on top of the CADP verification toolbox, evaluated on three published case-studies and more than 10000 examples taken from the non-regression test suites of CADP.

12h05 – 14h00


14h00 – 14h45

Hubert Garavel

Verification of an Industrial Asynchronous Secure Element using CADP


It is currently estimated that the number of connected objects in the Internet of Things (IoT) will reach between 50 and 80 billions in 2020. A study carried out by Hewlett Packard in 2015 (IoT Security Research) indicates serious security issues present in the IoT (90% of the connected objects collect data that are exposed, 80% of objects do not use identification or authentification mechanisms, and 70% do not encrypt the data transmitted). The recent attacks published that exploit connected objects (e.g., cameras or sensors) confirm the situation and the danger caused by their vulnerabilities.


A possible solution for securing the IoT is the endpoint security, which consists in securing each connected object by equipping it with a secure element, i.e., a microcontroller able to perform cryptography and to store secret data. This kind of microcontrollers can be successfully implemented using asynchronous circuits, which have (very) low power consumption and energy management functions adapted to the IoT requirements. In this talk, we will show how formal methods and verification can help in devising such circuits, by illustrating the usage of LNT and CADP in modelling and analyzing asynchronous circuits devised by Tiempo in the SecurIoT-2 project.

14h45 – 15h30

Frédéric Lang (joint work with Garavel and Laurent Mounier)

Compositional Verification in Action


Concurrent systems are intrinsically complex and their verification is hampered by the well-known ``state-space explosion'' issue. Compositional verification is a powerful approach, based on the divide-and-conquer paradigm, to address this issue. Despite impressive results, this approach is not used widely enough in practice, probably because it exists under multiple variants that make knowledge of the field hard to attain. In this talk, we highlight the seminal results of Graf & Steffen and propose a survey of compositional verification techniques that exploit (or not) these results.

15h30 – 16h00

Pause café

16h00 – 16h45

Radu Mateescu

Practical Handling of Fairness in MCL


One of the most common, and desirable, liveness properties of concurrent systems is inevitability (e.g., after a message has been sent, it will be inevitably received). Unfortunately, in many cases, due to unreliable components in the system (e.g., lossy communication channels), inevitability properties do not hold. One way to cope with this issue is to use fairness constraints, which restrict the evaluation of the inevitability property to those sequences satisfying a given fairness constraint (e.g., if an action is continuously enabled, it will be executed infinitely often).


We review in this talk the classical notions of fairness (unconditional, strong, and weak) originally defined in the state-based setting, and formulate them in the action-based, branching-time setting using MCL operators. We also propose a definition in MCL of inevitability extended with fairness constraints, and we compare it with the notion of fair reachability that is usually used when inevitability does not hold. We illustrate the usage of inevitability with fairness constraints on the Bounded Retransmission Protocol designed by Philips. Finally, we outline several perspectives for future work on this topic.

17h30 – 20h00

Balade au bord du lac d’Aiguebelette



Jeudi 12 Juillet 2018

9h00 – 10h00

Viet Anh Nguyen (IRT Saint-Exupéry)

Cache-conscious Off-line Real-time Scheduling for Multi-core Platforms: Algorithms and Implementation


Nowadays, real-time applications are more compute-intensive as more functionalities are introduced. Multi-core platforms have been released to satisfy the computing demand while reducing the size, weight, and power requirements. The most significant challenge when deploying real-time systems on multi-core platforms is to guarantee the real-time constraints of hard real-time applications on such platforms. This is caused by interdependent problems, referred to as a chicken and egg situation, which is explained as follows. Due to the effect of multi-core hardware, such as local caches and shared hardware resources, the timing behavior of tasks are strongly influenced by their execution context (i.e., co-located tasks, concurrent tasks), which are determined by scheduling strategies. Symmetrically, scheduling algorithms require the Worst-Case Execution Time (WCET) of tasks as prior knowledge to determine their allocation and their execution order. Most schedulability analysis techniques for multi-core architectures assume a single WCET per task, which is valid in all execution conditions. This assumption is too pessimistic for parallel applications running on multi-core architectures with local caches. In such architectures, the WCET of a task depends on the cache contents at the beginning of its execution, itself depending on the task that was executed before the task under study.


In this thesis, we address the issue by proposing scheduling algorithms that take into account context-sensitive WCETs of tasks due to the effect of private caches. We propose two scheduling techniques for multi-core architectures equipped with local caches. The two techniques schedule a parallel application modeled as a task graph, and generate a static partitioned non-preemptive schedule. We propose an optimal method, using an Integer Linear Programming (ILP) formulation, as well as a heuristic method based on list scheduling. Experimental results show that by taking into account the effect of private caches on tasks’ WCETs, the length of generated schedules are significantly reduced as compared to schedules generated by cache-unaware scheduling methods. Furthermore, we perform the implementation of time-driven cache-conscious schedules on the Kalray MPPA-256 machine, a clustered many-core platform. We first identify the practical challenges arising when implementing time-driven cache-conscious schedules on the machine, including cache pollution cause by the scheduler, shared bus contention, delay to the start time of tasks, and data cache inconsistency. We then propose our strategies including an ILP formulation for adapting cache-conscious schedules to the identified practical factors, and a method for generating the code of applications to be executed on the machine. Experimental validation shows the functional and the temporal correctness of our implementation. Additionally, shared bus contention is observed to be the most impacting factor on the length of adapted cache-conscious schedules.

10h00 – 10h30

Pierre Bouvier

Proposition d'amélioration de la gestion des chemins d'accès par la bibliothèque C standard


Pour manipuler les chemins d'accès, les développeurs C doivent utiliser des primitives de la bibliothèque standard du langage C, qui sont basename, dirname et realpath, ainsi que les fonctions de manipulation de chaînes.


Cet exposé présente une étude critique de ces primitives, une analyse présentant les opérations de manipulation de chemins les plus fréquentes, ainsi qu'une comparaison avec les autres langages afin de montrer ce qui peut être fait afin d'améliorer la bibliothèque standard du langage C.

10h30 – 11h00

Pause café

11h00 – 11h20

Lucie Colpart

Analysis of the Current CADP Web Site and Redesign Propositions


CADP (Construction and Analysis of Distributed Processes) is a verification toolbox developed by the CONVECS team. The access and documentation of this toolbox is available on the Web site http://cadp.inria.fr. This presentation discusses the current CADP Web site from different points of view: user's usages, navigation efficiency, responsive Web design, and visual design. It offers a preliminary study with new design ideas, focused on CADP user's experience in several environments (smartphone, computer).


We will first discuss which functionalities could be redesigned and which ones could be added, in order to benefit the users. Then, we will present a model of a new navigation system (mobile adaptable). Finally, we will propose some ideas of new design templates to discuss with the CONVECS team members.

11h20 – 12h05

Gianluca Barbon

Counterexample Simplification for Liveness Property Violation


Model checking techniques verify that a model satisfies a given temporal property. When the model violates the property, the model checker returns a counterexample, which is a sequence of actions leading to a state where the property is not satisfied. Understanding this counterexample for debugging the specification is a complicated task because the developer has to understand by manual analysis all the steps (possibly many) that have provoked the bug. The objective of this work is to improve the comprehension of counterexamples and thus to simplify the detection of the source of the bug. Given a liveness property, our approach first extends the model with prefix / suffix information w.r.t. that property. This enriched model is then analysed to identify specific states called neighbourhoods. A neighbourhood consists of a choice between transitions leading to a correct or incorrect part of the model. We exploit this notion of neighbourhood to highlight relevant parts of the counterexample, which makes easier its comprehension. Our approach is fully automated by a tool that we implemented and that was validated on several real-world case studies.

12h05 – 14h00

Déjeuner et fin du séminaire