Séminaire CONVECS 2019
Villard-de-Lans (Isère)

Logo CONVECS

 

Villard-de-Lans

 


Programme scientifique


Lundi 1er Juillet 2019

12h00 – 14h00

Déjeuner et début du séminaire

14h00 – 15h00

Frédéric Lang (joint work with Radu Mateescu and Franco Mazzanti)

Compositional Verification of Concurrent Systems by Combining Bisimulations

 

Compositional verification is a promising technique for analyzing action-based temporal properties of concurrent systems. One approach to verify a property expressed as a modal mu-calculus formula on a system with several concurrent processes is to build the underlying state space compositionally (i.e., by minimizing and recomposing the state spaces of individual processes, keeping visible only the relevant actions occurring in the formula), and check the formula on the resulting state space. It was shown previously that, when checking the formulas of the Lmu-dsbr fragment of mu-calculus (consisting of weak modalities only), individual processes can be minimized modulo divergence-preserving branching (divbranching) bisimulation.

 

We refine this approach to handle formulas containing both strong and weak modalities, so as to enable a combined use of strong or divbranching bisimulation minimization on concurrent processes depending whether they contain or not the actions occurring in the strong modalities of the formula. We extend the existing Lmu-dsbr fragment with strong modalities and show that the combined minimization approach preserves the truth value of formulas of the extended fragment. We implemented this approach on top of the CADP verification toolbox and demonstrated how it improves the capabilities of compositional verification on realistic examples of concurrent systems.

15h00 – 15h30

Wendelin Serwe (joint work with Radu Mateescu)

Formally Analyzing Attack-Resistance of Asynchronous Circuits

 

In this talk, I present work in progress about gate-level analysis of an asynchronous circuit designed to detect physical attacks (e.g., wire-cuts or short-circuits). I discuss different modeling approaches (for gates and possible attacks), verification results obtained for small configurations, and inductive reasoning principles to scale these results to larger circuits.

15h30 – 16h00

Pause café

16h00 – 16h35

Pierre Bouvier (joint work with Hubert Garavel)

Automated Discovery of Nested Units in Petri Nets

 

We revisit the problem of decomposing a Petri net into a set of communicating automata, a problem which has been around since at least the early 70s. We do this in light of Nested-Unit Petri Nets (NUPNs), a modern variant of Petri nets that supports locality and hierarchy. We propose a number of novel methods for automatically converting an ordinary, one-safe Petri net into a NUPN that has the unit-safeness property and such that the memory encoding of the reachable markings of this NUPN takes as few bits as possible. We consider both “flat” translations to communicating automata (which are a particular case of NUPNs having height one) and “hierarchical” translations to more general NUPNs having an arbitrary height. We also study the case of large Petri nets, whose state space is too large for being explored exhaustively. We report about the implementation of these methods, for which we developed specific translators that invoke already available third-party software, such as NUPN tools, SAT/SMT solvers, and tools for computing maximal cliques. Finally, we measure and compare the performance of our methods on a very large collection of NUPNs coming from diverse sources.

16h35 – 17h20

Armen Inants and Radu Mateescu

On-the-fly Action-based Probabilistic Model Checking

 

The quantitative analysis of concurrent systems requires expressive and user-friendly property languages combining temporal, data-handling, and quantitative aspects. We give an overview of the EVALUATOR 5 model checker recently added to CADP. The tool takes as input a formula in the MCL language extended with a probabilistic operator, and evaluates it on a PTS (Probabilistic Transition System) obtained from an LNT specification by assigning probabilities to transitions on the fly. We focus on the usage of the tool, illustrating it on examples of PTSs and data-based probabilistic formulas. We also propose an optimization technique, based on a static analysis of formulas, that can improve the performance of on-the-fly verification.

20h00

Dîner

Mardi 2 Juillet 2019

09h00 – 09h30

Loïc Letondeur (Orange Labs)

Artificial Intelligence and Edge Computing 

 

Deep neural networks, as building blocks implementing deep learning features, are nowadays spreading in a variety of application domains. We give an overview of the current trends in AI, their instantiation in the context of edge computing (carried out by connected devices at the border of the cloud), and the research challenges for the near future.

09h30 – 10h15

Umar Ozeer (joint work with Loïc Letondeur, Gwen Salaün, François-Gaël Ottogalli, and Jean-Marc Vincent)

