La potencia de las máquinas de estado no está en la expresividad, que no llega a ser Turing-complete, sino en la capacidad de verificación. Es lo suficientemente simple como para disponer de un amplio abanico de herramientas que pueden comprobar el funcionamiento incluso aunque para ello sea necesario analizar un número infinito de estados.

En el campo de la verificación formal hay tres tipos de herramientas:

• Los demostradores de teoremas (theorem provers). Se trata de herramientas diseñadas para construir pruebas matemáticas del comportamiento correcto de un programa. Para ello las herramientas proporcionan: 1) un lenguaje de especificación; 2) una o varias estrategias de prueba, que incluye tanto las reglas de inferencia como las estrategias de búsqueda; 3) una herramienta interactiva para construir y mantener pruebas. Herramientas de este tipo son, por ejemplo Prototype Verification System (PVS), Coq Proof Assistant, HOL, Isabelle, Agda, NuPRL, Epigram.
• Las herramientas de interpretación abstracta (abstract interpretation) también permiten demostrar que un programa (implementación) tiene una semántica que satisface una especificación mediante análisis estático del código. En esta caso la prueba se realiza a cierto nivel de abstracción que permite ignorar los detalles irrelevantes sobre la semántica y sobre la especificación. De este modo, la herramienta busca demostrar que una semántica abstracta satisface una especificación abstracta. Propiedades que en la semántica concreta son indecidibles (no es posible asegurar la falsedad o la veracidad) pasan a ser decidibles en la semántica abstracta. Es una técnica frecuentemente utilizada para el cálculo del tiempo de ejecución en el caso peor (WCET analysis). Algunas herramientas son Frama-C, aiT, RapiTime, SPARTA.
• Los verificadores de modelos (model checkers). Las herramientas de model checking permiten especificar el sistema empleando un modelo basado en grafos dirigidos (como las máquinas de estado) y en paralelo especificar las propiedades utilizando lógicas temporales. No es necesario adquirir experiencia previa para especificar sistemas o propiedades, sino que responden a una serie de patrones que pueden replicarse con facilidad. Algunas herramientas de este estilo son SMV, nuXmv, TLA+, Apalache, Z3, SPIN

Por tanto, de todas ellas, la más asequible para el contexto del Grado en Ingeniería Aeroespacial es model checking.

Matthew Dwyer desarrolló el concepto de patrón de especificación de propiedades y publicó un repositorio de patrones. La intención de este repositorio es recopilar patrones que se dan comúnmente en la especificación de sistemas concurrentes y reactivos. Las expresiones usando lógicas temporales son complicadas de aplicar correctamente, y es muy fácil equivocarse. Para facilitar su uso, los patrones de Dwyer vienen con descripciones que ilustran cómo mapear concepciones bien entendidas, pero imprecisas, del comportamiento del sistema en declaraciones precisas en lenguajes de especificación formal.

Los patrones se organizan según dos ejes diferentes: según las características de la ocurrencia y según el orden.

Para cada tipo de propiedad se reconocen cinco tipos de ámbito:

Por tanto tenemos en total 11 tipos de propiedades y para cada una de ellas 5 ámbitos diferentes, lo que corresponde a 55 patrones de propiedades, que pueden consultarse en los siguientes documentos:

• Catálogo de propiedades LTL de Matthew Dwyer. Este es el catálogo original y tiene enlaces a descripciones de cada uno de los tipos de propiedad. Incluye ejemplos y relaciones con otras propiedades. Se utiliza la notación de LTL original, utilizada por ejemplo en Promela, en la que el operador G (globally) se representa como [], el operador F (finally) se representa como <>, el operador X (next) se representa como o.
• Traducción a SMV del catálogo LTL en apéndice del manual de nuRV. Están incluidos en el mismo orden que los patrones de Matthew Dwyer, numerados de 0 a 54. Sin embargo para la descripción detallada no hay más remedio que utilizar el catálogo original.