Sujet : AltaRica Hybride

Responsable : André Arnold, Alain Griffault, Frédéric Herbreteau
Téléphone : (05 40 00) 60 94, (05 40 00) 69 15, (05 40 00) 33 36
e-mail : Andre.Arnold@labri.fr, Alain.Griffault@labri.fr, Frederic.Herbreteau@labri.fr
Equipe : MVTsi

Présentation du sujet :

Le modèle des automates à contraintes AltaRica est suffisamment général pour décrire la plupart des modèles formels dédiés à la vérification de systèmes. Ce formalisme nous permet de définir des sous-langages correspondant aux classes d'automates que l'on retrouve dans la littérature (automate fini, automate temporisé, automate hybride).

Les travaux passés ont permis la définition et le développement des outils liés au formalisme "modèles finis", et la définition du langage AltaRica temporisé est presque terminée.

Le travail de la thèse portera sur le formalisme AltaRica Hybride : il s'agira d'abord de définir la syntaxe et la sémantique de ce sous-langage, puis de développer les premiers outils permettant l'expérimentation. Fidèle à nos principes, ces travaux seront effectués avec en ligne de mire, l'applicabilité des résultats à des systèmes réels.

Le travail sera donc d'ordre fondamental, mais avec une participation dans les projets actuels de l'équipe relatif au domaine : l'AS155 "Approches formelles pour l'analyse et la synthèse sûre de contrôle des systèmes dynamiques hybrides" qui réunie des automaticiens et des informaticiens, et le projet européen ISAAC, afin d'avoir un retour d'éventuels utilisateurs.

Mot-clés : Systèmes hybrides, sémantique, modélisation, vérification.