Principios de la verificación de modelos

Principios de la verificación de modelos es un libro de texto sobre verificación de modelos , un área de la informática que automatiza el problema de determinar si una máquina cumple con los requisitos de especificación. Fue escrito por Christel Baier y Joost-Pieter Katoen , y publicado en 2008 por MIT Press .

La introducción y el primer capítulo describen el campo de la verificación de modelos : se puede analizar un modelo de una máquina o proceso para comprobar si cumple con las propiedades deseadas. Por ejemplo, una máquina expendedora podría cumplir la propiedad "el saldo nunca puede ser inferior a 0,00 €". Un videojuego podría aplicar la regla "si el jugador tiene 0 vidas, la partida termina en derrota". Tanto la máquina expendedora como el videojuego pueden modelarse como sistemas de transición . La verificación de modelos consiste en describir dichos requisitos en lenguaje matemático y automatizar las pruebas de que el modelo los cumple, o bien descubrir contraejemplos si el modelo es defectuoso.

El segundo capítulo se centra en la creación de un modelo adecuado para sistemas concurrentes , donde varias partes de un algoritmo (conjunto de instrucciones) pueden ser ejecutadas simultáneamente por diferentes máquinas o partes de una máquina.

El capítulo 3 explora los tipos de reglas que puede satisfacer un sistema de transición: propiedades de tiempo lineal . Una propiedad de seguridad , como "no son posibles estados de interbloqueo ", tiene la forma "un resultado indeseable nunca puede ocurrir". Una propiedad de vivacidad , como "un recurso compartido siempre estará disponible eventualmente para un componente que lo solicite", tiene la forma "un resultado deseable ocurrirá eventualmente". Las propiedades de equidad, como "un semáforo nunca deja de cambiar de color", pueden usarse como precondiciones , es decir, supuestos a partir de los cuales se pueden deducir otras propiedades.

El cuarto capítulo trata sobre las propiedades de los lenguajes regulares y ω-regulares , así como sobre máquinas teóricas como los autómatas de Büchi que modelan dichos lenguajes. Presenta algoritmos de verificación de modelos para comprobar propiedades o encontrar contraejemplos.

Los capítulos quinto y sexto exploran la lógica temporal lineal (LTL) y la lógica de árbol de computación (CTL), dos clases de fórmulas que expresan propiedades. La LTL codifica requisitos sobre rutas a través de un sistema, como «todo jugador de Monopoly pasa por la casilla de Salida infinitas veces»; la CTL codifica requisitos sobre estados en un sistema, como «desde cualquier posición, todos los jugadores pueden llegar a la casilla de Salida». También se definen fórmulas CTL* , que combinan ambas gramáticas. Se proporcionan algoritmos para la verificación de modelos de fórmulas en estas lógicas.

El séptimo capítulo explora métodos formales para comparar sistemas de transición, como la bisimulación ; el octavo trata sobre reducciones de orden parcial que buscan disminuir el cálculo necesario para verificar las propiedades de un modelo. Los capítulos noveno y décimo tratan sobre extensiones de las lógicas y autómatas considerados previamente, incluyendo la adición de una velocidad de reloj ( autómatas temporizados ) o probabilidades ( autómatas probabilísticos , basados ​​en cadenas de Markov ).

François Laroussinie, en un artículo para The Computer Journal , recomendó el libro a investigadores, profesores, estudiantes e ingenieros, calificándolo de «impresionante». Laroussinie consideró que el libro de texto era completo y de fácil lectura, con numerosos ejemplos, ejercicios e ideas motivadoras para los conceptos clave. Con un «marco unificado», los primeros siete capítulos abarcan la teoría clásica y los tres últimos, las extensiones de la verificación de modelos. ^{[ 1 ]}

En ACM Computing Reviews , Gabriel Ciobanu opinó que el libro de texto podría utilizarse en cursos avanzados de pregrado o posgrado, y que sería útil para los investigadores. Ciobanu elogió la presentación "clara e intuitiva" y afirmó que "debería valorarse por su enfoque pedagógico para abarcar conceptos básicos, resultados teóricos profundos y temas avanzados en la investigación de verificación de modelos". ^{[ 2 ]}

En 2014, el libro fue uno de los cinco textos académicos más citados monitoreados por el Book Citation Index (BKCI). ^{[ 3 ]}

• Lange, Martin (2010), MathSciNet , MR 2493187 {{citation}}: CS1 maint: publicación periódica sin título ( enlace )

• Sitio web oficial