Verificación de propiedades temporales de diseños community: un caso de estudio
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...
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Objeto de conferencia |
| Lenguaje: | Español |
| Publicado: |
2005
|
| Materias: | |
| Acceso en línea: | http://sedici.unlp.edu.ar/handle/10915/23148 |
| Aporte de: |
| Sumario: | 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. |
|---|