Jawher Jerray

Tools and implementations

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.