Departamento de Ciencias de la Computación

La verificación de modelos permite verificar si el modelo de un sistema tiene o no cierta propiedad. Cuando no la tiene, normalmente el modelo se modifica manualmente. Nosotros investigamos métodos para que dicha modificación ("actualización") se realice mecánicamente. Actualmente tenemos un método de actualización adecuado para modelos pequeños, y pensamos que es importante extender nuestra técnica a sistemas grandes con métodos "simbólicos". También es posible que nuestro método tenga aplicaciones en la Verificación "Incremental".

Actualmente el mayor uso de la verificación de modelos es en el diseño de circuitos digitales. El parecido entre dichos circuitos y las Redes Genéticas nos ha permitido emplear un verificador de modelos como herramienta auxiliar en la construcción de redes genéticas booleanas. Tenemos ya una primera versión de un sistema llamado "Antelope", que planeamos extender para convertirlo en un sistema más práctico.

Usualmente los modelos que se verifican con estas técnicas son finitios, lo que significa un problema para su aplicación a software ordinario (que típicamente representaría modelos infinitos). Nosotros hemos evitado esta dificultad concentrándonos en software para controlar sistemas inmersos, especificados con conjuntos de máquinas finitas. Como resultado, hemos podido emplear las técnicas existentes de Verificación de Modelos a la verificación de programas. Sin embargo, a la fecha solo hemos verificado sistemas pequeños. Pretendemos hacerlo con sistemas más grandes. Este es trabajo conjunto con Vladimir Estivill-Castro.