Méthodes formelles (informatiques), techniques qui permettent de raisonner rigoureusement, aide de logique mathématique, sur un programme informatique, ou du matériel électronique numérique.
Forte assurance de l'absence de bug dans les logiciels (Evaluation Assurance Level, Safety Integrity Level), utilisées dans le développement des logiciels les plus critiques. Différentes approches (démonstration de théorèmes, BDDs (pour Binary Decision Diagrams). Problème SAT ou problème de satisfaisabilité booléenne. Système de déduction de la logique mathématique, en particulier dans le calcul des prédicats. Système concret (mise au point des algorithmes, réalisation en logiciel et/ou circuit électronique) : si la spécification formelle est dotée d'une sémantique opérationnelle, si la spécification formelle est dotée d'une sémantique axiomatique.
L'approche basée sur des états
- Z
- SAZ
- Méthode B classique
- ASM
- TLA+
L'approche basée sur des événements
- Action Systems
- Méthode B événementielle
- VHDL
- Esterel
- SDL
- LOTOS
- E-LOTOS
- EB3
L'approche basée sur les contrats
- Eiffel
Algébrique :
- Larch : Larch family
- CASL : Common Algebraic Specification Language
L'Assistants de preuve :
- Rocq
- Isabelle
- Metamath
Autres approches et outils
- Réseau de Petri
- Algèbre de processus
- ACL2 : démonstration de théorèmes automatisée,
- AtelierB : spécification et preuve avec la méthode B,
- CADP : construction et analyse de processus distribués,
- Rocq : assistant d'aide à la preuve,
- Murφ : démonstration de propriétés,
- Prototype Verification System : assistant d'aide à la preuve,
- SMV, nuSMV : démonstration de propriétés avec BDDs et SAT,
- zChaff : démonstration avec SAT.
