Il est bien rare qu’un programme d’automate ou d’une application de sécurité soit bon du premier coup. Même si le programmeur fait preuve d’une grande rigueur. Il existe des techniques pour améliorer les choses, utilisées notamment dans le domaine de la conception des composants électroniques et de la conception des systèmes de sécurité dans les transports. C’est le cas notamment des méthodes formelles avec preuve…