| Ambos lados, revisión anteriorRevisión previaPróxima revisión | Revisión previa |
| seminarios_de_metodos_formales:2008 [2009/02/12 18:57] – chun | seminarios_de_metodos_formales:2008 [2018/08/10 03:03] (actual) – editor externo 127.0.0.1 |
|---|
| 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 === |
| 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 === |
| * 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 === |
| * Resumen: ... | * Resumen: ... |
| |
| | ------- |
| |
| === Martes 16 de Septiembre === | === Martes 16 de Septiembre === |
| * 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 === |
| |
| 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 === |
| * 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 === |
| "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 === |
| 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 === |
| |
| 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 === |
| | |
| | * Expositora: Lic. Natalia Colussi. |
| | |
| | * Título: "Derivación Estructurada y uso de Cuantificadores" - |
| | |
| | * Resumen: |
| | La derivación estructurada se proponen como una metodología de prueba alternativa a la derivación ecuacional de Dijkstra, |
| | extendiendo a esta última con subderivaciones, las cuales permiten que las inferencias se presenten en distintos niveles de detalle, y que el desarrollo de la prueba se lleve a cabo de una manera bastante natural e intuitiva. Esto último hace que el formalismo sea conveniente para la enseñanza en los cursos introductorios de métodos formales, donde los estudiantes deben elaborar ampliamente pruebas formales que garanticen que la construcción del programa respecto de la especificación dada es correcta. |
| | |
| | Se presentará una extensión del formalismo estructurado para manejar pruebas que involucran el uso de cuantificadores, donde la notación empleada para describir una cuantificación corresponderá a la notación de lineal de Dijkstra. |
| | |
| | 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 === |
| | |
| | * Expositor: Lic. Miguel Andres. |
| | |
| | * Título: Significant Diagnostic Counterexamples on Probabilistic Model Checking. |
| | |
| | * Resumen: |
| | This paper presents a novel technique for counterexample generation in probabilistic model checking of Markov chains and Markov Decision Processes. (Finite) paths in counterexamples are grouped together in witnesses that are likely to provide similar debugging information to the user. We list five properties that witnesses should satisfy in order to be useful as debugging aid: similarity, accuracy, originality, significance, and finiteness. Our witnesses contain paths that behave similarly outside strongly connected components. |
| | |
| | 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 === |
| | |
| | * Expositor: Lic. Gustavo Petri. |
| | |
| | * Título: Relaxed Memory Models: an Operational Approach POPL'09 |
| | |
| | * Resumen: |
| | Memory models define an interface between programs written in some language and their implementation, determining which behaviour the memory (and thus a program) is allowed to have in a given model. A minimal guarantee memory models should provide to the programmer is that well-synchronized, that is, data-race free code has a standard semantics. Traditionally, memory models are defined axiomatically, setting constraints on the order in which memory operations are allowed to occur, and the programming language semantics is implicit as determining some of these constraints. In this work we propose a new approach to formalizing a memory model in which the model itself is part of a weak operational semantics for a (possibly concurrent) programming language. We formalize in this way a model that allows write operations to the store to be buffered. This enables us to derive the ordering constraints from the weak semantics of programs, and to prove, at the programming language level, that the weak semantics implements the usual interleaving semantics for data-race free programs, hence in particular that it implements the usual semantics for sequential code. |
| |
| |
