V&V
Vérification
Méthodes formelles
- Modèle de système (S) \ra systèmes de transitions, code
- Modèle des exigences (\phi) \ra logiques (prédicats [premier ordre], temporelles, …)
Question posée : S = \phi ? \RA Model checking (explorer tous les chemins possibles pour vérifier des propriétés) ou Theorem proving (pareil mais différents, avec KeY par exemple pour les programmes java)