En busca de un libro que se deriva y construye un modelo de solicitud de cheques

Question

Estoy enseñando a mí mismo programa de verificación y actualmente estoy aprendiendo asistentes a prueba . Tengo el libro de Lógica y Razonamiento Automatizado cuales da las pruebas necesarias para la comprensión del sistema tal, pero lo más importante para mí que también da una implementación de los algoritmos necesarios como ocaml fuente .

Sé que algunas de las herramientas que figuran en Wikipedia: Comprobación de herramientas Modelo y YAHODA: Verificaciones Herramientas de base de datos son de código abierto, pero también lo prefiero cuando la teoría, pruebas, algoritmos y fuente código, se presentan al mismo tiempo de refuerzo entre sí, y en una progresión hasta llegar a una aplicación final.

¿Hay un libro de este tipo para la verificación de modelos?

editar

Me podría haber encontrado lo que estoy buscando en lógica Matemática de Informática con Prolog fuente . Como no tengo el libro, ¿alguien sabe si este libro se ajusta a la exigencia?

Answer 1

libro de John Harrison es una excepción en ir hasta el final de la teoría a la práctica y hacer todo el código fuente disponible. Creo que usted encontrará que es difícil encontrar un libro equivalente para la verificación de modelos, pero hay unos pocos que lograr una buena aproximación.

• Principios del Modelo de cheques por Baier y Katoen contiene una gran cantidad de ejemplos y muy detallado descripción algorítmica.
• El comprobador de modelos SPIN por Gerard Holzmann es un tratamiento muy diferente del autor de una de las primeras damas modelo. Se ha mantenido la herramienta durante unos treinta años y tiene un enfoque "programático".

Una mejor opción puede ser la de seguir las notas del curso y las tareas de laboratorio de algunos cursos disponibles en línea. Por lo menos se encuentra la teoría, la práctica y los ejemplos, a pesar de que no están organizados en un libro.

• Edmund Clarke en CMU tiene una lista de lectura que incluye tutoriales para algunos diversos comprobadores de modelos.
• curso de verificación de software rel="nofollow"> Joost-Pieter de Katoen y el seguimiento de modelo práctico Comprobación y Comprobación modelo avanzado cubrir mucho terreno.

Finalmente, esto no es del todo lo que pidieron, pero ya que ha estado estudiando la lógica y la comprobación ahora modelo, que invariablemente se encontrará con referencias a la interpretación abstracta, que es la base del análisis estático de software y está íntimamente relacionada con el modelo comprobar (aunque esta conexión no siempre es explícita en la literatura model checking).

• MIT Curso de Patrick Cousot es un tour de force que abarca desde bases teóricas de celosía a la implementación completa de un analizador estático para un lenguaje sencillo. Su material del curso incluye todo el código y los ejercicios.