Abstract FR:

Les systèmes temps-réels critiques présentent des caractéristiques spécifiques et imposent des contraintes de sûreté qui doivent être prises en compte dès la spécification. La modélisation formelle de ces systèmes permet leur validation et la définition de procédés fiables pour leur mise en oeuvre. L'approche objet permet en outre le développement par raffinement des comportements grâce à la notion centrale d'héritage. Nous nous intéressons au modèle synchrone dans lequel seules les notions de précédence et de simultanéité d'événements entrent en jeu. Nous étudions l'orientation objet de ce formalisme en introduisant des mécanismes d'encapsulation et d'héritage comportemental. La notion de renommage constitue ici une version spatiale de l'itération temporelle de l'algorithme classique de recherche des méthodes. La notion d'horloge de méthode permet de propager les informations de synchronisation et ainsi d'échapper à de nombreux cas d'anomalies de l'héritage.