Formal Verification of DEVS/GDEVS Hybrid Systems

Continuous complex systems are often described using differential equations, a privileged paradigm by the system modelers for its ease-use. However, the analytic methods to solve such equations rely on methods that discretize time with equal steps. Euler and Runge-Kutta are well-known examples, they discretize the time space to compute the state trajectory. Unfortunately, these methods collide with the complexity of the modelled system whose increase the computation time and memory size needed to solve the problem. In addition, they are approximation and induce often a rate of errors unacceptable in comparison to the state trajectory of the real system under steady.

The formalism Generalized Discrete Event System Specification (GDEVS) known to be a generalization of Discrete Event System Specification formalism allows the modelling of the dynamics of continuous systems using polynomial functions. Such a formalism provides a faithful representation of hybrid systems where the discrete approach driven by events quotes with the continuous approach which allows to compute the state of the system between the occurrence of two successive events.

Few works were interested to checking formally hybrid systems. This is due to the dynamics of such systems which is not possible to describe using a state machine or an underlying formalism. In addition, such a topic covers two different communities of scientists: software systems and continuous systems where the goals of modelling are totally opposed.

These works of thesis will provide answers to relevant questions such as the legitimacy of hybrid systems for simulation by verifying the absence of cycles with time duration equals to zero. Such a verification will guarantee that the simulation will execute a finite number of transitions for a given time interval. Other verifications related to the system environment will be possible. For example, does the system always ensure the control of its elements? Is any transition always possible? Etc.

A second aspect of this work that seems interesting to develop is the self-adaptability of hybrid systems in the face of a new context (environment).  Knowing that work has been done at the macroscopic level (DS-DEVS), work at the microscopic level remains to be developed. For example, how to define a set of transitions that will allow to go back to the initial state? How to define a set of transitions that will allow to correct an error? Etc.

Therefore, these works will allow, at the end, defining a formal framework for the modelers of hybrid systems.

APPLICATION DEADLINE: April 30th 2023

ENVISAGED STARTING DATE: October 1st 2023

ENVISAGED DURATION: 36 months

WORK LOCATION(S): LIS Lab UMR CNRS 7020, Aix Marseille Université – Campus de Saint Jérôme – Bat. Polytech, 52 Av. Escadrille Normandie Niemen, 13013 Marseille, France

QUALIFICATIONS, REQUIRED EDUCATION LEVEL, PROFESSIONAL SKILLS, RESEARCH REQUIREMENTS High skills in computer science (modeling and simulation) with strong background in mathematics

SOFT SKILLS: Autonomy, Analytical and critical thinking, good English language and the French is a plus.

REQUESTED DOCUMENTS OF APPLICATION, SELECTION PROCESS

• CV (max. 2 pages)
• Master diploma, academic transcripts level M1 (Bac+4) and M2 (Bac+5) if available
• Letter of motivation showing the engagement into the doctoral college and the reasons for choosing the PhD subject above

WHERE TO APPLY: Please send full application to: Amine HAMRI amine.hamri@lis-lab.fr