Construcción de un verificador de modelos.

Abstract

Este proyecto consiste en la construcción de un verificador de modelos que implemente los principales algoritmos de verificación. Para esto se escogieron dos lenguajes de propiedades que requieren distintos algoritmos de verificación. LTL requiere un algoritmo basado en autómatas que reconocen las ejecuciones de un sistema, tratando las mismas como palabras. Mientras que CTL requiere un algoritmo basado en el análisis de la satisfacibilidad de las fórmulas por los estados del sistema de transiciones. Este verificador debe ser fácil de utilizar y de mantener, además de flexible de forma que sea posible agregar nuevos lenguajes para describir propiedades. Para lograr esto se realizó un diseño orientado a objetos y con módulos bien definidos apuntando a su mantenimiento y extensión. También pensando en estos objetivos se escogió el lenguaje de programación Python 2.7 debido a que cumple con los requisitos del diseño. Además es un lenguaje que mezcla programación funcional con programación imperativa, lo que permite implementar algoritmos complejos en pocas instrucciones generando un código fácil de comprender por otras personas. Por otro lado se utilizó el formato de archivo GraphML para representar los sistemas de transiciones. Este formato es muy útil para representar grafos ya que existen varios editores para el mismo y al ser un lenguaje basado en XML existen muchas herramientas para su manipulación. Además se utilizó la herramienta Python Lex-Yacc para parsear las fórmulas. Esta herramienta requirió la definición de las gramáticas correspondientes para cada lenguaje. De esta forma se desarrolló un verificador fácil de utilizar, fácil de mantener, modularizado y flexible.