Ph.D. - Computational Sciences

Ph.D. Candidate in Computer science

Salary: 1769 euros brut

The income may increase with a teaching activity.

RESEARCH FIELD(S)1

• Computer sciences: Modelling and Simulation; Formal Verification

JOB DESCRIPTION

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 Rung-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 algebraic loops. 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.

References:

• Alur, R.: Formal versification of hybrid systems. In proceedings of EMSOFT 2011.
• Giambiasi N., B. Escudé and S. Gosh: GDEVS: A Generalized Discrete Event Specification for Accurate Modeling of Dynamic systems. Transactions of SCSI, 2000, 17 (3), pp.120-134.
• Platzer A.: Logics of dynamical systems. In proceeding of LICS 2012.
• Zeigler B.P., H. Praehofer and T. Gon Kim: Theory of Modeling and Simulation. Second edition 2000.

QUALIFICATIONS/SKILLS/EDUCATION & RESEARCH REQUIREMENTS

• Computer science with strong background in mathematics

JOB LOCATION

Laboratoire of Informatics and Systems (LIS) UMR CNRS 7020

Aix-Marseille University

Campus scientifique de St Jérôme – Av. Escadrille Normandie Niemen -13397 Marseille Cedex 20

REQUESTED DOCUMENTS OF APPLICATION

• 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.

CONTACT TO APPLY (Email, Websites, etc.)

Supervisor of thesis: Amine HAMRI (amine.hamri@lis-lab.fr), Associate professor HDR

Contact Person: If you wish to apply for this position, please specify that you saw it on AKATECH.tech