Une technique de vérification automatique qui explore exhaustivement l'espace d'états d'un modèle formel d'un système (généralement un système de transition à états finis) pour déterminer si le modèle satisfait une spécification exprimée dans une logique temporelle ou modale, et qui fournit des traces contre‑exemples lorsque la propriété est violée.

Principe

Traduire le système en un modèle d'états fini ou symbolique, exprimer la propriété désirée dans une logique de spécification (par ex. LTL, CTL) et effectuer une exploration exhaustive (explicite, symbolique, bornée ou réduite par ordre partiel) des états atteignables pour vérifier la propriété ; les contre‑exemples sont des traces d'exécution concrètes violant la propriété.

Démonstration

Vérifier une propriété de sécurité LTL sur un système concurrent à états finis en utilisant la vérification symbolique avec BDDs ou la vérification bornée par SAT : si la propriété échoue, l'outil renvoie une trace finie montrant la séquence de transitions conduisant à la violation, utilisable pour le débogage.

Mauvaise application

Appliquer la vérification de modèles naïvement à des systèmes à états infinis sans abstraction, supposer que la vérification bornée prouve des propriétés non bornées, ou interpréter à tort des contre‑exemples produits sous abstraction (contre‑exemples spurieux) comme des bugs réels.

Conséquence

La vérification par modèles fournit une détection de bogues guidée par contre‑exemples entièrement automatique et, lorsque c'est possible, des garanties de correction pour le modèle exploré ; elle impose une formalisation précise du comportement et des exigences du système mais se heurte au problème d'explosion de l'espace d'états qui limite l'évolutivité.

Inversion

Au lieu d'une exploration exhaustive des états, on peut employer la vérification déductive ou la preuve assistée qui raisonne symboliquement sur des classes de comportements ; l'inversion échange l'automatisation et les contre‑exemples concrets contre la généralité et des obligations de preuve.

Limite

Adaptée aux systèmes à états finis ou représentables finiment, ou aux systèmes susceptibles d'abstraction correcte ; différentes logiques et types de modèles (temporel, probabiliste, hybride) exigent des algorithmes étendus. La vérification par modèles porte sur la correction du modèle par rapport à une spécification, pas sur le code d'implémentation ou les hypothèses d'environnement sauf si elles sont modélisées.

Tension sémantique

Il existe une tension entre l'exploration en explicit state, les méthodes symboliques (BDD, SAT/SMT) et les approches abstraction/raffinement : ces choix influent sur l'évolutivité, l'interprétabilité des contre‑exemples et le caractère exhaustif ou borné des résultats. On trouve aussi le compromis entre recherche entièrement automatique et techniques de preuve interactives.

Synthèse

La vérification par modèles est une analyse automatisée et exhaustive d'un modèle formel par rapport à des spécifications temporelles ou logiques qui fournit contre‑exemples concrets pour le débogage et, le cas échéant, des garanties de correction ; son efficacité dépend de la représentation, de l'abstraction et des techniques de recherche qui atténuent l'explosion d'états.