|
Séminaire CONVECS 2019 |
|
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 |
|