Diferencias

Muestra las diferencias entre dos versiones de la página.

--- seminarios_de_metodos_formales:ano_2008 [2008/12/23 21:25] – actualizado nueces
+++ seminarios_de_metodos_formales:ano_2008 [2008/12/23 21:44] (actual) – borrado nueces
@@ Línea 1: / Línea 1: @@
-=== Martes 12 de agosto ===
-  * Expositor: Matias Lee
-  * Título: Secure Interface Automata.
-  * Resumen:
-Una interface describe cómo un sistema interactua con su entorno. Por esta razón, ellas juegan un papel muy importante en el desarrollo basado en componentes. Dadas las interfaces de 2 componentes sería muy util poder analizar si ellas son compatibles, es decir, si trabajan bien en forma conjunta. En esta charla presentamos un nuevo tipo de interface: Secure Interface Automata. Las mismas nos permiten hablar de “No Interferencia”, una propiedad de seguridad bastante estudiada. Analizamos como se comporta esta propiedad con respecto a la composición. Finalmente, definimos un algoritmo para restringir el comportamiento de una interfaz para obtener la propiedad deseada.
-=== Martes 19 de agosto ===
-  * Expositor: Nazareno Aguirre
-  * Título: Descripcion y Analisis de Especificaciones Tabulares de Requisitos usando DynAlloy (trabajo realizado en conjunto con Marcelo Frias, Mariano Moscato, Tom Maibaum y Alan Wassyng)
-  * Resumen:
-En esta charla presentare un lenguaje para la especificacion formal de requisitos llamado SCR (Software Cost Reduction), desarrollado por el Instituto de Investigacion Naval de EEUU. El lenguaje esta fuertemente basado en una notacion tabular, que permite organizar formulas (que describen la relacion que el sistema debe mantener con el ambiente) de manera concisa y clara. El lenguaje posee ademas maduras herramientas de analisis basadas en model checking y demostracion semi-automatica de teoremas.
-Discutire ademas algunas limitaciones de SCR, en particular en lo concerniente a la combinacion de tablas. Mostrare como este problema puede atacarse utilizando DynAlloy, una extension al lenguaje de especificaciones Alloy que incorpora acciones (y programas). DynAlloy posee una herramienta de analisis, que indirectamente utiliza SAT solvers mediante la traduccion de especificaciones DynAlloy a Alloy, y el uso del Alloy Analyzer (la herramienta asociada al lenguaje Alloy).