Université de Rennes 1 Formal verification of a synchronous data-flow compiler : from Signal to C Vérification formelle d’un compilateur synchrone: de Signal vers C Vérification formelleValidation de la traductionCompilateur validéProgrammes synchronesModèles polychronesSystèmes embarquésSystèmes critiquesDétection des blocagesCompilationPolychronyGraphiques de dépendanceSMT solvingValeur-graphiquesGraphique réécriture. Formal verificationTranslation validationValidated CompilerSynchronous ProgramsPolychronous ModelsEmbedded systemsSafety-critical systemsDeadlock detectionCompilationPolychronyDependency graphsSMT solvingValue-graphsGraph rewriting. Méthodes formelles (informatique) Thèses et écrits académiques Compilateurs (logiciels) Thèses et écrits académiques Les langages synchrones tels que Signal, Lustre et Esterel sont dédiés à la conception de systèmes critiques. Leurs compilateurs, qui sont de très gros programmes complexes, peuvent a priori se révéler incorrects dans certains situations, ce qui donnerait lieu alors à des résultats de compilation erronés non détectés. Ces codes fautifs peuvent invalider des propriétés de sûreté qui ont été prouvées en appliquant des méthodes formelles sur les programmes sources. En adoptant une approche de validation de la traduction, cette thèse vise à prouver formellement la correction d'un compilateur optimisé et industriel de Signal. La preuve de correction représente dans un cadre sémantique commun le programme source et le code compilé, et formalise une relation entre eux pour exprimer la préservation des sémantiques du programme source dans le code compilé. Synchronous languages such as Signal, Lustre and Esterel are dedicated to designing safety-critical systems. Their compilers are large and complicated programs that may be incorrect in some contexts, which might produce silently bad compiled code when compiling source programs. The bad compiled code can invalidate the safety properties that are guaranteed on the source programs by applying formal methods. Adopting the translation validation approach, this thesis aims at formally proving the correctness of the highly optimizing and industrial Signal compiler. The correctness proof represents both source program and compiled code in a common semantic framework, then formalizes a relation between the source program and its compiled code to express that the semantics of the source program are preserved in the compiled code. Electronic Thesis or DissertationText en application/zip1 : 1269 Kohttps://ecm.univ-rennes1.fr/nuxeo/site/esupversions/e10492b5-206a-42fa-b643-e752dac5a750 Ngô Van Chan 1981-03-22 VN 180731211 chan.ngo2203@gmail.com 2014REN1S034 http://www.theses.fr/2014REN1S034 2014-07-01 Informatique Université de Rennes 1thesis.degree.grantor_1 02778715X Doctorat non ouiTalpinJean-Pierreintervenant_1094211515 Mathématiques, informatique, signal, électronique et télécommunicationsecoleDoctorale_1 139007164 IRISApartenaireRecherche_1 026386909 Université européenne de BretagnepartenaireRecherche_2 139075119 ddc:004 TalpinJean-PierreUniversité de Rennes 1Sciences et technologie, médecine, pharmacie, odontologie, droit, économie, gestion, philosophieMathématiques, informatique, signal, électronique et télécommunicationsÉcole doctorale Mathématiques, informatique, signal, électronique et télécommunications (Rennes)IRISAUniversité européenne de Bretagne ASCII PDF 1299115