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

Génie Logiciel

Le génie logiciel est une branche du génie qui a pour but de concevoir, d’appliquer et de mettre à jour les processus, méthodes et techniques du développement et de la mise en œuvre  des logiciels informatiques dans divers champs d’applications allant des mobiles, PCs, serveurs, jusqu’aux grandes machines parallèles. Ces logiciels sont conçus de manière à éviter ou à minimiser les fautes ou erreurs de fonctionnement ou de déploiement, et ont pour but le bien-être, la sécurité et la satisfaction des clients ou des organisations.

Le génie logiciel propose des méthodes complètes couvrant tout le cycle de vie d’un logiciel ou d’un système informatique, de la spécification des exigences, jusqu’au déploiement et maintenance du logiciel. Ces méthodes font preuve de robustesse, de fiabilité et de répétabilité par rapport à leur fonctionnement attendu. En plus du fonctionnement attendu, des attributs de qualité  comme la maintenabilité, évolutivité et réutilisabilité font aussi partie du cahier des charges des logiciels.

Le génie logiciel regroupe plusieurs sous-domaines comme l’architecture logicielle, l’approche orientée objet et l’intégration entre systèmes, et a des pistes communes avec d’autres domaines du génie et de la gestion, comme la spécification des cahiers des charges et la gestion des projets, respectivement.