Vérification de logiciels

La validation et la vérification des logiciels sont aujourd'hui des enjeux majeurs, tant industriels qu'économiques; de plus en plus, la maîtrise de ces aspects influe directement sur la réussite de l'entreprise. Différentes techniques vérifient formellement tout ou partie de logiciels critiques dont il faut impérativement garantir la correction. Cet ouvrage est consacré à l'une des techniques les plus utilisées et les plus efficaces, le model-checking. Le model-checking a permis de découvrir et de mieux circonscrire des erreurs au sein d'applications industrielles (protocole de contrôle audio Bang et Olufsen, supervision de fabrication distribuée Renault, téléphonie cellulaire Motorola). L'usage du model-checking connaît donc un réel essor, notamment dans des domaines d'applications tels que le contrôle de bus informatiques, les protocoles de communication ; la commutation téléphonique ; les systèmes de contrôle-commande en automatique ; Les circuits intégrés. Divisé en trois parties, cet ouvrage propose, dans un premier temps, des explications concernant les principes fondamentaux de cette technique (modélisation par automates finis, produit synchronisé d'automates, logique temporelle, algorithmes de model-checking, model-checking symbolique, systèmes temporisés). La deuxième partie est, elle, consacrée à des questions pratiques liées à l'écriture des propriétés de correction et aux approches permettant de les vérifier. Enfin, plusieurs outils de model-checking sont présentés en fin de volume. Rédigé par une équipe de spécialistes, ce guide en langue française est le seul ouvrage disponible traitant du model-checking. Il intéressera tant les étudiants en second et troisième cycles d'informatique et d'automatique que les élèves des écoles d'ingénieurs. Ce livre a été rédigé par une équipe de chercheurs et d'enseignants-chercheurs du laboratoire Spécification et vérification, unité mixte de recherche n° 8643 de l'Ecole normale supérieure de Cachan et du CNRS. Ce travail col1ectif a été coordonné par Philippe Schnoebelen, chargé de recherche au CNRS.