Global ETD Search

1	Formal verification of a synchronous data-flow compiler : from Signal to C / Vérification formelle d’un compilateur synchrone : de Signal vers C Ngô, Van Chan 01 July 2014 (has links) 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. Vérification formelle Validation de la traduction Compilateur validé Programmes synchrones Modèles polychrones Systèmes embarqués Systèmes critiques Détection des blocages Compilation Polychrony Graphiques de dépendance SMT solving Valeur-graphiques Graphique réécriture. Formal verification Translation validation Validated Compiler Synchronous Programs Polychronous Models Embedded systems Safety-critical systems Deadlock detection Compilation Polychrony Dependency graphs SMT solving Value-graphs Graph rewriting.
2	Vérification Formelle d'un Compilateur Synchrone: de Signal vers C Ngo, Van Chan 01 July 2014 (has links) (PDF) Les langages synchrones tels que SIGNAL, LUSTRE et ESTEREL sont dédiés à la conception de systèmes critiques. Leurs compilateurs, qui sont de très gros programmes complexes, peuvent a priori se révéler incorrects dans certains situations, ce qui donnerait lieu alors à des résultats de compilation erronés non détectés. Ces codes fautifs peuvent invalider des propriétés de sûreté qui ont été prouvées en appliquant des méthodes formelles sur les programmes sources. En adoptant une approche de validation de la traduction, cette thèse vise à prouver formellement la correction d'un compilateur optimisé et industriel de SIGNAL. La preuve de correction représente dans un cadre sémantique commun le programme source et le code compilé, et formalise une relation entre eux pour exprimer la préservation des sémantiques du programme source dans le code compilé. Vérification formelle Validation de la traduction Compilateur validé Programmes synchrones Modèles polychrones Systèmes embarqués Systèmes critiques Détection des blocages Compilation Polychrony Graphiques de dépendance SMT solving Valeur-graphiques Graphique réécriture

Search results

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 Formelle d'un Compilateur Synchrone: de Signal vers C