Return to search

Vérification Formelle d'un Compilateur Synchrone: de Signal vers C

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é.

Identiferoai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-01058041
Date01 July 2014
CreatorsNgo, Van Chan
PublisherUniversité Rennes 1
Source SetsCCSD theses-EN-ligne, France
LanguageEnglish
Detected LanguageFrench
TypePhD thesis

Page generated in 0.0022 seconds