Nowak, David
Thèse de : Rennes 1
176 pages - 1999 - Document en français
Abstract : In recent years, the verification of safety critical systems has become an area of increasing importance in computer science because of the constant progression of software developments in sensitive fields like medicine, communication, transportation and (nuclear) energy. Such systems are often concurrent. These strong requirements have led to the development of specific programming languages and related verification tools for concurrent systems. We focus our research on concurrent systems that continuously react to their environment at a speed determined by this environment. They are called reactive systems. Synchronous languages, such as Signal, are best suited for the design of reactive systems. Synchronous languages enable a very high-level specification and an extremely modular implementation of complex systems by structurally decomposing them into elementary synchronous processes. We investigate the use of a proof assistant for the specification of infinite state systems and for the verification of co-inductive properties. We formalize the trace semantics of Signal within the proof assistant Coq. We choose to use co-inductive features of Coq because we find it is a natural and simple mathematical tool to handle infinite objects such as signals. Our practice confirms that this is also an efficient way to prove correctness properties of reactive systems specified in Signal. We then generalize our previous approach to be able to deal with causality in synchronous programs. We develop a variant of event structures that we call synchronous structures. Within this approach, we can deal with causality and we need not denote the absence of a signal by a special value as it is done usually. It is more consistent with reality because the absence of a signal has to be inferred by the program (endochrony).
Résumé : Ces dernières années, la vérification des systèmes informatiques critiques est devenue un sujet de recherche important en raison du développement croissant de logiciels pour la médecine, les moyens de transports ou les centrales nucléaires. Dans ces domaines, une erreur de programmation peut coûter très cher financièrement ou en vies humaines. Dans ce cadre, les informaticiens ont été amenés à développer des langages dits synchrones dédiés à la programmation des systèmes réactifs. Un système réactif est un système qui réagit continûment avec son environnement à une vitesse imposée par son environnement. Il ne termine pas forcément et peut être concurrent. En général, la concurrence entraîne le non-déterminisme mais le modèle synchrone se distingue par le fait qu'il fait cohabiter concurrence et déterminisme. Dans cette thèse, nous formalisons dans l'outil d'aide à la preuve Coq une version co-inductive de la sémantique des traces du langage synchrone Signal. Nous utilisons la co-induction car nous pensons qu'il s'agit là d'un outil mathématique 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 système réactif spécifié en Signal. Afin de pouvoir traiter la causalité dans les programmes synchrones, nous généralisons ensuite cette approche en développant une variante des structures d'événements que nous appelons les structures synchrones. Par cette approche, il est possible de traiter les dépendances conditionnées entres signaux et il n'est pas nécessaire de dénoter l'absence d'un signal par une valeur spéciale comme cela est fait usuellement. C'est plus en accord avec la réalité car l'absence d'un signal doit être inférée par le programme (endochronie).
Key-Words : SYNCHRONOUS PROGRAMMING / PROOF ASSISTANT / SYNCHRONOUS STRUCTURE
