|
Séminaire CONVECS 2024 |
|
Programme scientifique
|
Jeudi 28 Novembre 2024 |
||
|
09h00 –
09h30 |
Café
d’accueil |
|
|
09h30 –
10h00 |
Germán Vega (joint work with Akram Idani and Yves Ledru) A
Process-Centric Approach to Insider Threats Identification in Information
Systems The development of complex software systems as done today generates
countless security vulnerabilities that are difficult to detect. In this
context, several research works have adopted the Model Driven Security (MDS)
approach, which investigates software models rather than implementations.
However, although these works provide useful techniques for security modeling
and validation, they do not address the impact of functional behavior on the
security context of the system, which can be cause for several flaws, specially insider threats. In order to address this
challenge, we propose a dynamic analysis based on the B method for both
functional and security concerns. Our contribution extends the B4MSecure
platform that we developed in our previous works, by introducing a
workflow-centric layer to model expected business processes, as well as
possible malicious activities. This new layer is built on CSP || B and brings
new validation possibilities to B4MSecure. |
|
|
10h00 –
10h30 |
Quentin Nivon (joint work with Gwen Salaün
and Frédéric Lang) GIVUP:
Automated Generation and Verification of Textual Process Descriptions A business process is defined as a set of tasks executed in a certain
order to achieve a specific goal. BPMN has become the standard modelling language for describing and developing business
processes. One of the main challenges in the business process management area
is to provide techniques and tools for analysing
and optimising processes, which are necessary for
example to avoid bugs or unexpected process executions. However, modelling and debugging processes is a difficult task.
This paper presents GIVUP, a tool that takes as input descriptions of a
process and of a functional property written in natural language. GIVUP
transforms the textual process into BPMN and the textual property into the
corresponding LTL formula. It then verifies whether the BPMN process
satisfies the property. This is achieved by using several internal
transformations and model checking techniques. This approach is helpful for
any kind of users, and can be used during several stages of the lifecycle of
a process, such as the design phase or any refinement phase. GIVUP is freely
accessible online, and a demo video can be found at: https://www.youtube.com/watch?v=oxkPMJcheMs. |
|
|
10h30 –
11h00 |
Pause
café |
|
|
11h00 –
12h00 |
Hubert Garavel (joint work with Frédéric
Lang and Wendelin Serwe) An
Account of the LNT Project (1998-2024) We present the work carried out during more than two decades on
defining the LNT language and equipping it with compilers for verification
purposes. LNT is a modern formal method for the description of concurrent asynchronous
systems. The language has an imperative flavour,
combining the best features of process calculi and mainstream programming
languages. LNT was used in many case-studies, often in industrial context,
and is also taught in university courses in France and abroad. |
|
|
12h00 –
12h30 |
Zachary Assoumani (joint work with Wendelin
Serwe) Formal Modelling of the HPDCache using
LNT HPDCache is an
L1 high-performance data cache compatible with RISC-V and AMBA AX15
processors. This cache is part of the CVA6 implementation of the RISC-V
architecture, used by several industrial companies (Bosch, Thales,
...). HPDCache is highly configurable,
equipped with out-of-order execution and replay features, and has a three-stage pipeline architecture able to handle about
ten simultaneous transactions. We present a formal model of HPDCache in LNT that can serve as basis for various
analyses, such as verification, performance evaluation, and conformance test
generation. |
|
|
12h30 –
14h00 |
Déjeuner |
|
|
Quartier
libre |
||
|
15h00 –
16h00 |
Frédéric
Lang Vérification
compositionnelle de systèmes concurrents asynchrones Les systèmes modernes (matériels
et logiciels) sont souvent constitués de "tâches" qui s'exécutent
en parallèle et communiquent. La complexité qui en découle nécessite de
disposer d'outils permettant de vérifier leur bon fonctionnement, en particulier
pour les systèmes critiques. Cet exposé abordera la modélisation formelle de
ces systèmes sous forme de réseaux de processus communicants, ainsi que de
leurs propriétés, soit sous forme de formules de logique temporelle, soit
sous forme d'automate. Nous aborderons le problème consistant à vérifier ces
propriétés en tentant de repousser le problème de l'explosion combinatoire
des états, notamment par des méthodes compositionnelles. |
|
|
16h00
– 16h30 |
Pause
café |
|
|
16h30
– 17h00 |
Wei Chen (joint work with Leila Kloul) Stochastic Modelling of
Autonomous Vehicles Driving Scenarios using PEPA We present an advanced stochastic modeling approach
using PEPA (Performance Evaluation Process Algebra) to simulate and analyze
autonomous vehicle driving scenarios. Our method addresses the complexity of
modeling real-world environments by incorporating critical elements such as
dynamic traffic interactions, environmental factors, and sensor data
variability. By applying PEPA, we develop a framework that evaluates the
likelihood of different scenarios, enabling automated test case generation. |
|
|
17h00 –
17h15 |
Jean-Baptiste Horel (joint work with
Alessandro Renzaglia, Radu
Mateescu, and Christian Laugier) Scenario-based
Validation of Autonomous Vehicles using Augmented Reality Validation of autonomous vehicles (AVs) is a critical task in their
development and for their approval on public roads. Scenario-based testing is
the state-of-the-art validation method and is recommended by international
automotive regulators. While simulated execution of critical scenarios is
essential, it cannot yet fully replace real-world testing, which however
remains tedious, time-consuming, and resource-intensive. In this work, we
propose an enhanced methodology using Augmented Reality to bridge the gap,
providing an intermediate testing method that enables comprehensive
real-world testing with reduced cost and improved realism. To demonstrate
this methodology, we conducted tests in a controlled environment using six
critical scenarios selected from road crash studies. |
|
|
17h15 –
17h45 |
Aline Uwimbabazi (joint work with Jean-Baptiste
Horel, Radu Mateescu, Philippe Ledent, and Wendelin Serwe) Formal
Assessment of Driving Scenarios using Probabilistic Model Checking Devising scenarios for testing autonomous vehicles is still a
challenging task that requires a tradeoff between cost and achieved coverage
of the considered operational design domain. Often scenarios are derived from
accident statistics and real traffic datasets, relying on expert knowledge
and intuition to select the most relevant ones for simulation and/or field
testing. This task is carried out mostly manually, and would benefit from a
precise method to assess scenario relevance and compare scenarios. In this
paper, we suggest a generic approach to compare scenarios based on
quantitative measures computed by probabilistic model checking. We illustrate
the approach to compare variations of scenarios derived from frequent
situations in accident statistics, in terms of measures such as collision
probability and duration. |
|
|
17h45 –
18h15 |
Irman Faqrizal (joint work with Tatiana Liakh,
Midhun Xavier, Gwen Salaün,
and Valeriy Vyatkin) Probabilistic
Model Checking for IEC 61499: A Manufacturing Application The ever-increasing complexity of industrial control systems generates
a demand for reliable development methods. IEC 61499, a recent industrial
standard, helps to develop complex distributed systems based on their
positive characteristics, namely reusability, reconfigurability,
interoperability, and portability. Formal verification techniques, such as
model checking, have been proposed to ensure the correctness of these systems
during the design time. However, they do not consider the presence of the
environment that can impact the application behaviour
at runtime. This work combines design time and runtime analyses to apply
probabilistic model checking on an IEC-61499-based manufacturing application.
We present several probabilistic properties to be checked. The results are visualised graphically to be analysed,
which allows one to optimise the system's
quantitative features, such as productivity. |
|
|
18h15 –
18h45 |
Wendelin Serwe (joint work with Hubert Garavel,
Frédéric Lang, Philippe Ledent,
and Aline Uwimbabazi) On
Experiments to Model and Solve Jobshop Scheduling
with CADP In this talk, we present our experiments on using CADP to tackle the jobshop scheduling problem, an NP hard optimization
problem consisting in the computation of a shortest-time schedule of jobs
(i.e., sequence of tasks) on several machines. We present four LNT models
using different modeling styles and discuss their respective advantages and inconvenients. |
|
|
18h45 –
19h00 |
Cocktail |
|
|
19h00 –
20h30 |
Dîner
et fin du séminaire |
|