No es ningún secreto que tanto los sistemas software como hardware generalmente presentan
errores. Los métodos de testeo y simulación pueden identificar muchos problemas importantes,
pero para sistemas que tienen requerimientos de seguridad o que son económicamente críticos, es
indispensable llevar a cabo una verificación exhaustiva. Tal análisis se puede realizar utilizando
métodos de verificación formal.
Un enfoque de la verificación formal es la verificación de modelos, que es un proceso totalmente
automático basado en la construcción de modelos abstractos para representar sistemas. Poste-
riormente, sobre estos modelos se comprueban propiedades deseadas del sistema, normalmente
expresadas en alguna lógica temporal, como por ejemplo lógica linear temporal. Las propiedades
expresadas con fórmulas de lógica linear temporal pueden describir el orden de los eventos en el
tiempo sin describir el tiempo explícitamente. Por eso mismo, son útiles a la hora de verificar las
posibles ejecuciones de un sistema.
Este proyecto pretende implementar algoritmos de verificación de modelos que determinen si una
fórmula de lógica linear temporal que exprese una propiedad de un cierto sistema es satisfecha por
éste.
It is no secret that computer software programs, computer hardware designs, and computer sys-
tems in general exhibit errors. Testing and simulation methods can identify many significant
problems, but for systems that have safety or economically critical requirements, exhaustive ver-
ification is indispensable. Such exhaustive analysis can be performed with the use of formal
verification methods.
One approach to formal verification is model checking, which is a fully automated process based
on the construction of abstract models to represent systems. These models are then checked
against desired properties defining a specification, usually expressed in some temporal logic, such
as linear temporal logic (LTL). Temporal properties can describe the ordering of events in time
without introducing time explicitly, thereby being useful when verifying the possible executions
of a system.
This project aims to implement model checking algorithms that determine whether an LTL formula
expressing a desired property is satisfied in a computing system.
