Verificación formal y refinamientos en P/PML

Abstract

En el contexto de las aplicaciones industriales, existen distintos métodos formales propuestos que permiten el modelado de los elementos de este tipo de sistemas. La lógica P/PML (Product/Process Modeling Logic) es un método formal desarrollado para la especificación y construcción de sistemas industriales de tiempo real. Esta lógica es una extensión de la lógica dinámica de primer orden agregando (a) acciones atómicas arbitrarias en lugar de solo asignación, (b) variables sobre procesos que permiten especificar sistemas parcialmente, (c) un operador de paralelismo y (d) restricciones de tiempo sobre los procesos. En este trabajo se estudian los aspectos de verificación y derivación formal de procesos en la lógica P/PML. En la primer parte se define el formalismo P/PML, su sintaxis y semántica, y se dan algunos ejemplos de procesos en esta lógica. En la segunda parte de este trabajo se explora el concepto de verificación formal de procesos en P/PML, tratándose el aspecto de corrección parcial. Como resultado, se desarrolla un sistema formal de prueba que permite verificar la corrección parcial de procesos con respecto a especificaciones lógicas. En la tercer parte de este trabajo se explora el segundo concepto mencionado antes, el de derivación formal de procesos en la lógica P/PML, desarrollándose como resultado un calculo de refinamientos que permite derivar procesos a partir de especificaciones lógicas. Por ultimo, se presentan las conclusiones acerca de este trabajo y se citan algunas posibles extensiones a desarrollar en el futuro.