\section{Sujet \thesujet : Modélisation et vérification temporelles en
AltaRica}\refstepcounter{sujet}\label{temps}

\subsection*{Fiche signalétique}

\begin{tabular}{llll}
{\bf Responsable} & Antoine Rauzy & 05 56 84 60 83 & Antoine.Rauzy@labri.u-bordeaux.fr \\
{\bf Collaborateur} & Alain Griffault & 05 56 84 69 15 & Alain.Griffault@labri.u-bordeaux.fr\\
{\bf Equipe} & \multicolumn{3}{l}{MVTsi}\\
{\bf Titre} & \multicolumn{3}{l}{\begin{tabular}{p{4in}}Modélisation et vérification temporelles en AltaRica.\end{tabular}}\\
{\bf Catégorie} & \multicolumn{3}{l}{Théorique et expérimentale}\\
{\bf Position/AltaRica} & \multicolumn{3}{l}{Définition du langage}\\
 & \multicolumn{3}{l}{Court et Moyen termes}\\
{\bf Financement} & \multicolumn{3}{l}{Bourse de thèse MENRT}
\end{tabular}

\subsection*{Présentation du sujet}

\begin{description}
\item[Contexte] 

Les systèmes critiques et/ou complexes représentant des systèmes
industriels font très souvent références au temps. Celui-ci sert pour
indiquer des informations de natures quelques fois très différentes~:

\begin{itemize}
\item Des informations statistiques et/ou stochastiques sur les
  occurrences de certains événements.
\item Des informations de causalité entre événements.
\item Des délais pendant lesquels des événements sont impossibles.
\item Des délais pendant lesquels des événements sont possibles.
\item Des durées pour l'accomplissement de certains événements.
\end{itemize}

Le sémantique de l'actuelle version du langage AltaRica vis à vis du
temps est la suivante~: les événements et le changement global d'état
qui en découle sont de durée nulle. C'est à dire, que le langage
AltaRica permet de décrire des systèmes réactifs, ou le temps est
assimilable aux entiers naturels.

Le langage AltaRica semble donc insuffisant pour traiter un certain
nombre de problèmes pour lesquels il a été défini.

\item[Travail demandé]

Le sujet de la thèse est l'étude du temps dans le projet AltaRica. Un
premier travail consistera à recenser et à formaliser les besoins
en terme d'ordonnancement, d'observateurs et de contrôleur de modèle
AltaRica.

Une seconde étape consistera à comparer les puissances d'expression
des modèles d'automates temporisés et/ou hybrides par rapport aux
automates à contraintes AltaRica.

La phase terminale devra, non seulement aboutir à des préconisations
pour le projet AltaRica; mais également à des recommandations d'ordre
méthodologiques pour la description en AltaRica d'un système temporisé.

\item[Environnement]

La thèse s'appuiera évidemment sur les exemples temps-réels
académiques, mais également sur plusieurs exemples de systèmes
industriels qui sont d'ores et déjà disponibles (au LaBRI) et font
l'objet de collaboration entre le LaBRI et divers partenaires
industriels (CEA, Aerospatiale).

\end{description}

