Les méthodes formelles sont principalement utilisées lorsqu’une très forte assurance d’absence de bug est requise pour un logiciel. Face à l’augmentation de la complexité des systèmes à vérifier, l’exhaustivité des méthodes formelles apporte un niveau de garantie qui n’est plus atteignable à l’aide des techniques de tests classiques. Cette session a pour objectif de montrer la valeur ajoutée des méthodes formelles au cours d’un cycle de développement Model-Based Design via l’utilisation de Simulink Design Verifier™ au niveau modèle et de Polyspace^® au niveau modèle et code source.