Vérification de modèles pour les logiciels
La vérification de modèles vérifie automatiquement si le modèle d'un système satisfait une spécification en logique temporelle en explorant de manière exhaustive ses états atteignables.
Definition
La vérification de modèles est une technique de vérification automatique qui, étant donné un modèle à états finis d'un système et une spécification en logique temporelle, vérifie de manière exhaustive si la spécification est respectée et produit une trace de contre-exemple si ce n'est pas le cas.
Scope
Ce sujet couvre la vérification automatique des systèmes à états finis et concurrents par rapport aux propriétés de logique temporelle (sûreté et vivacité), le problème de l'explosion d'états et les techniques pour le combattre (représentation symbolique avec des diagrammes de décision binaires, réduction par ordre partiel, abstraction), la vérification de modèles bornée avec SAT/SMT, et l'affinage d'abstraction guidé par contre-exemple pour les logiciels.
Core questions
- Comment une propriété peut-elle être vérifiée en explorant tous les états atteignables ?
- Qu'est-ce que le problème de l'explosion d'états et comment est-il atténué ?
- Comment les méthodes symboliques et bornées permettent-elles de faire évoluer la vérification de modèles ?
- Comment les systèmes logiciels à états infinis sont-ils abstraits en modèles finis ?
Key theories
- Vérification de modèles par logique temporelle
- Clarke, Emerson et Sistla, et indépendamment Queille et Sifakis, ont introduit des algorithmes pour vérifier automatiquement les systèmes concurrents à états finis par rapport aux spécifications en logique temporelle.
- Vérification de modèles symbolique
- Burch et ses collègues ont représenté symboliquement des ensembles d'états à l'aide de diagrammes de décision binaires, permettant la vérification de systèmes comportant un nombre astronomique d'états et surmontant l'explosion d'états naïve.
Clinical relevance
La vérification de modèles est utilisée pour vérifier les conceptions matérielles (hardware), les protocoles de communication, et les logiciels concurrents et critiques pour la sécurité, où elle permet de détecter des bogues subtils que les tests ne parviennent pas à identifier et fournit des contre-exemples qui localisent les défaillances. Son automatisation la distingue de la démonstration de théorèmes interactive.
History
S'appuyant sur l'introduction de la logique temporelle pour les programmes par Pnueli, Clarke et Emerson et, indépendamment, Queille et Sifakis ont conçu la vérification de modèles vers 1981-82, un travail ultérieurement récompensé par un prix Turing. La vérification de modèles symbolique avec des diagrammes de décision binaires (années 1990) et la vérification de modèles bornée basée sur SAT ont considérablement étendu sa portée, et les méthodes d'abstraction-raffinement l'ont appliquée aux logiciels.
Debates
- Lutte contre l'explosion d'états
- Le défi central est que le nombre d'états croît exponentiellement avec la taille du système ; les chercheurs débattent du meilleur mélange de représentation symbolique, d'abstraction, de réduction par ordre partiel et de vérification bornée pour maintenir la vérification traitable.
Key figures
- Edmund Clarke
- E. Allen Emerson
- Joseph Sifakis
- Kenneth McMillan
- Amir Pnueli
Related topics
Seminal works
- clarke1986
- queille1982
- burch1992
Frequently asked questions
- En quoi la vérification de modèles diffère-t-elle de la démonstration de théorèmes ?
- La vérification de modèles est entièrement automatique et explore de manière exhaustive l'espace d'états d'un système pour des modèles finis ou abstraits, tandis que la démonstration de théorèmes utilise la déduction logique (souvent de manière interactive) et peut gérer des systèmes à états infinis mais nécessite davantage de guidage humain.
- Qu'est-ce que le problème de l'explosion d'états ?
- C'est la croissance exponentielle du nombre d'états atteignables à mesure qu'un système acquiert des composants ou des variables, ce qui limite la vérification de modèles naïve et motive les techniques symboliques, bornées et basées sur l'abstraction.