Titre :	V'ERIFICATION DE LOGICIELS : Techniques et outils du model-checking
Type de document :	texte imprimé
Auteurs :	Collection l'enseignement mathématique, Auteur
Editeur :	Paris : Presses polytechniques romandes
Année de publication :	1999
Importance :	197P
Format :	24x17cm
ISBN/ISSN/EAN :	978-2-7117-8646-6
Langues :	Français (fre) Langues originales : Français (fre)
Mots-clés :	Logiciels
Index. décimale :	004 Traitement de données. Informatique
Résumé :	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.

V'ERIFICATION DE LOGICIELS : Techniques et outils du model-checking [texte imprimé] / Collection l'enseignement mathématique, Auteur . - Paris : Presses polytechniques romandes, 1999 . - 197P ; 24x17cm.
ISBN : 978-2-7117-8646-6
Langues : Français (fre) Langues originales : Français (fre)

Mots-clés :	Logiciels
Index. décimale :	004 Traitement de données. Informatique
Résumé :	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.