Model checking (ou vérification des systèmes réactifs)

Le model checking  est un domaine de l’informatique ayant pour but de vérifier le bon fonctionnement des systèmes concurrents ou réactifs. Ce domaine est en relation étroite avec le  domaine de la logique mathématique, plus particulièrement avec la logique temporelle linéaire propositionnelle, ou encore la logique temporelle arborescente. 

Les logiciels du model checking sont issus d’une recherche intensive dans le domaine d’exploration d’états de système à transition finis. Ce domaine a connu de nombreux apports dans la tâche de réduction du volume de l’exploration, comme la méthode du « Partial Order Reduction » par exemple.

Différents logiciels comme Spin [1] et Uppaal [2], nous permettent de décrire et de représenter notre système concurrent par un modèle simplifié, et de le vérifier par rapport à des propriétés de sûreté, de vivacité ou d’équité. Les propriétés de sûreté nous garantissent qu’un mauvais état de fonctionnement n’est jamais atteint, tandis que les propriétés de vivacité nous garantissent qu’un état convenable survient finalement, les propriétés d’équité nous garantissent que toutes les séquences d’exécution laissent les autres séquences accessibles aussi.

Les logiciels du model checking permettent par exemple de vérifier les algorithmes classiques des systèmes répartis (Spin en particulier) comme les algorithmes d’élection d’un chef, la terminaison d’un calcul et l’exclusion mutuelle. Aussi on peut vérifier les protocoles de communication comme le protocole du bit alterné, ajoutons aussi qu’on peut vérifier les propriétés de sécurité des protocoles de cryptographie. Les systèmes réactifs en temps réel peuvent être vérifiés à l’aide du logiciel Uppaal qui permet la modélisation des systèmes en des automates temporisés, et assure la vérification des propriétés sur les systèmes en utilisant des conditions portant sur le temps entre les événements.

En résumé, le model checking nous propose un  moyen simple et efficace pour la vérification des systèmes réactifs ou concurrents en utilisant des abstractions qui facilitent notre vue du système à vérifier.

[1] Spin outil de vérification. http://spinroot.com

[2] Uppaal outil de vérification. http://uppaal.org