PhD Defense: Jawher Jerray

Dec 10 11:00 ₂₀₂₁

Abstract: Dynamical systems have a major impact on human development, especially critical systems that can put human lives at risk if something goes wrong. Hence, the need of studying the behavior of these systems to guarantee their correct functioning. Nevertheless, computing such type of system has never been an easy task, as the complexity of these systems is constantly increasing, in addition to the perturbations that may arise during their operation, as well as undefined parameters that may exist. To ensure that a system always produces the expected results and does not fail in any way, a formal verification of its behavior and properties is necessary.

In this thesis, we study dynamical systems from different perspectives and using various techniques. More specifically, we focus on the formal verification of critical properties such as schedulability, synchronization, robustness and stability.

In the first part, we start with the formal verification of real-time systems under uncertainty, where we use parametric timed automata sometimes extended by stopwatches to model systems with preemption. This formalism is very suitable for real-time systems due to its good expressiveness. It allows studying the schedulability of the flight control of a space launcher with unknown parameters and under constraints. Then, a synthesis of the admissible timing values of the unknown parameters is provided by a parametric timed model checker. We increase the complexity of the problem by taking into consideration the switch time between two threads. We extend this work by developing a tool called Time4sys2imi that translates a given real-time system design into parametric timed automata in order to infer some timing constraints ensuring schedulability.

In the second part, we study the stability of dynamical systems and the robustness of controls. We give a simple technique based on Euler's integration method, which allows building an invariant set around a given system. This technique guarantees that the approximate Euler solutions are attracted by a limit cycle. We apply the method on different systems, including chaotic systems with strange attractors. Furthermore, we show that a basic combination of a random sampling with a symbolic computation method assists to deal with robust control problems for nonlinear systems. Also, we illustrate a basic condition guaranteeing that a system with perturbation is robust under a repeated control sequence obtained by solving a horizon optimal control problem. Finally, we unified the main contributions of the second part in a tool called ORBITADOR which checks the stability of a given system and notably returns plots containing the evolution of the system in different views and the shape of the invariant if it exists.

Jury:

• Thao Dang, VERIMAG - Reviewer
• Goran Frehse, ENSTA Paris - Reviewer
• Frédérique Bassino, Université Sorbonne Paris Nord - Examiner
• Giuseppe Liparini, Université de Lille - Examiner
• Raphaël Jungers, Université catholique de Louvain - Examiner
• Laure Petrucci, Université Sorbonne Paris Nord - Examiner
• Étienne André, Université de Lorraine - Co-advisor
• Laurent Fribourg, ENS Paris Saclay - Co-advisor