Alla ricerca di un libro che deriva e costruisce un modello di applicazione di controllo

Question

sto insegnando me stesso verifica dei programmi e attualmente sto imparando assistenti prova . Ho il libro Handbook of Practical Logica e Ragionamento Automatico che dà le prove necessarie per la comprensione di tale sistema una, ma ancora più importante per me è dà anche un'implementazione degli algoritmi necessari come OCAML fonte .

So che alcuni degli strumenti elencati nella Wikipedia: Modello strumenti e YAHODA: Verifiche Strumenti database sono open source, ma anche lo preferisco quando la teoria, prove, algoritmi e fonte codice sono presentati allo stesso tempo rinforzo reciprocamente, e in una progressione fino a costruire un'applicazione finale.

C'è un libro del genere per il model checking?

Modifica

I potrebbe aver trovato quello che sto cercando in Logica matematica per l'Informatica con Prolog fonte . Come io non ho il libro, qualcuno sa se questo libro si inserisce il requisito?

Answer 1

Il libro di John Harrison è un'eccezione ad andare tutta la strada dalla teoria alla pratica e rendendo tutto il codice sorgente disponibile. Penso che sarà difficile trovare un libro di equivalente per il model checking, ma ce ne sono alcune che consentano una buona approssimazione.

• Principi del Modello Controllo da Baier e Katoen contiene un sacco di esempi e abbastanza dettagliato descrizione algoritmica.
• La SPIN Modello Checker Gerard Holzmann è un trattamento molto diverso da parte dell'autore di uno dei primi model checker. Egli ha mantenuto lo strumento per circa 30 anni e ha un approccio "programmatico".

Una scommessa migliore potrebbe essere quella di seguire le note del corso e le assegnazioni di laboratorio di alcuni corsi disponibili on-line. Almeno si trova la teoria, la pratica ed esempi, anche se non sono organizzati in un libro.

• Edmund di Clarke in CMU ha una lista di letture che comprende tutorial per una serie di vari model checker.
• corso verifica del software rel="nofollow"> Joost-Pieter di Katoen e il follow-on Pratica Model Checking e Avanzate Model Checking coprire un sacco di terra.

Infine, questo non è del tutto quello che hai chiesto, ma dal momento che avete studiato la logica e la verifica ora modello, è invariabilmente incorrere in riferimenti a interpretazione astratta, che è alla base del programma di analisi statica ed è intimamente connessa al modello controllo (anche se questo collegamento non è sempre esplicito nella letteratura model checking).

• di Patrick Cousot MIT Corso è un tour de force che copre tutto, dal reticolo fondamenta teoriche al completa implementazione di un analizzatore statico per un linguaggio semplice. Il suo materiale didattico include tutto il codice e gli esercizi.