Título: Verificación de propiedades temporales de diseños community: un caso de estudio
Autores: Aguirre, Nazareno Matías
Regis, Germán
Fecha: 2012-10-29
2005-10
2005-10
Publicador: Unversidad Nacional de La Plata
Fuente:

Tipo: Objeto de conferencia
Objeto de conferencia
Tema: Temporal logic
Design languages
Verification
Ciencias Informáticas
Descripción: En este trabajo, exploramos la utilización de una lógica temporal lineal de primer orden para la verificación de propiedades de ejecuciones de programas abstractos, escritos en un lenguaje de diseño de programas llamado CommUnity. CommUnity es un lenguaje cuya semántica y mecanismos de composición están basados en construcciones de teoría de categorías. Desarrollamos un caso de estudio, en el cual hacemos uso de una interpretación de programas CommUnity como sistemas de transición de estados, y experimentamos con el uso del demostrador de teoremas STeP para realizar verificaciones. Finalmente, discutimos algunas posibles formas de realizar las actividades de verificación de manera modular, aprovechando los distintos tipos de morfismos de programas disponibles en CommUnity.
II Workshop de Ingeniería de Software y Bases de Datos (WISBD)
Idioma: Español