|
Séminaire CONVECS 2023 |
|
Programme scientifique
|
Mercredi 14 Juin 2023 |
||
|
13h00 – 14h30 |
Déjeuner et début du séminaire |
|
|
14h30 –
15h30 |
Hubert Garavel What's Wrong
with Process Calculi? And How to Recover? Based on the foundational works of Tony Hoare and Robin Milner,
process calculi provide sound bases for specifying and analyzing concurrent
systems. After decades of intense research, process calculi seem to have
entered a phase of decline, in which they are only known and used by a
shrinking community of experts. We look retrospectively to understand the
reasons for the present situation and propose, based upon research going on
in Grenoble, potential directions for a wider dissemination of process
calculi. |
|
|
15h30 –
16h15 |
Pierre Bouvier (joint work with Hubert Garavel) Identifying
Duplicates in Large Collections of Petri Nets and Nested-Unit Petri Nets We propose efficient techniques for detecting isomorphism between
nets, i.e., for identifying, in large collections of (safe) Petri nets or
Nested-Unit Petri Nets, all the nets that are identical modulo a permutation
of places, a permutation of transitions, and/or a permutation of units. Our
approach relies upon the successive application of diverse algorithms of increasing
complexities: net signatures, net canonizations, and characterization of
isomorphic nets in terms of isomorphic graphs. We implemented this approach
in a complete tool chain that we successfully assessed on four collections,
the largest of which comprises 241,000+ nets with many duplicates. |
|
|
16h15 –
16h45 |
Pause café |
|
|
16h45 –
17h30 |
Quentin Nivon (joint work with Irman
Faqrizal and Gwen Salaün) Patching
Liveness Bugs in Concurrent Programs Model checking automatically verifies that a model, e.g., a Labeled
Transition System (LTS), obtained from higher-level specification languages,
satisfies a given temporal property. When the model violates the property,
the model checker returns a counterexample, but this counterexample does not
precisely identify the source of the bug. Moreover, manually correcting the
given specification or model can be a painful and complicated task. In this
paper, we propose some techniques for computing patches that can correct an
erroneous specification violating a liveness property.
These techniques first extract from the whole behavioral model the part that
does not satisfy the given property. In a second step, this erroneous part is
analyzed using several algorithms in order to compute the minimal number of
patches in the specification, so as to make it satisfy the given property. The
approach is fully automated using a tool we implemented and applied to a
series of examples for validation purposes. |
|
|
17h30 –
18h15 |
Radu Mateescu On-the-fly
Model Checking of Linear-time Properties in MCL We briefly compare linear-time (LTL) and branching-time (CTL) temporal
logics, and illustrate how linear-time properties can be expressed in the MCL
branching-time logic of CADP using the infinite looping operator. The
on-the-fly model checking of this operator on a Labeled Transition System
(LTS) is translated to the local resolution of a Boolean Equation System
(BES) containing marked variables, which must belong to a cycle of
dependencies in a solution of the BES. These BESs are represented as Boolean
graphs (a.k.a. dependency graphs) very similar to Büchi
automata on infinite words, and can be solved efficiently using depth-first
search (DFS) graph traversal algorithms. We compare two such algorithms
available in the CAESAR_SOLVE library of CADP, namely A3 (based on computing
strongly connected components in the Boolean graph) and A10 (based on nested
DFS, the traditional algorithm used for LTL model checking) in terms of
efficiency and quality of diagnostics produced. |
|
|
18h15 – 19h15 |
Frédéric Lang Compositional
Verification using CADP We consider the verification of temporal logic properties on the
formal model of a system described as a parallel composition of processes.
The well-known state explosion problem may be palliated by compositional
verification, a divide-and-conquer approach that consists in generating,
reducing with respect to some equivalence relation, and composing in an
incremental way the state spaces of individual processes. The choice of the
equivalence relation is crucial in that it must compress the state space
sufficiently while still preserving the properties of interest. I will
present the principles of compositional verification, the tools available in
CADP, as well as hints for choosing an appropriate (sharp) equivalence
relation. |
|
|
20h00 |
Dîner |
|
|
Jeudi 15 Juin 2023 |
||
|
09h00 – 09h45 |
Stéphane Ducasse Pharo and its Tools Pharo (http://www.pharo.org)
is a reflective and immersive language with its IDE (Integration Development
Environment). Its syntax fits on half of a postcard. In this talk, I will
briefly present the fundamental elements of Pharo
(objects, messages, and lambdas) in 10 minutes, as well as several useful
tools, such as automatic runtime deprecation and control flow break points
using a few lines of code. I will also show how one can shape the tools to increase
the speed of the development process (in particular, Xtreme
Test Driven Development). I will present, for example, the tools we built
around Druid, an AOT (Ahead-of-Time) compiler we are developing, as well as
some sketches of debugging assembly from within Pharo. |
|
|
09h45 –
10h15 |
Gwen Salaün (joint work with Philippe Merle) Automated
Verification of TOSCA Workflows TOSCA is a specification language used for modeling topology and
orchestration of cloud applications. This language particularly allows the
description of workflows that can be used for specifying management tasks
such as (un)deployment plans. This textual language for describing TOSCA
workflows does not provide any visualization techniques for graphically
designing or observing the corresponding workflows. Moreover, this language
is error-prone and can be source of mistakes when writing management plans.
In this work, we propose a transformation from TOSCA to the graphical
workflow-based language BPMN, so as to allow the visualization of TOSCA
workflows. We also provide automated verification techniques for analyzing
TOSCA workflows in terms of functional and architectural properties, as well
as execution times. The transformation and verification steps are achieved in
a fully automated way and were validated on a set of realistic TOSCA
workflows. |
|
|
10h15 – 10h50 |
Philippe Ledent (joint work with Radu
Mateescu and Wendelin Serwe) Formal
Semantics for PSS by Translation to LNT PSS (Portable test and Stimulus Standard) is an industrial language to
ease the generation of test suites for System-on-Chip architectures, by
completing a verification intent with necessary
intermediate actions satisfying a set of constraints on the system. However,
in the absence of formal semantics, it remains challenging to precisely
control test generation and to provide guarantees about the obtained test
suite. In this paper, we propose formal semantics for PSS by translation to
the formal language LNT supported by the CADP toolbox, thus paving the way
for a precise analysis of PSS models and a generation of test suites with
coverage guarantees. |
|
|
10h50 – 11h20 |
Pause café |
|
|
11h20 – 11h50 |
Suraj Gupta Blockchain for Log Data Blockchains have
emerged as a promising technology for secure and reliable data storage. A blockchain is a decentralized, distributed ledger that
records transactions in a secure and transparent manner. The use of blockchains for storing log data has gained significant
attention in recent years due to its potential to enhance the security and
reliability of log data storage. The talk will explore the potential benefits
and challenges of using blockchains for log data
storage and provide insights into the potential of blockchain
technology for this application. |
|
|
11h50 – 12h25 |
Lucie Muller (joint work with Radu Mateescu, Wendelin Serwe, Mihai Nica, Tilen Semenic,
and Armin Traussnig) Probabilistic
Fault Analysis using Formal Modeling and Fault Injection Because faults in critical systems may have severe consequences, these
systems need to be thoroughly validated, ideally using formal methods. In
practice, the impact of faults on the system behavior is often studied using
fault injection methods. In this paper, we use fault injection on formal
models and propose two methods to quantitatively estimate the impact of
faults w.r.t. the expected correct behavior: the former
compares the faulty model with the correct one and computes the probability
of deviation, and the latter computes the probabilities that correctness
requirements do no longer hold in the faulty model. We illustrate the methods
on the simple example of a coffee vending machine. Both methods can assess
the criticality of faults, and have been applied to an industrial case study
of a high-voltage battery for electric vehicles. |
|
|
12h30 – 14h00 |
Déjeuner |
|
|
14h00 – 14h45 |
Florian Gallay (joint work with Yliès Falcone) Decentralized
Runtime Enforcement We consider the problem of runtime enforcement on decentralized
systems with no central observation point nor central
authority. A so-called enforcer is attached to each system component and
observes its local trace. Should the global trace violate the specification,
the various enforcers coordinate to correct their local traces.
We formalize the decentralized runtime enforcement problem and define the
expected properties of enforcers, namely soundness, transparency, and
optimality. We present two enforcement algorithms that are based on LTL
specifications. The first one explores all alternatives to perform a globally
optimal correction, while the second follows an incremental strategy based on
locally optimal choices. We then introduce DECENT, a benchmark for these
algorithms and compare them with a centralized version. Finally, we introduce
a third algorithm that uses automata instead of LTL to address some of the
issues caused by formula rewriting in the previous ones. |
|
|
14h45 – 15h30 |
Ahang Zuo (joint
work with Yliès Falcone
and Gwen Salaün) Probabilistic
Runtime Enforcement of Executable BPMN Processes A business process is a collection of structured tasks that
communicate to provide a service or a product. Business processes do not
execute once and for all, but are executed multiple times, resulting in
multiple instances. In this context, it is particularly difficult to ensure
correctness and efficiency of the multiple executions of a process. In this
work, we propose to rely on Probabilistic Model Checking (PMC) to
automatically verify that multiple executions of a process respect some specific
probabilistic property. This approach applies at runtime; the evaluation of
the property is periodically verified and the corresponding results updated. However,
we go beyond runtime PMC for BPMN (Business Process Modeling Notation) here
because, in addition, we propose runtime enforcement techniques, which allow
one to keep executing the process while avoiding the violation of the
property. To do so, our approach combines monitoring techniques, computation
of probabilistic models, PMC, and runtime enforcement techniques. The
approach has been implemented as a toolchain and
validated on several realistic BPMN processes. |
|
|
15h30 – 16h00 |
Pause café |
|
|
16h00 – 16h45 |
Irman Faqrizal (joint
work with Yliès Falcone
and Gwen Salaün) Adaptive
Industrial Control Systems via IEC 61499 and Runtime Enforcement This work envisions Industrial Control Systems (ICSs) that can easily
adapt to specific requirements. We rely on the recent international standard
IEC 61499 as a stepping stone towards this goal. This standard is known for
its reconfigurability, allowing downtimeless
system evolution. However, an IEC 61499 application consisting of multiple
function blocks (FBs) can be reconfigured in many different ways, such as
inserting or deleting FBs, creating new FBs with their respective internal
behaviors, and adjusting the connections between FBs. These require
considerable effort and cost, and there is no guarantee to satisfy the
requirements. We apply runtime enforcement techniques for supporting adaptive IEC
61499 applications. This set of techniques can modify the runtime behavior of
a system according to specific requirements. Our approach begins with
specifying the requirements as a state machine-based notation called contract
automaton. This automaton is then used to synthesize an enforcer as a FB. Finally,
the new FB is integrated into the application to execute according to the
requirements. A tool is developed to automate the approach. In addition,
experiments are performed to evaluate the performance of enforcers by
measuring the execution time of several applications before and after the
integration of enforcers. |
|
|
16h45 –
20h00 |
Quartier
libre |
|
|
20h00 |
Dîner |
|
|
Vendredi 16 Juin 2023 |
||
|
09h00 – 09h30 |
Stéphane Ducasse Software
Maps In this talk, I
will present Rotten green tests, i.e., tests that contain assertions, that
say everything is ok, but still do not do their job. I will also present
some facts around software evolution and the need for software maps. Then, I
will present some maps and the Moose reengineering platform. In addition, I
will briefly present Roassal, a platform for
developing new visualizations and how to integrate them in Pharo. |
|
|
09h30 – 10h00 |
Hubert Garavel Building
Compiler Front-ends Using Syntax We present an approach for building compiler front-ends using, on the
one hand, the SYNTAX tool to perform lexical and syntactic analyses, and, on
the other hand, a novel library SXML, to build an abstract syntax tree and
print it to a file in XML-like or JSON-like format. We illustrate the
approach with the example of a front-end compiler for the synchronous
language LUSTRE. |
|
|
10h00 – 10h30 |
Wendelin Serwe (joint work with Hubert Garavel
and Frédéric Lang) Compiler
Construction Using SYNTAX and LNT This talk presents the compiler construction technology used over the
last 20 years by the CONVECS team. This technology is based on the SYNTAX
system for building the lexer and parser, and on
the (data part of) the formal description language LNT (interfaced with the C
language) for building the abstract syntax tree and the various processing
steps performed on it: static semantics checks, code generation, etc. |
|
|
10h30 – 11h00 |
Pause café |
|
|
11h00 – 11h30 |
Jean-Baptiste Horel (joint
work with Robin Baruffa, Lukas Rummelhard,
Alessandro Renzaglia, and Christian Laugier) A
Navigation-Based Evaluation Metric for Probabilistic Occupancy Grids: Pathfinding Cost Mean Squared Error While robotics increasingly relies on occupancy grids for environment
perception, the lack of specifically-designed metrics leads existing research
to employ Image Quality Assessment (IQA) metrics and topological evaluations,
which were primarily designed for binary occupancy
grids. While appropriate as a first approximation, not taking into account
the particular nature and usage of probabilistic occupancy grids limits the
accuracy of their evaluation. In this paper, we propose the PathFinding Cost Mean Squared Error (PFC-MSE), a new
probabilistic occupancy grid comparison metric designed to incorporate their
main usage and attributes. Emulating grid-based navigation methods, the
metric defines the difference between two grids as the measured spread
between the navigation behavior their use induces,
which emphasizes variations in general topology over local cell-value
fluctuations. Experimental results on 10,000 driving scenes exhibit the
relevance of the approach in quantifying grid disparities compared to
existing approaches. |
|
|
12h30 – 14h00 |
Déjeuner et fin du séminaire |
|