Description
Outils de mise en oeuvre industrielle des techniques formelles
Traité RTA, série Informatique et Systèmes d'Information
Coordinator: BOULANGER Jean-Louis
Language: FrenchSubjects for Outils de mise en oeuvre industrielle des techniques...:
Publication date: 04-2012
390 p. · 15.6x23.4 cm · Hardback
Withdrawn from sale
390 p. · 15.6x23.4 cm · Hardback
Withdrawn from sale
Description
/li>Contents
/li>
Les techniques formelles réalisent des modèles de
spécifications et/ou de conception et servent principalement à l'analyse
statique de code, à la démonstration du respect de propriété et à la bonne
gestion des calculs sur les flottants.
Différents domaines tels les systèmes de transport, la production d'énergie ou la santé prennent en compte l'implémentation de ces méthodes pour satisfaire les exigences de sécurité élevées des systèmes critiques. Leur mise en œuvre dans le cadre d'une application industrielle (application de grande taille, contrainte de coût et de délais, etc.) ne peut se faire que par l'emploi d'outils suffisamment matures et performants.
Cet ouvrage collectif présente des exemples concrets d'utilisation des techniques formelles comme la méthode B, SCADE, MaTeLo, ControlBuild, SparkAda et POLYSPACE et des techniques de vérification associées. Il en identifie aussi les avantages et les difficultés.
Différents domaines tels les systèmes de transport, la production d'énergie ou la santé prennent en compte l'implémentation de ces méthodes pour satisfaire les exigences de sécurité élevées des systèmes critiques. Leur mise en œuvre dans le cadre d'une application industrielle (application de grande taille, contrainte de coût et de délais, etc.) ne peut se faire que par l'emploi d'outils suffisamment matures et performants.
Cet ouvrage collectif présente des exemples concrets d'utilisation des techniques formelles comme la méthode B, SCADE, MaTeLo, ControlBuild, SparkAda et POLYSPACE et des techniques de vérification associées. Il en identifie aussi les avantages et les difficultés.
Introduction - Jean-Louis BOULANGER. Chapitre 1. Des langages
classiques aux méthodes formelles. Chapitre 2. SCADE : mise en oeuvre et
applications. Chapitre 3. SPARK, un langage et une boîte à outils pour le
développement de logiciel critique. Chapitre 4. ControlBuild. Chapitre 5.
Model Based Testing. Génération automatique de cas de test à l'aide d'une
modélisation par chaînes de Markov. Chapitre 6. Analyse de sécurité des
systèmes embarqués avec AltaRica. Chapitre 7. Méthode B et outils B.
Chapitre 8. Polyspace. Chapitre 9. Synthèse et conclusions. Conclusion.
Bibliographie. Glossaire. Index.
© 2024 LAVOISIER S.A.S.