Outils de mise en oeuvre industrielle des méthodes formelles

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.