|
Séminaire CONVECS 2018 |
|
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 3. Cyber-physical
interactions which introduce non-deterministic and physical world's space and
time dependent events. |
|
|
20h00 |
Dîner |
|
|
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 |
Déjeuner |
|
|
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 |
|
|
20h00 |
Dîner |
|
|
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 |
|