Failure Management for Cyber-Physical Consistency for IoT Applications in the Fog

 

Fog Computing is especially appealing to the Internet of Things (IoT) because it provides computing, storage and communication resources at the edge of the network, near the physical world (PW). Thus, IoT devices near the PW can have interesting properties such as low latencies, real-time operations and data privacy. The Fog, however, is unstable because it is constituted of billions of devices in a dynamic environment. Moreover, the Fog is cyber-physical and devices are subjected to external PW conditions which increase the occurrence of failures. When failures occur in such an environment, the resulting inconsistencies with respect to the PW can be hazardous and costly. We propose a failure management protocol for IoT applications deployed in the Fog that focuses on maintaining consistency with respect to the PW upon recovery. Consistency is ensured by repairing the application and restoring a target state by exploiting the behavioural models of entities upon recovery. The protocol was validated on a smart home testbed as well as through model checking techniques.

10h15 – 10h45

Pause café

10h45 – 11h30

Ajay Muroor-Nadumane (joint work with Michel Le Pallec, Radu Mateescu, Alejandro Martinez-Rivero, and Gwen Salaün)

Advanced Rule-based Composition and Deployment for Web of Things

 

The Internet of Things (IoT) consists of network connected devices and software elements that communicate with each other to fulfil certain tasks. Consumers can build IoT applications by combining various such devices using existing tools. Typically, consumers build applications using Trigger Action Programming (TAP) i.e., rules in the form of If-This-Then-That (IFTTT). TAP is popular partly due to its simplicity. However, to build advanced applications, TAP in its current form is lacking. In this talk, we propose extensions to TAP rules so that users can compose multiple rules to build advanced applications. These extensions are backed by a new UI for end-users to build such applications. Further, we discuss the verification and deployment mechanisms integrated in this work. Finally, an end-to-end implementation (from design to deployment) built on top of Mozilla WebThings platform will be shown to generate further discussion.

11h30 – 12h15

Gwen Salaün (joint work with Francisco Duran and Ajay Muroor-Nadumane)

Automated Composition, Analysis and Deployment of IoT Applications

 

Building IoT applications of added-value from a set of available devices with minimal human intervention is one of the main challenges facing the IoT. This is a difficult task that requires models for specifying objects, in addition to user-friendly and reliable composition techniques which in turn prevent the design of erroneous applications. In this work, we tackle this problem by first describing IoT applications using abstract models obtained from existing models of concrete devices. Then, we propose automated techniques for building compositions of devices using a repository of available devices, and an abstract goal of what the user expects from such compositions. Since the number of possible solutions can be quite high, we use both filtering and ranking techniques to provide the most pertinent solutions to users. The provided solutions satisfy the given goal and may be analysed with respect to properties such as deadlock-freeness or unmatched send messages. Finally, the application can be deployed using existing deployment engines.

12h15 – 14h00

Déjeuner

14h00 – 14h45

