Ciencias de la Computación FAMAF

Herramientas de usuario

Herramientas del sitio

Traza:
seminarios_de_metodos_formales:2008

Diferencias

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

Enlace a la vista de comparación

Ambos lados, revisión anteriorRevisión previa
Próxima revisión		Revisión previa
seminarios_de_metodos_formales:2008 [2009/02/12 19:05] – chunseminarios_de_metodos_formales:2008 [2018/08/10 03:03] (actual) – editor externo 127.0.0.1
Línea 8: Línea 8:
 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.  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 === === Martes 19 de agosto ===
Línea 21: Línea 21:
 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). 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).
  
 +-------
  
 === Martes 26 de Agosto === === Martes 26 de Agosto ===
Línea 30: Línea 31:
   * Resumen:    * Resumen: 
 En esta charla se presentará una extensión al lenguaje NuSMV para especificación de sistemas tolerantes a fallas. Con este nuevo lenguaje queremos contribuir al diseño de una herramienta de model checking que permita verificar propiedades sobre este tipo de sistemas. En esta charla se presentará una extensión al lenguaje NuSMV para especificación de sistemas tolerantes a fallas. Con este nuevo lenguaje queremos contribuir al diseño de una herramienta de model checking que permita verificar propiedades sobre este tipo de sistemas.
 +
 +-------
  
 === Martes 9 de Septiembre === === Martes 9 de Septiembre ===
Línea 39: Línea 42:
   * Resumen: ...    * Resumen: ... 
  
 +-------
  
 === Martes 16 de Septiembre === === Martes 16 de Septiembre ===
Línea 48: Línea 52:
   * Resumen:   * Resumen:
 De acuerdo a trabajos recientes en el área de Sistemas Estocásticos Distribuidos, los schedulers distribuidos son necesarios para obtener resultados realistas durante el análisis. En este trabajo, nuestro objetivo es establecer relaciones entre diferentes clases de schedulers distribuidos. Estas relaciones permiten obtener resultados como, por ejemplo, la complejidad del problema de model-checking para una determinada clase. Mostraremos resultados de NP-hardness e indecidibilidad obtenidos a partir de las relaciones entre clases. De acuerdo a trabajos recientes en el área de Sistemas Estocásticos Distribuidos, los schedulers distribuidos son necesarios para obtener resultados realistas durante el análisis. En este trabajo, nuestro objetivo es establecer relaciones entre diferentes clases de schedulers distribuidos. Estas relaciones permiten obtener resultados como, por ejemplo, la complejidad del problema de model-checking para una determinada clase. Mostraremos resultados de NP-hardness e indecidibilidad obtenidos a partir de las relaciones entre clases.
 +
 +-------
  
 === Martes 23 de Septiembre === === Martes 23 de Septiembre ===
Línea 61: Línea 67:
  
 La definición y el estudio de estos objetos continuos hace necesario el uso de la Teoría de Conjuntos Descriptiva, cuyos resultados típicos incluyen la caracterización de distintas clases de espacios medibles, espacios de medida y determinación de la ``complejidad" de subconjuntos de espacios métricos (puntos de continuidad y convergencia, etc.) La definición y el estudio de estos objetos continuos hace necesario el uso de la Teoría de Conjuntos Descriptiva, cuyos resultados típicos incluyen la caracterización de distintas clases de espacios medibles, espacios de medida y determinación de la ``complejidad" de subconjuntos de espacios métricos (puntos de continuidad y convergencia, etc.)
 +
 +-------
  
 === Martes 14 de Octubre ===  === Martes 14 de Octubre === 
Línea 70: Línea 78:
   * Resumen:   * Resumen:
 De acuerdo a trabajos recientes en el área de Sistemas Estocásticos Distribuidos, los schedulers distribuidos son necesarios para obtener resultados realistas durante el análisis. En este trabajo, nuestro objetivo es establecer relaciones entre diferentes clases de schedulers distribuidos. Estas relaciones permiten obtener resultados como, por ejemplo, la complejidad del problema de model-checking para una determinada clase. Mostraremos resultados de NP-hardness e indecidibilidad obtenidos a partir de las relaciones entre clases. De acuerdo a trabajos recientes en el área de Sistemas Estocásticos Distribuidos, los schedulers distribuidos son necesarios para obtener resultados realistas durante el análisis. En este trabajo, nuestro objetivo es establecer relaciones entre diferentes clases de schedulers distribuidos. Estas relaciones permiten obtener resultados como, por ejemplo, la complejidad del problema de model-checking para una determinada clase. Mostraremos resultados de NP-hardness e indecidibilidad obtenidos a partir de las relaciones entre clases.
 +
 +-------
  
 === Martes 21 de Octubre === === Martes 21 de Octubre ===
