À retenir
- C'est une méthode exhaustive : elle ne laisse aucune place au hasard contrairement aux tests classiques.
- Elle fournit un contre-exemple (une trace d'exécution) précis quand une erreur est détectée.
- Elle repose sur une base mathématique solide appelée logique temporelle.
L'exploration de modèle est une technique automatique de vérification qui examine tous les états possibles d'un système pour s'assurer qu'il respecte bien ses règles de sécurité et de fonctionnement. C'est un peu comme si un ordinateur testait chaque embranchement d'un scénario complexe pour garantir qu'aucune erreur ne peut jamais survenir, peu importe les circonstances.
Étymologie
Traduction littérale de l'anglais Model Checking. Le terme est apparu au début des années 1980 avec les travaux de chercheurs comme Edmund M. Clarke et Allen Emerson. Il désigne l'acte de vérifier (checking) une abstraction mathématique (model) d'un programme.
Exemples d'usage
- Vérifier qu'un système de freinage automatique s'active systématiquement en cas d'obstacle, sans exception possible.
- S'assurer qu'un protocole de communication réseau ne se retrouve jamais dans un état de
deadlock(blocage mutuel) où plus aucun message ne circule.
Cas d'usage
On l'utilise principalement dans les domaines où une erreur logicielle ou matérielle peut être catastrophique : l'aéronautique, l'industrie nucléaire, la conception de microprocesseurs ou le développement de protocoles cryptographiques.
Bonnes pratiques
Pour que l'exploration soit efficace, il faut simplifier le modèle au maximum (abstraction) afin d'éviter l'explosion combinatoire, un phénomène où le nombre de situations à tester devient trop grand pour les capacités de calcul de l'ordinateur.
Synonymes
Antonymes
Conseil
Considérez l'exploration de modèle comme un outil de preuve mathématique automatisé. Si vous travaillez sur du code critique, apprenez à définir des spécifications claires (ce que le programme DOIT ou ne DOIT JAMAIS faire) avant même de coder.
Questions fréquentes
Quelle est la différence avec un test logiciel ?
Un test ne vérifie que certains scénarios choisis, alors que l'exploration de modèle vérifie absolument toutes les combinaisons possibles du système.
Est-ce que cela remplace les tests ?
Non, car l'exploration travaille sur un modèle simplifié du système, alors que les tests s'exécutent sur le produit réel final.