Les méthodes formelles :
permettent de définir mathématiquement et rigoureusement les propriétés de fonctionnement d’un système. Les méthodes formelles peuvent s’appliquer à n’importe quel stade de développement d’un projet, aussi bien en phase de spécification qu’en phase d’implémentation.
La sûreté de fonctionnement :
vise à garantir avec un certain niveau de confiance l’impossibilité de comportements dangereux d’un système ou d’un équipement. Autrement dit, cette « assurance de bon fonctionnement » impose la maîtrise claire et rigoureuse du fonctionnement de ce système ou de cet équipement.
Ainsi, les méthodes formelles, hautement recommandées au tout début du cycle de développement d’un système c’est-à-dire dans les phases de spécification des prescriptions de sécurité d’un système à haut niveau d’intégrité (SIL4 pour EN 61508, et SIL3 SIL4 pour l’EN 50128), apportent au processus de sûreté de fonctionnement des prescriptions de sécurité spécifiées de manière structurée claire, précise, univoque, vérifiable, testable, maintenable, et exempte de toute terminologie ou description ambiguë et/ou susceptible d’être mal comprise par les utilisateurs du document à tous les stades du cycle de développement.