Línea 79: Línea 89:
 "El uso de simulaciones computacionales en ciencia es una práctica extremadamente fructífera, no sólo por razones económicas, sino porque la rapidez y precisión para el cálculo producen resultados muy alentadores, inclusive frente a experimentos tradicionales. El estudio filosófico de estos métodos de sustitución de experimentos pretende evaluar estas prácticas a la luz del poder epistémico que de ellas surgen, esto es, discutir las bases mismas de las simulaciones computacionales intentando penetrar en la justificación de la confianza en los resultados. La propuesta es, pues, aproximarse filosóficamente a las simulaciones computacionales mediante la discusión de algunas preguntas tradicionales de corte epistemológico, ontológico y metodológico." "El uso de simulaciones computacionales en ciencia es una práctica extremadamente fructífera, no sólo por razones económicas, sino porque la rapidez y precisión para el cálculo producen resultados muy alentadores, inclusive frente a experimentos tradicionales. El estudio filosófico de estos métodos de sustitución de experimentos pretende evaluar estas prácticas a la luz del poder epistémico que de ellas surgen, esto es, discutir las bases mismas de las simulaciones computacionales intentando penetrar en la justificación de la confianza en los resultados. La propuesta es, pues, aproximarse filosóficamente a las simulaciones computacionales mediante la discusión de algunas preguntas tradicionales de corte epistemológico, ontológico y metodológico."
  
 +-------
  
 === Martes 28 de Octubre ===  === Martes 28 de Octubre === 
Línea 90: Línea 101:
 La utilidad de estos resultados es doble: permiten conocer de manera inmediata las propiedades de clausura de una clase de estructuras si tenemos axiomas con una buena sintaxis, y permiten mejorar estos últimos si son conociedas las propiedades de clausura. La utilidad de estos resultados es doble: permiten conocer de manera inmediata las propiedades de clausura de una clase de estructuras si tenemos axiomas con una buena sintaxis, y permiten mejorar estos últimos si son conociedas las propiedades de clausura.
  
 +-------
  
 === Martes 25 de Noviembre === === Martes 25 de Noviembre ===
Línea 109: Línea 120:
  
 A través de una metodología de investigación cualitativa, basada en entrevistas y observaciones de clases se intenta delinear cómo las  características de las prácticas áulicas organizan y constituyen el aprendizaje. También se analiza cómo se construyen, de manera situada dentro del aula, las nociones de demostración, abstracción y formalización, consideradas centrales para lograr una participación legítima en la comunidad.  A través de una metodología de investigación cualitativa, basada en entrevistas y observaciones de clases se intenta delinear cómo las  características de las prácticas áulicas organizan y constituyen el aprendizaje. También se analiza cómo se construyen, de manera situada dentro del aula, las nociones de demostración, abstracción y formalización, consideradas centrales para lograr una participación legítima en la comunidad. 
 +
 +-------
  
 === Martes 2 de Diciembre === === Martes 2 de Diciembre ===
Línea 123: Línea 136:
  
 También se analizarán algunos de los resultados existentes en la puesta a prueba de este formalismo en distintos niveles de enseñanza. También se analizarán algunos de los resultados existentes en la puesta a prueba de este formalismo en distintos niveles de enseñanza.
 +
 +-------
  
 === Martes 9 de Diciembre ===  === Martes 9 de Diciembre === 
Línea 134: Línea 149:
  
 Then, we show how to compute these witnesses by reducing the problem of generating counterexamples for general properties over Markov Decision Processes, in several steps, to the easy problem of generating counterexamples for reachability properties over acyclic Markov chains. Then, we show how to compute these witnesses by reducing the problem of generating counterexamples for general properties over Markov Decision Processes, in several steps, to the easy problem of generating counterexamples for reachability properties over acyclic Markov chains.
 +
 +-------
  
 === Jueves 18 de Diciembre === === Jueves 18 de Diciembre ===
seminarios_de_metodos_formales/2008.1234465550.txt.gz · Última modificación: 2018/08/10 03:03 (editor externo)