En poursuivant votre navigation sur ce site, vous acceptez le dépôt de cookies dans votre navigateur. (En savoir plus)

PhD - A Hierarchical Time Model for Event-B (M/F)

This offer is available in the following languages:
- Français-- Anglais

Date Limite Candidature : mardi 12 août 2025 23:59:00 heure de Paris

Assurez-vous que votre profil candidat soit correctement renseigné avant de postuler

Informations générales

Intitulé de l'offre : PhD - A Hierarchical Time Model for Event-B (M/F) (H/F)
Référence : UMR7271-MAGRIC-005
Nombre de Postes : 1
Lieu de travail : VALBONNE
Date de publication : mardi 22 juillet 2025
Type de contrat : CDD Doctorant
Durée du contrat : 36 mois
Date de début de la thèse : 1 octobre 2025
Quotité de travail : Complet
Rémunération : 2200 gross monthly
Section(s) CN : 06 - Sciences de l'information : fondements de l'informatique, calculs, algorithmes, représentations, exploitations

Description du sujet de thèse

Define an heterogeneous model of time based on the tagged signal
model ([1][1]) into the Event-B methodology ([2][2]). This should consist in defining hooks (called Logical clocks ([3][3])) for both probing and control into an Event-B machine in such a way that several models of time (synchronous, event-triggered, discrete-event, continuous-time) can be used jointly as part of the Event-B models.
To demonstrate the usefulness of the approach, we shall use several case studies (4) and produce an open-source demonstrator based on Rodin platform ([5][5]) using Rodin's component plugin ([6] [6]). Once the clocks are injected within the Event-B model, we expect to be able to run ad-hoc verification techniques that shall largely depends on the actual model of time in use. Such Laboratoire i3S, UMR 7271
Laboratoire Méthodes Formelles, UMR 9021, pôle Modélisation des systèmes Critiques,
verification techniques and tools can range from assistant provers, model-checkers (symbolic, stochastic) to heterogeneous simulation tools (like Ptolemy ([7][7]), TESL ([8][8]), ModHel'X ([9][9]), GeMoC ([10][10]) .
Required skills :
- Master degree in Computer Science, formal methods, embedded systems, or a related field.
- Background in the use of formal methods.
- Open mindedness about the use of different languages and frameworks, proficiency in at least one classical programming languages (e.g., Java, Typescript, C++).
- Familiarity with classical development practices, including unit testing and CI/CD (Continuous Integration/Continuous Deployment).
- Strong ability to adapt to dynamic research environments and solve complex technical
challenges.

Contexte de travail

This position is available within the Comred depertment of the i3S / UMR 7271 Laboratory in Sophia Antipolis. The Laboratory for Computer Science, Signals and Systems at Sophia Antipolis (i3S), created in 1989, conducts research in computer science. With a staff of nearly 300 members, including professors and researchers from the Université Côte d'Azur, CNRS and Inria researchers, administrative and technical staff, doctoral students and trainees, it is one of the largest public laboratories on the Côte d'Azur and was one of the first to be established in the Sophia Antipolis technology park.

Contraintes et risques

None