Séminaire du 15 septembre 2023
Lieu
LIPN, CNRS UMR 7030, Université Paris 13, Institut Galilée.
Programme
14h00-15h00: Mo Fougali (IRIF); Compositional Verification of Embedded Real-Time Systems
In an embedded real-time system (ERTS),
real-time tasks (software) are typically executed on a multicore shared-memory platform (hardware).
The number of cores is usually small,
contrasted with a larger number of complex tasks that share data to collaborate.
Since most ERTSs are safety-critical,
it is crucial to rigorously verify their software against various
real-time requirements under the actual hardware constraints
(concurrent access to data, number of cores).
Both the real-time systems and the formal methods communities
provide elegant techniques to realize such verification,
which nevertheless face major challenges.
For instance, model checking (formal methods) suffers from the state-space explosion problem,
whereas schedulability analysis (real-time systems)
is pessimistic and restricted to simple task models and schedulability properties.
In this paper, we propose a scalable and generic approach to formally verify ERTSs.
The core contribution is enabling,
through joining the forces of both communities,
compositional verification
to tame the state-space size.
To that end, we formalize a realistic ERTS model
where tasks are complex with an arbitrary number of jobs and critical sections,
then show that compositional verification of such model is possible,
using a hybrid approach (from both communities),
under the state-of-the-art partitioned fixed-priority (P-FP)
with limited preemption scheduling algorithm.
The approach consists of the following steps, given the above ERTS model and scheduling algorithm.
First, we compute fine-grained data sharing bounds
for each critical section that reads or writes some data from the shared memory.
Second, we generalize an algorithm that, aware of the data sharing bounds,
computes an affinity (task-core allocation)
guaranteeing the schedulability of hard-real-time (HRT) tasks.
Third, we devise a timed automata (TA) model of the ERTS,
that takes into account the affinity, the data sharing bounds and the scheduling algorithm,
on which we demonstrate that various properties can be verified compositionally,
\ie on a subset of cores instead of the whole ERTS,
therefore reducing the state-space size.
In particular, we enable the scalable computation of tight worst-case response times (WCRTs)
and other tight bounds separating events on different cores,
thus overcoming the pessimism of schedulability analysis techniques.
We fully automate our approach and show its benefits on three real-world complex ERTSs, namely two autonomous robots and the automotive case study from the WATERS 2017 industrial challenge.
15h00-16h00 : Masaki Waga (Université de Kyoto); Toward Trustworthy AI-CPS with Automata Learning
Abstract :
While AI systems and Cyber-Physical Systems (CPS) are increasingly used,
it is still challenging to ensure their reliability. I will show
approaches combining automata learning and formal verification toward
trustworthy AI-CPS. In this approach, we use automata learning to
approximate the behavior of black-box AI-CPS and perform verification
and analysis on the approximated automaton using formal methods.
Concretely, after giving an overview of automata learning algorithms, I
will present our recent results: (1) automatic testing of stochastic
black-box systems with MDP learning and probabilistic model checking,
(2) safe reinforcement learning on black-box environments using automata
learning and shielding, and (3) active learning algorithm of timed
automata.
16h00-16h30: pause café
16h30-17h00: vie du groupe