Abstract FR:

Ces dernieres annees, la verification des systemes informatiques critiques est devenue un sujet de recherche important en raison du developpement croissant de logiciels pour la medecine, les moyens de transports ou les centrales nucleaires. Dans ces domaines, une erreur de programmation peut couter tres cher financierement ou en vies humaines. Dans ce cadre, les informaticiens ont ete amenes a developper des langages dits synchrones dedies a la programmation des systemes reactifs. Un systeme reactif est un systeme qui reagit continument avec son environnement a un vitesse imposee par son environnement. Il ne termine pas forcement et peut etre concurrent. En general, la concurrence entraine le non-determinisme mais le modele synchrone se distingue par le fait qu'il fait cohabiter concurrence et determinisme. Dans cette these, nous avons formalise dans l'outil d'aide a la preuve coq une version co-inductive de la semantique des traces du langage synchrone signal. Nous avons choisi d'utiliser la co-induction car nous pensons qu'il s'agit la d'un outil mathematique naturel et simple pour manipuler des objets infinis tels que les signaux. La pratique nous permet de confirmer que la co-induction est un outil efficace pour prouver la correction d'un systeme reactif specifie en signal. Afin de pouvoir traiter la causalite dans les programmes synchrones, nous avons ensuite generalise cette approche en developpant une variante des structures d'evenements que nous appelons les structures synchrones. Par cette approche, il est possible de traiter les dependances conditionnees entres signaux et il n'est pas necessaire de denoter l'absence d'un signal par une valeur speciale comme cela est fait usuellement. C'est plus en accord avec la realite car l'absence d'un signal doit etre inferee par le programme (endochronie).