Abstract FR:

Ce travail presente les bases de l'architecture d'un systeme distribue, temps reel, sur de fonctionnement, se pretant bien a la validation. Ce systeme est base sur une implementation distribuee du modele synchrone a l'aide d'un temps logique distinct du temps reel. Une analyse temporelle du fonctionnement du systeme permet d'assurer le respect de la semantique synchrone, ainsi que le respect des contraintes temporelles de l'application. Des mecanismes de tolerance aux fautes peuvent etre decrits de maniere synchrone, la semantique des fautes, qui est precisee dans le langage, etant respectee a l'implementation. La distinction entre le temps reel et le temps logique entraine des modifications dans les techniques classiques de validation: la notion de temps reel est introduite dans la logique temporelle utilisee comme langage de specification, et les techniques de modelchecking sont modifiees pour en tenir compte