Luca Di Stefano (Gran Sasso Science Institute, L'Aquila, Italy - joint work with Rocco de Nicola and Omar Inverso)

Specification and Analysis of Multi-Agent Systems with LAbS

 

A desirable goal in the design of multi-agent systems is to obtain complex collective behavior from the interaction of relatively simple agents. Whenever possible, this ability (as well as the safety of the system) should be guaranteed through formal reasoning. To achieve this goal, and due to the specific challenges presented by these systems, there is a need for very high-level languages that allow for compact and intuitive specifications, as well as tools that can assist in the development and analysis process. To address these needs we have developed LAbS, a specification language for agents that interact indirectly, by manipulating and diffusing their limited share of knowledge. Our additional contribution is SLiVER, a tool for the analysis of LAbS systems. SLiVER relies on an intermediate representation of LAbS processes as symbolic transition systems, which may then be encoded as nondeterministic programs in several existing languages. This allows us to analyze our systems with different off-the-shelf tools. As an example of our approach, we show an overview of our work on LAbS-to-LNT translation and some preliminary results obtained with the CADP toolbox.

14h45 – 15h30

Philippe Ledent (joint work with Christian Laugier, Radu Mateescu, and Alessandro Renzaglia)

Formal Validation of CMCDOT, a Probabilistic Perception System for Autonomous Vehicles

 

We are moving towards the level 3 of autonomous driving, where vehicles can not only control their speed but also execute the safety-critical actions themselves. This requires the autonomous vehicle to be excellent in its perception of the environment, its decision-making, and its action-taking. Because of the high risk for human lives, the automotive industry for autonomous vehicles is heading towards the critical regulations that are already used in the aerospace and railway domains where formal verification is required. Although the regulations for autonomous vehicles are not ready yet, we can anticipate them by already formally verifying the various systems used for autonomous driving. Today, the challenge in robotic perception for autonomous vehicles is to perform an accurate perception of the environment and create a relevant model.  

 

We perform the formal verification of a perception system for autonomous cars: the Conditional Monte Carlo Dense Occupancy Tracker (CMCDOT). CMCDOT belongs to the family of perception systems that use occupancy grids and probabilistic predictions. We validate CMCDOT by selecting in its outputs the information that is necessary to show that it rises to the challenge. This information is dumped into traces and the formal verification is performed using the XTL tool of the CADP toolbox. Our work departs from the classical verification on traces by combining the extraction and the manipulation of data values in the events, walking back and forth through the traces. We produce quantitative results that go beyond classical temporal logic verification.

15h30 – 16h00

Pause café

16h00 – 16h45

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

Asynchronous Testing of Synchronous Components in GALS Systems

 

GALS (Globally Asynchronous Locally Synchronous) systems, such as the Internet of Things or autonomous cars,  integrate reactive synchronous components that interact asynchronously. The complexity induced by combining synchronous and asynchronous aspects makes GALS systems difficult to develop and debug. Ensuring their functional correctness and reliability requires rigorous design methodologies, based on formal methods and assisted by validation tools. We propose a testing methodology for GALS systems integrating: (1) synchronous and asynchronous concurrent models; (2) functional unit testing and behavioural conformance testing; and (3) various formal methods and their tool equipments. We leverage the conformance test generation for asynchronous systems to automatically derive realistic scenarios (environment constraints and oracles), which are necessary ingredients for the unit testing of individual synchronous components, and are difficult and error-prone to design manually. We illustrate our approach on a simple, but relevant example inspired by autonomous cars.

16h45 – 20h00

Balade dans le Vercors

20h00

Dîner

Mercredi 3 Juillet 2019

09h00 – 09h45

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

Recent Achievements of the CAPHCA Project

 

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, achievements, and current activities of the project.

09h45 – 10h30

Viet Anh Nguyen (IRT Saint-Exupéry – joint work with Eric Jenn, Frédéric Lang, Radu Mateescu, and Wendelin Serwe)

Using Model Checking to Identify Timing Interferences on Multicore Processors

 

Multicore platforms provide the computing capabilities and the power efficiency required by the complex applications embedded in aeronautical, spatial, and automotive systems. For multiple tasks to run concurrently and in parallel on the different cores, some of the hardware resources provided by the platform – including buses, caches, IPs – must be shared. This sharing may lead tasks to interfere with each other. Therefore, crucial design activities are to identify interferences, and bound the penalty induced by those interferences, as part of the demonstration of compliance of applications to their temporal requirements.

 

A first and conservative approach is to consider that every access to a shared resource leads to an interference. This safe approach is usually too pessimistic to be useful. We propose a less pessimistic approach, which takes into account the actual behavior of the application and the hardware to filter out situations where interferences cannot occur.

 

Our method relies on (i) the behavioral modeling of the applications and their execution platform using the LNT formal language, (ii) the definition of interferences using temporal properties, and (iii) the exploitation of the behavioral model and the temporal properties using the CADP formal verification toolbox. This method is applied to the Infineon AURIX TC275 system-on-chip. Experimental results indicate that our approach is both safe and prevents reporting spurious interferences compared to a purely structural analysis.

10h30 – 11h00

Pause café

11h00 – 11h45

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

From LOTOS to LNT

 

We revisit the early publications of Ed Brinksma devoted, on the one hand, to the definition of the formal description technique LOTOS (ISO International Standard 8807:1989) for specifying communication protocols and distributed systems, and, on the other hand, to two proposals (Extended LOTOS and Modular LOTOS) for making LOTOS a simpler and more expressive language. We examine how this scientific agenda has been dealt with during the last decades. We review the successive enhancements of LOTOS that led to the definition of three languages: E-LOTOS (ISO International Standard 15437:2001), then LOTOS NT, and finally LNT. We present the software implementations (compilers and translators) developed for these new languages and report about their use in various application domains.

12h00 – 14h00

Déjeuner et fin du séminaire