Vous cherchez un livre qui construit et une dérive l'application de vérification de modèle

Question

Je suis moi-même la vérification du programme d'enseignement et apprends actuellement assistants de preuve . Je le livre Manuel du Raisonnement logique et automatisé pratique qui donne les preuves nécessaires à la compréhension d'un tel système, mais plus important encore pour moi, il donne également une implémentation des algorithmes nécessaires comme OCAML la source .

Je sais que certains des outils énumérés dans Wikipedia: Model Checking outils et YAHODA: Base de données Outils Verifications sont open source, mais je préfère aussi quand la théorie, les preuves, les algorithmes et la source Code sont présentés en même temps de renfort de l'autre, et dans une progression mise en place à une application finale.

Y at-il un tel livre pour la vérification du modèle?

EDIT

Je peut avoir trouvé ce que je cherche dans logique mathématique pour la science informatique avec de source Prolog. Comme je n'ai pas le livre, personne ne sait si ce livre correspond à l'exigence?

Answer 1

Le livre de John Harrison est une exception dans tout le chemin de la théorie à la pratique et de faire tout le code source disponible. Je pense que vous trouverez qu'il est difficile de trouver un livre équivalent pour la vérification du modèle, mais il y a quelques qui permettent d'atteindre une bonne approximation.

• Principes de Model Checking par Baier et Katoen contient beaucoup d'exemples et assez détaillés Description algorithmiques.
• Le modèle SPIN Vérificateur par Gérard Holzmann est un traitement très différent de l'auteur l'un des premiers contrôleurs de modèle. Il a maintenu l'outil pour une trentaine d'années et a une approche « programmatique ».

Un meilleur pari peut être de suivre les notes de cours et les affectations laboratoire de certains cours disponibles en ligne. Au moins, vous trouverez la théorie, la pratique et des exemples, même si elles ne sont pas organisées dans un livre.

• le cours Edmund Clarke à la CMU a une liste de lecture qui comprend des tutoriels pour quelques contrôleurs de différents modèles.
• Joost-Pieter cours de vérification du logiciel de Katoen et le suivi sur Modèle pratique Vérification et Modèle avancé Vérification couvrir beaucoup de terrain.

Enfin, ce n'est pas tout à fait ce que vous avez demandé, mais puisque vous avez été en train d'étudier la logique et la vérification maintenant modèle, vous toujours courir dans des références à l'interprétation abstraite, qui est la base d'une analyse statique de programmes et est intimement lié au modèle vérifier (bien que cette connexion est pas toujours explicite dans le modèle de vérification littérature).

• cours du MIT Patrick Cousot est un tour de force couvrant tout de fondations au treillis théorétiques la mise en œuvre complète d'un analyseur statique pour un langage simple. Son matériel de cours comprend tout le code et les exercices.