Génération automatique d'observateurs pour la vérification formelle d'exigences temporelles

Dote d’une semantique formelle, outille [4] [3], le profil UML temps reel TURTLE (Timed UML and RT-LOTOS Environment) couvre les phases d’analyse, conception et prototypage des systemes distribues [1]. Son utilisation est d’autant plus justifiee lorsque le systeme a concevoir necessite de verifier formellement des exigences temporelles et de tracer les dites exigences au long du cycle de developpement du systeme. L’objectif de ce poster est de montrer les dernieres avancees en matiere de traitement des exigences temporelles : expression de ces exigences dans un langage dedie, synthese automatique d’observateurs pour guider la verification et construction de matrices de tracabilite.