Description
Utilisations industrielles des techniques formelles
interprétation abstraite
Traité RTA, série Informatique et Systèmes d'Information
Author: BOULANGER Jean-Louis
Language: FrenchSubjects for Utilisations industrielles des techniques formelles:
Publication date: 06-2011
416 p. · 15.6x23.4 cm · Hardback
Withdrawn from sale
416 p. · 15.6x23.4 cm · Hardback
Withdrawn from sale
Description
/li>Contents
/li>
Cet ouvrage présente des exemples concrets d'utilisations industrielles des techniques formelles.
Ces techniques réalisent des modèles de spécifications et/ou de conception et servent également à l'analyse statique de code, à la démonstration du respect de propriété, à la bonne gestion des calculs sur les flottants, etc...
Les standards des différents domaines prennent en compte la mise en oeuvre des méthodes formelles comme moyen de construire un logiciel critique de sécurité.
Les exemples industriels de mise en oeuvre des techniques formelles basées sur l'analyse statique, comme l'interprétation abstraite avec des exemples d'utilisation des outils Astrée, Caveat, CodePeer, Framac ou Polyspace sont détaillés.
Ces techniques réalisent des modèles de spécifications et/ou de conception et servent également à l'analyse statique de code, à la démonstration du respect de propriété, à la bonne gestion des calculs sur les flottants, etc...
Les standards des différents domaines prennent en compte la mise en oeuvre des méthodes formelles comme moyen de construire un logiciel critique de sécurité.
Les exemples industriels de mise en oeuvre des techniques formelles basées sur l'analyse statique, comme l'interprétation abstraite avec des exemples d'utilisation des outils Astrée, Caveat, CodePeer, Framac ou Polyspace sont détaillés.
Introduction. Chapitre 1. Techniques formelles pour la vérification et la validation. Chapitre 2. L'analyseur statique Astrée. Chapitre 3. Airbus : vérification formelle en avionique. Chapitre 4. Polyspace. Chapitre 5. Robustesse logicielle vis-à-vis de valeurs dysfonctionnelles par analyse statique. Chapitre 6. CodePeer : au-delà de la recherche de bugs avec l'analyse. Chapitre 7. Méthodes formelles et conformité au standard DO-178C/ED-12C en aéronautique. Chapitre 8. Analyse statique de code : une méthode intégrée outillée développée par thales pour l'étude du passage en entiers et des débordements pour des composants logiciels SIL4. Chapitre 9. Conclusion et perspectives. Glossaire. Index.
© 2024 LAVOISIER S.A.S.