Footnote:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Description:
Cette thèse s'inscrit dans le domaine de la vérification dulogiciel. Le but de la vérification du logiciel est d'assurer qu'uneimplémentation, un programme, répond aux exigences, satisfait saspécification. Cela est particulièrement important pour le logicielcritique, tel que des systèmes de contrôle d'avions, trains oucentrales électriques, où un mauvais fonctionnement pendantl'opération aurait des conséquences catastrophiques.Les exigences du logiciel peuvent concerner la sûreté ou lefonctionnement. Les exigences de sûreté, tel que l'absence d'accès à lamémoire en dehors des bornes valides, sont souvent implicites, dans lesens que toute implémentation est censée être sûre. D'autre part, les exigences fonctionnelles spécifient ce que leprogramme est censé faire. La spécification d'un programme est souventexprimée informellement en décrivant en anglais la mission d'une partie du code source. La vérification duprogramme se fait alors habituellement par relecture manuelle,simulation et tests approfondis. Par contre, ces méthodes negarantissent pas que tous les possibles cas d'exécution sontcapturés. La preuve déductive de programme est une méthode complète pour assurerla correction du programme. Ici, un programme, ainsi que saspécification formalisée à l'aide d'un langage logique, est un objetmathématique et ses propriétés désirées sont des théorèmes logiques àprouver formellement. De cette façon, si le système logiquesous-jacent est cohérent, on peut être complètement sûr que lapropriété prouvée est valide pour le programme en question et pourn'importe quel cas d'exécution. La génération de conditions de vérification est une techniquecensée aider le programmeur à prouver les propriétés qu'il veut surson programme. Ici, un outil (VCG) analyse un programme donné avec saspécification et produit une formule mathématique, dont la validitéimplique la correction du programme vis à vis de saspécification, ce qui est particulièrement intéressant lorsque lesformules générées peuvent être prouvées automatiquement à l'aide ...