Jawher Jerray

Contexts:

1. I worked on a project piloted by partners of the “C3S chaire” about Model-based High-level Integration of Heterogeneous Components.
   This work aims to define techniques to join the semantics of components captured with heterogeneous models and at different levels of abstraction while maintaining real-time communication between components and ensuring accurate verifications applied to safety and security properties.
2. I also worked on a project in collaboration with Huawei Munich, where the main objective is to develop a methodology that ensures both the safety and security of software updates for autonomous vehicles. The solution we proposed to this problem is to integrate safety and security patterns into models.
3. I participated in the ANR project called TCE which aims to produce educational resources in cybersecurity, in the form of digital content and educational platforms for French universities.

keywords:

• Formal verification
• Hardware/Software architectures
• Heterogeneous Components
• Meta-models
• Semantics
• Simulation
• TTool
• SystemC

I worked in the LoVe team at LIPN, particularly in the verification research axis.
My thesis (funded by the Université Sorbonne Paris Nord, ED Galilée) focused on formal methods specifically with parametric timed model-checking in order to analyse real-time systems under uncertainty. The main works carried out during the first part of the thesis are:

• Scheduling analysis of a launcher flight control system under constraints and using Parametric Timed Automata (PTA).
• Automatic translation of Time4sys models (real-time systems models) to PTAs which allows to verify the schedulability of real-time systems under uncertainty.

keywords:

• Model checking
• Formal methods
• Real-time systems
• Parametric timed automata

I have also worked on the study of other types of systems, notably the analysis of dynamic systems including hybrid systems. The contributions made in this part include:

• Synchronization of dynamical systems using symbolic Euler's method.
• Stability of parametric time-periodic systems using bounded invariants via stroboscopic set-valued maps.
• Robustness of dynamical systems by generating a robust optimal periodic control using dynamic programming and guaranteed Euler’s method.
• Optimization of dynamical systems by a minimax control using random sampling and symbolic computation.

keywords:

• Control
• Optimization
• Robustness
• Synchronization
• Hybrid systems
• Symbolic methods
• Reachability
• Stability

Synchro is a method that aims to find formal sufficient conditions to guarantee phase synchronization using the notion of reachability since it is delicated to obtain the exact parameter values of the system for which the phenomenon of phase synchronization manifests. More precisely, this method selects a portion \(S\) of the state space, and shows that any solution starting at \(S\) returns to \(S\) within a fixed number of periods \(k\). Besides, it shows that the components of the solution are then (almost) in phase.
Synchro is applied on the Brusselator reaction-diffusion and the biped walker examples. These examples can also be seen as challenges for the verification of continuous and hybrid systems.

Robust gives a simple condition of set inclusion which guarantees that the system is open-loop stable in the presence of perturbation when it is generating by periodic control that should be intrinsically robust or stable against possible perturbations or uncertainties.
In contrast with many methods of OPC using elements of the theory of limit cycles, this method does not use any notion of Lyapunov function/differential equation nor any notion of contraction. A by-product of this method is a simple way to prove the existence of a limit cycle for the process in the absence of perturbation.
The simplicity of Robust is illustrated on a classical examples of bioreactor, spin and Van der Pol systems.

Parameter presents a method to prove the existence of a limit cycle (LC) of a dynamic system \(\Sigma\) and construct an enclosure of the LC which is an invariant set of \(\Sigma\). The method essentially consists in adding a small additive perturbation to \(\Sigma\), and finding an approximation \(T\) of the exact period such that the set of solutions of the perturbed system at the instant \((i+1)T\) is included in the set of solutions at \(iT\) for some integer \(i\).
Indeed, this property, combined with a contraction condition ensuring the stability of \(\Sigma\), guarantees the existence of an LC. The addition of a small perturbation allows using only an approximate value \(T\) of the exact period, avoiding precise tedious calculations. It also allows, for a parametric dynamic system, to use the same value \(T\) for showing in a generic manner the existence of LCs for a whole range of values of the parameter.
The interest of Parameter is shown for classical examples of periodic systems such as the Brusselator, Biped and Van der Pol systems.

MCRS aims at the synthesis of an approximate minimax control for a system dynamic given in the form \(\dot{x}(t) = f(x(t),u(t),d(t))\) where \(x\) represents the state, \(u\) the control (or input) and \(d\) a disturbance (or perturbation). The disturbance \(d(t)\) is prescribed to a compact domain \({\cal D}\) on which it can take any value (bounded uncertainty).
This method makes use of symbolic computation to enclose the solutions corresponding to all possible disturbance \(d(\cdot)\in{\cal D}\), together with a simple algorithm of random sampling to select the minimum control \(u^*(\cdot)\).
The interest of MCRS is illustrated on an example of a biochemical reactor.

ORBITADOR is a tool for stability analysis of dynamical systems. ORBITADOR uses a method that generates a bounded invariant set of a differential system with a given set of initial conditions around a point \(x_0\) to prove the existence of a limit cycle. This invariant has the form of a tube centered on the Euler approximate solution starting at \(x_0\), which has for radius an upper bound on the distance between the approximate solution and the exact ones. The method consists in finding a real \(T > 0\) such that the snapshot of the tube at time \(t = (i + 1)T\) is included in the snapshot at \(t = iT\), for some integer \(i\) with adding a small bounded uncertainty. This uncertainty allows using an approximate value \(T\) of the exact period.

Time4sys2imi is a tool translating Time4sys models (Time4sys is a formalism developed by Thales Group, realizing a graphical specification for real-time systems) into parametric timed automata in the input language of IMITATOR (IMITATOR is a parametric model checker taking as input networks of PSA extended with useful features such as synchronization actions and discrete variables.).
This translation allows not only to check the schedulability of real-time systems, but also to infer some timing constraints (deadlines, offsets ...) guaranteeing schedulability.