Biblioteca Digital | FCEN-UBA

Biblioteca Digital ¿Por qué?
Objetivos
Impactos
Estadísticas
Documentos
Presentaciones
Notas
Autores y derechos
¿Por qué depositar?
¿Cómo depositar?
Autorización
Depositar y publicar
Editoriales
Publicar mi tesis Formulario Tesis Posgrado
Formulario Tesis Grado
Normativa
Res. CD 2053/05
Res. CD 2533/09
Res. CD 0272/13
Res. CD 2793/15

Colecciones Tesis Doctorales
Fotografías
Publicaciones
Archivo
Libros
Reportes Técnicos

Tesis > TEMA

Computación [ 80 tesis ]

Ingeniería del Software [ 13 tesis ]

Marré, Martina. "Análisis del flujo de programas para reducir y estimar el costo de los criterios de cubrimiento de Testing" (1997) Facultad de Ciencias Exactas y Naturales. Universidad de Buenos Aires

pdf

Resumen Registro Cita

Resumen:
El testing de un sistema de software consiste en ejecutarlo sobre un conjunto de datos de input conveniente y chequear que el output producido es el esperado. El testing es ampliamente usado para mejorar la calidad del software, y específicamente, para descubrir errores inevitablemente introducidos durante el proceso de desarrollo del software. Uno de los problemas más difíciles en testing es saber cuándo detener el proceso de prueba. Por un lado, no es posible en general dar una respuesta a si un test suite garantiza la ausencia de defectos. Por otro lado, necesitamos una manera de limitar el costo del testing. Por consiguiente, es útil tener criterios para determinar cuándo se ha testeado "suficientemente" un programa. Idealmente, el proceso de testing se debe planear de antemano. Sin embargo, en la práctica se incorporan los tests de a uno, hasta se satisface algún criterio de terminación o criterio de adecuación. En particular, se pueden usar diferentes cubrimientos para determinar cuándo se ha probado un programa lo suficiente. La idea es garantizar que cada instrucción, decisión, u otra parte de un programa se ha ejecutado por lo menos una vez bajo la prueba realizada. Un problema mayor es que el testing emplea una cantidad considerable del tiempo y recursos gastados en la producción de software (9). Por consiguiente, sería útil: 1. Reducir el costo del testing, y 2. Estimar el costo del testing. En particular, el número de tests a ser ejecutados impacta fuertemente en el costo del testing. De hecho, el tiempo y los recursos necesarios para realizar el testing aumenta con el número de casos de prueba. Entonces, para reducir el costo del testing, el número de casos de prueba generados para satisfacer un criterio de selección de casos debe ser lo más pequeño posible. Además, una cota en el número de tests que tienen que ser ejecutados para satisfacer una estrategia de selección de casos de test puede ser usada por gerentes y testers para estimar el esfuerzo necesario para llevar a cabo la ejecución de los tests. En práctica, un criterio de testing define una colección de requisitos que deben cumplirse. En el caso de criterios de cubrimiento estructurales, estos requisitos se mapean en un conjunto de entidades del flowgraph (o grafo del flujo de control) del programa, que se deben cubrir cuando se ejecutan los datos de test. En este trabajo presentamos un método para reducir y estimar el número de tests necesarios para satisfacer criterios de cubrimiento estructurales, basado en el concepto nuevo de spanning sets of entities o conjunto expandido de entidades. Este concepto se basa en la observación de que un test generalmente cubre más de una entidad. Sin embargo, este hecho tradicionalmente no se considera cuando se mide el cubrimiento de los tests y se identifica las entidades no cubiertas, o cuando se seleccionan más tests para aumentar el cubrimiento. Los métodos existentes para seleccionar tests generan un dato para cubrir una entidad seleccionada en forma arbitraria, y considerada en forma aislada a las otras entidades. Si el dato de test generado también ejecuta otras entidades, se considerarán cubiertas a posteriori. Pero no se realiza ningún esfuerzo para generar a priori datos de test que satisfagan varios requisitos simultáneamente. Nuestro método supera estos inconvenientes, ya que identifica mediante análisis estático un subconjunto de entidades mínimo con la propiedad de que cualquier conjunto de tests que cubre este subconjunto cubre toda entidad en el programa. Llamamos a este subconjunto mínimo un "spanning set of entities". En este trabajo, primero definimos los conjuntos de entidades que se asocian con cada criterio en una familia entera de criterios de cubrimiento de test, muy populares. Luego presentamos un método generalizado para identificar un spanning set of entities para los criterios considerados. Nuestro método puede ser automatizado. Una vez que ha sido incluido en el proceso de testing, la información puede ser usada para: Evaluar la adecuación del testing más efectivamente. Reducir el costo del testing. Estimar el costo del testing. Generar test suites. En esta tesis presentamos nuestro estudio del uso de spanning sets of entities en testing.

Abstract:
Testing a software system consists of executing it over a suitable sample of input data and then checking if the output produced matchs what was expected. Testing is widely used to enhance software quality, and, specifically, to uncover bugs that are inevitably introduced during the software development process. One of the most difficult problems in testing is knowing when to stop the testing process. On the one hand, it is not possible in general to give an answer to whether a test suite guarantees the absence of faults. On the other hand, we need a way to limit the cost of testing. Therefore, it is useful to have criteria to determine when a program has been tested "enough". Ideally, the testing process should be planned in advance. However, in practice the tests are incorporated little by little, until some adequacy criterion is satisfied. In particular, different coverages can be used to determine when the program has been tested enough. The idea is to guarantee that each statement, decision or other feature of the program has been executed at least once under some test. A major problem is that testing takes a considerable amount of the time and resources spent on producing software . Therefore, it would be useful to have ways 1. to reduce the cost of testing, and 2. to estimate this cost. In particular, the number of tests to be ezecuted impacts heavily on the cost of testing. In fact, the time and resources needed for testing increase as the number of test cases increases. Hence, to reduce the cost of testing, the number of test cases generated to satisfy a selected test criterion should be as small as possible. Moreover, a bound on the number of tests that have to be performed to satisfy a selected test strategy can be used by managers and testers to estimate the effort needed to carry out the tests. A test criterion in practice sets a collection of requirements to be fulfilled. For structural coverage criteria, these requirements are mapped onto a set of entities in the program flowgraph that must be covered when the tests are executed. In this work we present a method for reducing and estimating the number of tests needed to satisfy structural coverage criteria, based on the new concept of spanning sets of entities. This concept is based on the observation that one test generally covers more than one entity. However, this fact is not traditionally considered when coverage is measured and not covered entities are identified, or when more tests have to be selected in order to aug~nent coverage. Methods for selecting tests generate a test datum for covering one entity selected arbitrarily and considered in isolation from the other entities. If the generated test datum also exercises other entities, these will then be considered as covered a-posteriori. But no effort is made to generate a-priori test data that satisfy multiple requirements. Our method overcomes these drawbacks by identifying with static analysis a minimum subset of entities with the property that any set of tests covering this subset covers every entity in the program. We call this minimum subset a "spanning set of entities". In this work, we fist define the sets of entities that are associated with a whole family of popular test coverage criteria. Then we present a generalized method of identifying a spanning set of entities for the criteria considered. Our method can be automated. Once it has been included in the software testing process, this information can be used for evaluating test adequacy more effectively; reducing the cost of testing; estimating the cost of testing; generating test suites. In this thesis we present our study of the use of spanning sets of entities in coverage testing.

Braberman, Víctor Adrián. "Modelando y verificando diseños de sistemas de tiempo real" (2000) Facultad de Ciencias Exactas y Naturales. Universidad de Buenos Aires

pdf

Registro Cita

Abstract:
Real-time systems are found in an increasing variety of application fields. Usually, they are embedded systems controlling devices that may risk lives or damage properties: they are safety critical systems. Hard Real-Time requirements (late means wrong) make the development of such kind of systems a formidable and daunting task. The need to predict temporal behavior of critical real-time systems has encouraged the development of an useful collection of models, results and tools for analyzing schedulability of applications (e.g., ). However, there is no general analytical support for verifying other kind of high level timing requirements on complex software architectures. On the other hand, the verification of specifications and designs of real-time systems has been considered an interesting application field for automatic analysis techniques such as model-checking. Unfortunately, there is a natural trade-off between sophistication of supported features and the practicality of formal analysis. To cope with the challenges of formal analysis real-time system designs we focus on three aspects that, we believe, are fundamental to get practical tools: model-generation, modelreduction and model-checking. Then, firstly, we extend our ideas presented in and develop an automatic approach to model and verify designs of real-time systems for complex timing requirements based on scheduling theory and timed automata theory (a wellknown and studied formalism to model and verify timed systems). That is, to enhance practicality of formal analysis, we focus our analysis on designs adhering to Fixed-Priority scheduling. In essence, we exploit known scheduling theory to automatically derive simple and compositional formal models. To the best of our knowledge, this is the first proposal to integrate scheduling theory into the framework of automatic formal verification. To model such systems, we present I/O Timed Components, a notion and discipline to build non-blocking live timed systems. I/O Timed Components, which are build on top of Timed Automata, provide other important methodological advantages like influence detection or compositional reasoning. Secondly, we provide a battery of automatic and rather generic abstraction techniques that, given a requirement to be analyzed, reduces the model while preserving the relevant behaviors to check it. Thus, we do not feed the verification tools with the whole model as previous formal approaches. To provide arguments about the correctness of those abstractions, we present a notion of Continuous Observational Bismulation that is weaker than strong timed bisimulation yet preserving many well-known logics for timed systems like TCTL . Finally, since we choose timed automata as formal kernel, we adapt and apply their deeply studied and developed analysis theory, as well as their practical tools. Moreover, we also describe from scratch an algorithm to model-check duration properties, a feature that is not addressed by available tools. That algorithm extends the one presented in .

López Pombo, Carlos Gustavo. "Fork algebras como herramienta de razonamiento entre especificaciones heterogéneas" (2007) Facultad de Ciencias Exactas y Naturales. Universidad de Buenos Aires

pdf

Resumen Registro Cita

Resumen:
Las lógicas han sido usadas como sistemas formales para especificar sistemas de software. Más aun, las especificaciones lógicas, por ser formales, contribuyen en la aplicación de métodos técnicas correctas de verificación. Diversos formalismos han sido desarrollados para lidiar con estos aspectos y muchos de ellos son eficientes en describir ciertas características de los sistemas de software. Por ejemplo, la lógica temporal, proposicional y de primer order, consigue describir la forma en la que los sistemas de software evolucionan en el tiempo. La lógica dinámica también permite la especificación de sistemas pero lo hace describiendo cómo los programas transforman el estado del sistema. Estos son sólo algunos ejemplos de cómo una lógica particular permite la especificación de determinados comportamientos de un sistema. La pregunta interesante acerca de este hecho es: Existe un lenguaje ideal para especificar el comportamiento de un sistema? A pesar de que no vamos a concentrarnos en responder esta pregunta, creemos que ese lenguaje debe tener una sintaxis clara y una semántica fácil de entender, con el propósito de facilitar la comprensión de especificaciones y la aplicación de métodos formales. Entre las propuestas que recopilamos, las instituciones se imponen como un formalismo para razonar entre lógicas, y una institución universal, que permita razonar entre las lógicas interesantes sería la respuesta a nuestra pregunta. En esta tesis mostraremos que una definición adecuada de la institución de las fork algebras es útil para razonar entre diversas lógicas proposicionales y de primer orden que aparecen frecuentemente en la especificación de software.

Abstract:
Logics have often been used as formal systems suitable for the specification of software artifacts. Moreover, logical specifications, being formal, might contribute towards the application of sound verification techniques. Several formalisms have been developed to cope with these aspects and most of them are effective in describing some particular characteristics of software systems. For example, propositional and first-order temporal logics succeed in describing the way software systems evolve along time. Dynamic logic also allows system specification but it does so by describing how programs transform the system state. These are only some examples of how a particular logic allows to specify a certain system behavior. The interesting question about this fact is: Is there an ideal language to specify the behavior of a system? Although we will not concentrate on answering this question, we believe such language must have a clear syntax and an easy to understand semantics with the purpose of facilitating the comprehension of specifications and the application of formal methods. Among the proposals we surveyed, institutions prevail as a formalism to reason across logics, and a sort of universal institution, allowing us to reason across all interesting logics would be the answer to our question. We will show in this thesis that an adequately defined institution of fork algebras is useful for reasoning across many propositional and first-order logics ubiquitous in software specification.

Garbervetsky, Diego. "Síntesis de especificaciones paramétricas de utilización de la memoria dinámica" (2007) Facultad de Ciencias Exactas y Naturales. Universidad de Buenos Aires

pdf

Resumen Registro Cita

Resumen:
En los últimos años se ha visto un gran interés en las comunidades de sistemas de tiempo real y embebidos en el uso de de lenguajes orientados a objetos tipo Java. Los motivos de este interés se deben en parte a que este tipo de tecnologías facilitan la encapsulación de abstracciones y la comunicación mediante interfaces bien de_nidas. Otro aspecto importante es la gran comunidad de desarrolladores y la cantidad de bibliotecas y herramientas de desarrollo disponible. Sin embargo, para poder adoptar lenguajes de este tipo en ambientes embebidos y de tiempo real hay que solucionar al menos dos grandes problemas: la impredictibilidad temporal dada por las interrupciones relacionadas con la colección de objetos (garbage collector) y poder analizar requerimientos de memoria de las aplicaciones. Ha habido un número importante de trabajos donde se intenta atacar el problema de impredictibilidad temporal de los administradores de memoria automáticos desde distintos enfoques tales como garbage collectors con ciertas garantías temporales o directamente utilizando modelos alternativos de administración de memoria. Sin embargo, no ha habido muchos avances con respecto al estudio cuantitativo de requisitos de memoria. En esta tesis abordamos el problema de predecir automáticamente certi_cados de utilización y requisitos de memoria. Para ellos presentamos primero una técnica que permite obtener expresiones paramétricas de las solicitudes de memoria dinámica sin considerar ningún mecanismo de colección de objetos. Luego proponemos un esquema alternativo de administración de memoria junto con una técnica que permite la transformación de código Java convencional en otro con la misma funcionalidad pero adaptado para la nueva política de manejo de la memoria. Bajo este nuevo esquema, proponemos una técnica que permite determinar de manera paramétrica la cantidad de memoria necesaria para correr el programa o parte de él. Todas estas técnicas fueron implementadas en un prototipo que nos permitió analizar automaticamente un conjunto interesante de aplicaciones siendo los resultados iniciales bastante promisorios.

Abstract:
Current trends in the embedded and real-time software industry are leading towards the use of object-oriented programming languages such as Java. From the software engineering perspective, one of the most attractive issues in objectoriented design is the encapsulation of abstractions into objects that communicate through clearly de_ned interfaces. However, in order to be able to successfully adopt languages with object oriented features like Java in embedded and real-time systems, is necessary to solve at least two problems: eliminate execution unpredictability due to garbage collection and automatically analyze memory requirements. There has been some work trying to deal with the _rst problem but the problem of computing memory requirements is still challenging. In this thesis we present our approach to tackle both problems by presenting solutions towards more predictable memory management and predicting memory requirements. The e_ort is mainly focused in the latter problem as we found it hard, less explored, strongly relevant for all kinds of embedded systems and its applicability and usefulness is beyond real-time applications. This thesis presents a series of techniques to automatically compute dynamic memory utilization certi_cates. We start by computing a technique that produces parametric speci_cations of memory allocations without consider any memory reclaiming mechanism. Then, we approximate object lifetime using escape analysis and synthesize a scoped-based memory organization where objects are organized in regions that can be collected as a whole. We propose a technique to automatically translate conventional Java code into code that safely adopts this memory management mechanism. Under this new setting we infer parametric speci_cations of the size of each memory regions. Finally, we predict the minimum amount of dynamic memory required to run a method (or program) in the context of scoped memory management by computing parametric speci_cations of the size of memory regions and by modeling the potential con_gurations of the regions in run time. We develop a prototype tool that implemented the complete chain of techniques and allow us to experimentally evaluate the e_ciency and accuracy of the method on several Java benchmarks. The results are very encouraging.

Schapachnik, Fernando. "Verificación de autómatas temporizados en arquitecturas monoprocesador y multiprocesador" (2007) Facultad de Ciencias Exactas y Naturales. Universidad de Buenos Aires

pdf

Resumen Registro Cita

Resumen:
Los sistemas de tiempo real están presentes en dispositivos embebidos, teléfonos celulares, controladores de vuelo, etc. Su complejidad es cada vez mayor, y cada vez cumplen funciones más críticas, donde las consecuencias de sus fallas son cada vez más graves. Por estos motivos tiene sentido realizar un análisis riguroso sobre ellos, que permita asegurar que sus diseños cumplen ciertas propiedades deseables. A este tipo de análisis se le suele llamar verificación automática o model checking. Un formalismo muy difundido para realizar esta tarea es el de los autómatas temporizados, una extensión de la teoría clásica de autómatas que permite trabajar con tiempo denso. Si bien las técnicas basadas en este tipo de autómatas se conocen desde hace un par de décadas, sufren aún de problemas de escalabilidad, lo que dificulta una utilización mayor en casos reales. Esta tesis analiza diversos mecanismos para acelerar la verificación de autómatas temporizados, tanto en el (clásico) ambiente monoprocesador, como así también en arquitecturas distribuidas. Durante el transcurso de la misma se construyó el model checker Zeus, que se utiliza para la experimentación. Luego de presentar la motivación e introducción al tema, se presentan los conceptos básicos del formalismo y las estructuras de datos más utilizadas en este tipo de herramientas. Se destacan los dos algoritmos tradicionales de verificación, forward y backwards. A continuación, se explora la paralelización del algoritmo backwards: se presenta una prueba de corrección de una versión distribuida y asincrónica del mismo, se la implementa, y se experimenta también con una versión sincrónica y con otra que reparte la carga de trabajo sobre los procesadores de manera dinámica. Se analizan los resultados obtenidos y se argumenta que son cercanos a óptimos utilizando la unidad de distribución de trabajo actual: la asignación de nodos del autómata a procesadores. Luego se aborda la paralización del algoritmo forward junto con una estrategia para la redistribución dinámica de trabajo entre los procesadores. Después de demostrar su corrección, se analizan varios casos de estudio sobre distintas configuraciones, obteniéndose resultados positivos pero no óptimos, y comprobándose que aún queda mucho por investigar con respecto a la distribución de este algoritmo, y planteándose varias posibles líneas de investigación. En el capítulo siguiente se compara el presente trabajo con otros del área, y se argumenta que ciertos resultados positivos obtenidos por otros investigadores tienen como causa no la paralización en sí sino ciertos efectos colaterales de la misma, que tal vez podrían reproducirse en un monoprocesador. A continuación se presenta trabajo realizado en pos de obtener una nueva estructura de datos. En ese marco, se introducen los rCDDs (restricted Clock Difference Diagrams) junto con casos de estudio en los que estos mejoran los tiempos de ejecución hasta en un treinta por ciento. El siguiente capitulo explora dos optimizaciones también validas para el caso monoprocesador. La primera consiste en computar rangos posibles para los valores de las estructuras de datos y de esa manera reacomodarlas para detectar antes ciertas condiciones de corte de operaciones utilizadas con mucha frecuencia. Los resultados muestran mejoras de hasta un diecisiete por ciento en los tiempos de ejecución. La segunda consiste en computar una aproximación al hipervolumen de los poliedros representados por las estructuras de datos, de manera tal de evitar O(n2) comparaciones al costo de O(1). Esta técnica logra una reducción de tiempo de hasta casi un veinte por ciento. El anteúltimo capítulo presenta VInTiMe, una herramienta gráfica que permite describir diseños de tiempo real, especificar sus propiedades de manera amigable, y verificarlas utilizando el model checker distribuido Zeus, de manera sencilla. Constituye un esfuerzo por acercar los métodos formales al usuario no tan experimentado. Finalmente, se exponen las conclusiones del trabajo, donde se argumenta la dificultad de decidir de antemano qué optimizaciones y/o parámetros serán más convenientes para un caso de estudio dado, y se proponen ideas alternativas para atacar el problema.

Abstract:
Real-time systems are present today in embedded devices, cellphones, flight controllers, etc. Their complexity is ever increasing, as well as the criticality of their functions. Consequences of failure are each day more dangerous. This is why performing a rigorous analysis over them makes sense, allowing to assert that their design complies with some desirable properties. This type of analysis is usually called automated verification or model checking. A well-known formalism for model checking is timed automata, an extension of the classical automata theory allowing to model dense time. Although timed automata-based techniques are known since a couple of decades ago, they still suffer from scalability issues, jeopardizing a broader adoption in real cases. This thesis analyzes diverse mechanisms to speedup timed automata verification, both in the (classical) monoprocessor environment, as well as in distributed architectures. While working on it, the model checker Zeus was built as a base for experimentation. After motivating and introducing the subject matter, foundational concepts of the formalism are presented, as well as the data structures more used by the tools. Special attention is payed to the two traditional verification algorithms, forward and backwards. Next, the parallelization of the backwards algorithm is explored: a correctness proof of a distributed and asynchronous version is presented. It is implemented, and experimentation is also done with a synchronous version and another one that dynamically balances workload among processors. Obtained results are analyzed and it is argued that they are close to optimal, as long as the same unit of distribution is used: assigning each automata node to only one processor. After that, a distributed version of the forward algorithm is analyzed, along with a dynamic workload migration strategy. Its correctness is proved, and various case studies over different configuration settings are tried. Positive results are achieved, yet not optimal, corroborating that there is still much research to perform regarding this algorithm. Also, various possible future continuation lines are presented. Next chapter compares against other work in the literature, and argues than certain positive results achieved by other researchers might be caused not by the distribution per se, but actually as a byproduct of it, and that the same effects might be reproducible in a monoprocessor setting. Work towards a new data structure is next, introducing rCDDs (short for restricted Clock Difference Diagrams). Along with their details and algorithms, case studies showing up to a thirty percent of improvement in running times are presented. After that, two optimizations also valid for the monoprocessor setting are introduced. The first one computes ranges of possible values for the data structures, trying to accommodate them in such a way that certain finishing conditions for the most used operation are met earlier. Results show improvements of up to a seventeen percent in running times. The second one is about computing an approximation to the hypervolume of the polyhedra represented by the data structures, thus avoiding O(n2) comparisons at the price of O(1). This technique allows to reduce running times by up to almost twenty percent. The penultimate chapter presents VInTiMe, a graphical tool that allows to describe real-time system designs, specify their properties in a friendly way, and verify them using the distributed model checker Zeus, in a simple manner. This is an efford to put formal methods closer to the practitioner. Lastly, conclusions are presented, arguing the difficulty of deciding beforehand which optimizations and parameters would be better for a particular case study, and proposing alternative ideas to palliate such an issue.

Galeotti, Juan Pablo. "Verificación de software usando Alloy" (2010) Facultad de Ciencias Exactas y Naturales. Universidad de Buenos Aires

pdf

Resumen Registro Cita

Resumen:
La verificación acotada de software usando SAT consiste en la traducción del programa junto con las anotaciones provistas por el usuario a una fórmula proposicional. Luego de lo cual la fórmula es analizada en busca de violaciones a la especificación usando un SAT-solver. Si una violación es encontrada, una traza de ejecución exponiendo el error es exhibida al usuario. Alloy es un lenguaje formal relacional que nos permite automáticamente analizar especificiaciones buscando contraejemplos de aserciones con la ayuda de un SAT-solver off-the-shelf. Las contribuciones de la presente tesis son principalmente dos. Por un lado, se presenta una traducción desde software anotado en lenguaje JML al lenguaje Alloy. Para conseguir esto, se presenta: • DynAlloy, una extensión al lenguaje de especificación Alloy para describir propiedades dinámicas de los sistemas usando acciones. Extendemos la sintaxis de Alloy con una notación para escribir aserciones de correctitud parcial. La semántica de estas aserciones es una adaptación del precondición liberal más débil de Dijsktra. • DynJML, un lenguaje de especificación orientado a objetos que sirve de representación intermedia para facilitar la traducción de JML a DynAlloy. • TACO, un prototipo que implementa la traducción de JML a DynAlloy. En segundo lugar, introducimos una técnica novedosa, general y complementamente automatizable para analizar programas Java secuenciales anotados con JML usando SAT. Esta técnica es especialmente beneficiosa cuando el programa opera con estructuras de datos complejas. Para esto, se instrumenta el modelo Alloy con un predicado de ruptura de simetrías que nos permite el cómputo paralelo y automatizado de cotas ajustadas para los campos Java.

Abstract:
SAT-based bounded verification of annotated code consists of translating the code together with the annotations to a propositional formula, and an- alyzing the formula for specification violations using a SAT-solver. If a violation is found, an execution trace exposing the error is exhibited. Alloy is a formal specification language that allows us to automatically ana- lyze specifications by searching for counterexamples of assertions with the help of the off-the-shelf SAT solvers. The contributions of this dissertation are twofold. Firstly, we present a trans- lation from Java Modelling Language (a behavioural specification language for Java) to Alloy. In order to do so, we introduce: • DynAlloy, an extension to the Alloy specification language to describe dynamic properties of systems using actions. We extend Alloy’s syntax with a notation for partial correctness assertions, whose semantics relies on an adaptation of Dijkstra’s weakest liberal precondition. • DynJML, an intermediate object-oriented specification language to allevi- ate the burden of translating JML to DynAlloy. • TACO, a prototype tool which implements the entire tool-chain. Secondly, we introduce a novel, general and fully automated technique for the SAT-based analysis of JML-annotated Java sequential programs dealing with complex linked data structures. We instrument Alloy with a symmetry-breaking predicate that allows for the parallel, automated computation of tight bounds for Java fields. Experiments show that the translations to propositional formulas require significantly less propositional variables, leading to a speedup on the analysis of orders of magnitude compared to the non-instrumented SAT-based analysis.

de Caso, Guido. "Modelos abstractos de comportamiento basados en habilitación" (2013) Facultad de Ciencias Exactas y Naturales. Universidad de Buenos Aires

pdf

Resumen Registro Cita

Resumen:
Muchas interfaces programáticas de aplicación (APIs) presentan restricciones no triviales respecto al orden en que sus operaciones deben ser invocadas. Para los desarrolladores a cargo de implementar dichas APIs, validar si las mismas proveen el comportamiento esperado es un problema desafiante. De todas formas, incluso en la ausencia de requerimientos formales, los desarrolladores de APIs poseen un modelo mental informal sobre el comportamiento esperado de la API. Este trabajo apunta a asistir a estos desarrolladores en la validación de sus APIs mediante la construcción de modelos que puedan comparar con sus modelos mentales. Presentamos las abstracciones basadas en habilitación (EPAs), un novedoso modelo de comportamiento de grano grueso que presenta una versión sobreaproximada del protocolo de uso de una API. Las EPAs agrupan las instancias concretas de una API que habilitan el mismo conjunto de operaciones, lo cual ofrece buena trazabilidad entre el modelo y la API. Brindamos algoritmos que construyen EPAs a partir de especificaciones o implementaciones de APIs. Luego estudiamos nuestro enfoque mediante una serie de casos de estudio en los cuales expertos de dominio usaron EPAs para identificar problemas en APIs de escala industrial, una evaluación de la expresividad de las EPAs y tres experimentos controlados apuntando a establecer cómo entienden los desarrolladores a las EPAs. Estas experiencias confirman que los modelos de grano grueso tales como las EPAs pueden jugar un rol importante en procesos manuales tales como validación.

Abstract:
Many application programming interfaces (APIs) present non-trivial restrictions with respect to the order in which their operations ought to be called. For a developer in charge of implementing an API, validating whether it provides the expected behaviour is a challenging problem. Nevertheless, even in the absence of formal requirements, API implementers possess an informal mental model of the expected API behaviour. This work aims to assist these developers in the validation of their APIs by constructing models that they can compare against their mental models. We introduce enabledness-preserving abstractions (EPAs), a novel coarse-grained behaviour model which presents an overapproximated version of an API usage protocol. EPAs group concrete instances of an API that enable the same set of operations, offering good traceability links between the model and the API. We present EPA construction algorithms from either API specifications or API implementations. We then study our approach by means of a series of cases studies where experts used EPAs to identify issues in industrial strength APIs, an evaluation of EPA expressiveness, and three controlled experiments aimed at establishing how developers understand EPAs. These experiences confirm that coarse-grained models such as EPAs can play an important role in human-intensive processes such as validation.

Moscato, Mariano Miguel. "Mejoras a la demostración interactiva de propiedades Alloy utilizando SAT-Solving" (2013) Facultad de Ciencias Exactas y Naturales. Universidad de Buenos Aires

pdf

Resumen Registro Cita

Resumen:
El análisis formal de especificaciones de software suele atacarse desde dos enfoques, usualmente llamados: liviano y pesado. En el lado liviano encontramos lenguajes fáciles de aprender y utilizar junto con herramientas automáticas de análisis, pero de alcance parcial. El lado pesado nos ofrece lograr certeza absoluta, pero a costo de requerir usuarios altamente capacitados. Un buen representante de los métodos livianos es lenguaje de modelado Alloy y su analizador automático: el Alloy Analyzer. Su análisis consiste en transcribir un modelo Alloy a una fórmula proposicional que luego se procesa utilizando SAT-solvers estándar. Esta transcripción requiere que el usuario establezca cotas en los tamaños de los dominios modelados en la especificación. El análisis, entonces, es parcial, ya que está limitado por esas cotas. Por ello, puede pensarse que no es seguro utilizar el Alloy Analyzer para trabajar en el desarrollo de aplicaciones críticas donde se necesitan resultados concluyentes. En esta tesis presentamos un cálculo basado en álgebras de Fork que permite realizar demostraciones en cálculo de secuentes sobre especificaciones Alloy. También hemos desarrollado una herramienta (Dynamite) que lo implementa. Dynamite es una extensión del sistema de demostración semiatomático PVS, método pesado ampliamente utilizado por la comunidad. Así, Dynamite consigue complementar el análisis parcial que ofrece Alloy, además de potenciar el esfuerzo realizado durante una demostración usando el Alloy Analyzer para detectar errores tempranamente, refinar secuentes y proponer términos para utilizar como testigos de propiedades cuantificadas existencialmente.

Abstract:
Formal analysis of software models can be undertaken following two approaches: the lightweight and the heavyweight. The former offers languages with simple syntax and semantics, supported by automatic analysis tools. Nevertheless, the analysis they perform is usually partial. The latter provides full confidence analysis of models, but often requires interaction from highly trained users. Alloy is a good example of a lightweight method. Automatic analysis of Alloy models is supported by the Alloy Analyzer, a tool that translates an Alloy model to a propositional formula that is then analyzed using off- the-shelf SAT-solvers. The translation requires user-provided bounds on the sizes of data domains. The analysis is limited by the bounds, and is therefore partial. Thus, the Alloy Analyzer may not be appropriate for the analysis of critical applications where more conclusive results are necessary. In this thesis we develop Dynamite, an extension of PVS that embeds a complete calculus for Alloy. PVS is a well-known heavyweight method. It provides a semi-automatic theorem prover for higher order logic. Dynamite complements the partial automatic analysis offered by the Alloy Analyzer with semi-automatic verification through theorem proving. It also improves the theorem proving experience by using the Alloy Analyzer to provide automatic functionality intended for early detection of errors, proof refinement and witness generation for existentially quantified properties.

Ponzio, Pablo Daniel. "Cómputo secuencial eficiente de cotas ajustadas, y su impacto en la performance de los análisis de programas basados en SAT" (2014-06-13) Facultad de Ciencias Exactas y Naturales. Universidad de Buenos Aires

pdf

Resumen Registro Cita

Resumen:
Dada una descripción formal de los estados válidos del heap -por ejemplo, un invariante de una estructuras de datos- las cotas ajustadas para los campos del heap son el conjunto de los valores que pueden tomar los campos en alguna instancia válida. Así, los valores de campos que no pertenecen a las cotas ajustadas pueden ser ignorados por los análisis automáticos (acotados) de código, reduciendo así el espacio de estados a explorar, y mejorando la performance del análisis. Sin embargo, el cómputo de cotas ajustadas es costoso. El único enfoque conocido que computa estas cotas en un tiempo aceptable, TACO+, es intrínsecamente paralelo, y requiere de un cluster con varias computadoras para su ejecución eficiente. En este trabajo se aborda el problema de computar eficientemente cotas ajustadas en entornos de ejecución secuenciales. Así, se presentan dos nuevos enfoques para resolver este problema. El primero, denominado bottom-up, utiliza un procedimiento de decisión basado en SAT para visitar instancias válidas del heap, y computa cotas ajustadas usando los valores de los campos de estas instancias. bottom-up, al igual que TACO+, requiere de una especificación en algún lenguaje declarativo de alto nivel -como JML para JAVA- de los estados válidos del heap. De esta manera, bottom-up y TACO+ generan cotas ajustadas equivalentes. El segundo, SLBD, se basa en una especificación del heap en términos de un predicado inductivo de la lógica de separación. Este enfoque computa cotas ajustadas mientras realiza (un número finito de) desplegados del predicado inductivo de entrada. En algunos casos SLBD puede producir cotas ajustadas diferentes a las de TACO+ (y bottom-up). Se evaluaron experimentalmente los enfoques bottom-up, SLBD y la técnica relacionada TACO+, en la generación de cotas ajustadas para varias clases contenedoras JAVA. Los resultados muestran que, en un ambiente de ejecución secuencial, bottom-up es un orden de magnitud más rápido que TACO+ (secuencializado), y que SLBD es dos órdenes de magnitud más rápido que bottom-up. Además, se evaluó el impacto de las cotas ajustadas generadas por nuestros enfoques en la veri ficación de código y en la generación exhaustiva de estructuras (que satisfacen un predicado) basados en SAT. Los resultados indican que los enfoques que computan cotas ajustadas secuencialmente (vía bottom-up o SLBD), y luego las aprovechan durante el análisis, son significativamente más eficientes que los análisis convencionales, que no explotan la idea de cotas ajustadas. Además, para los análisis basados en SAT mencionados, los resultados muestran que las cotas ajustadas computadas por SLBD tienen un impacto similar a las computadas por TACO+ y bottom-up.

Abstract:
Given a formal description of the feasible heap states -for example, an invariant for a data structure-, tight field bounds for heap fields are the set of values that the fields can take in any valid instance. Thus, field values that do not belong to the tight field bounds can be safely ignored by automated (bounded) program analyses, reducing the state space to be explored, and improving the performance of the analysis. However, computing tight field bounds is an expensive process. The only known approach to compute these bounds that performs reasonably, TACO+, is intrinsically parallel, and it requires a cluster of several computers to run efficiently. In this work we address the problem of computing tight field bounds efficiently under a secuential execution environment. Thus, we introduce two novel approaches to solve this problem. The first, called bottom-up, uses a SAT based decision procedure to traverse valid heap instances, and computes tight field bounds using the field values of the visited instances. bottom-up, like TACO+, requires a description of the feasible heap states in a high level declarative language -like JML for JAVA-. In this way, bottom-up and TACO+ yield equivalent tight field bounds. The second, SLBD, is based on a specification of the valid heap states in terms of a separation logic's inductive predicate. This approach computes tight field bounds during the process of unfolding its input's inductive predicate (a finite number of times). In some cases, the tight field bounds computed by SLBD and TACO+ (and bottom-up) might differ. We assessed bottom-up, SLBD and the related technique TACO+ experimentally, in generating tight field bounds for several JAVA container classes. The results show that, under a secuential execution environment, bottom-up is an order of magnitude faster than TACO+ (secuentialized), and that SLBD is two orders of magnitude faster than bottom-up. Moreover, we assesed the impact of the tight field bounds produced by our approaches in SAT based code analysis and in exhaustive bounded generation of structures (satisfying a predicate). The results show that the approaches that compute tight field bounds secuentially (via bottom-up or SLBD), and subsecuently exploit them during analysis, are significatively faster than the more conventional analyses that do not take advantage of tight field bounds. Furthermore, for the aformentioned SAT based analyses, the experiments show that the tight field bounds computed by SLBD have a similar impact to those computed by TACO+ and bottom-up.

Czemerinski, Hernán. "Criterios basados en abstracciones de comportamiento para testing de conformidad de protocolos" (2015-04-14) Facultad de Ciencias Exactas y Naturales. Universidad de Buenos Aires

pdf

Resumen Registro Cita

Resumen:
Los artefactos de código que tienen requerimientos no triviales con respecto al orden en el que sus métodos o procedimientos deben ser invocados son comunes y aparecen, por ejemplo, como implementaciones de APIs y objetos. El testeo de que dichos artefactos se ajusten a su protocolo esperado es un problema importante y desafiante. En esta tesis se proponen y estudian criterios de adecuación de testing de conformidad basados en cubrir una abstracción de la semántica del comportamiento esperado. Por lo tanto, los criterios son independientes tanto del lenguaje de especificación y las estructuras sintácticas usadas para describir el protocolo esperado como del lenguaje utilizado para implementarlo. En consecuencia, los resultados pueden ser de utilidad para diversos enfoques de caja negra para el testeo de conformidad de protocolos. Los resultados experimentales muestran que los criterios propuestos son buenos predictores de detección de fallas de conformidad y de criterios de cobertura estructurales clásicos como cobertura de sentencias y ramas. Además, también muestran que la división del dominio derivado de los criterios propuestos produce subdominios densos en fallas, y que al priorizar casos de test de acuerdo con los criterios propuestos se tiende a producir ordenamientos que generan una detección temprana de fallas de conformidad de protocolos.

Abstract:
Code artefacts that have non-trivial requirements with respect to the ordering in which their methods or procedures ought to be called are common and appear, for instance, in the form of API implementations and objects. Testing such code artefacts to gain confidence in that they conform to their intended protocols is an important and challenging problem. In this thesis we propose and study experimentally conformance testing adequacy criteria based on covering an abstraction of the intended behavior's semantics. Thus, the criteria are independent of the specification language and structure used to describe the intended protocol and the language used to implement it. As a consequence the results may be of use to black box conformance testing approaches in general. Experimental results show that the criteria are a good predictor for fault detection for protocol conformance and for classical structural coverage criteria such as statement and branch coverage. Additionally, they also show that the division of the domain derived from the criterion produces subdomains such that most of its inputs are fault-revealing, and that prioritising test cases according to the abstraction coverage achieved tends to produce orderings that lead to earlier detection of protocol conformance failures.

Pavese, Esteban. "Garantías cuantitativas para espacios de estados no tratables" (2015-10-19) Facultad de Ciencias Exactas y Naturales. Universidad de Buenos Aires

pdf

Resumen Registro Cita

Resumen:
Los lenguajes basados en máquinas de estados finitos (también llamados automátas finitos) son usados de manera ubicua para la especificación de sistemas de software. La formalidad de estos modelos permite la aplicación de técnicas de validación tales como el model checking. De esta manera, pueden responder con seguridad si un sistema cumple o no las propiedades de interés. Al mismo tiempo, estás máquinas pueden ser utilizadas de manera composicional, especificando comportamientos aislados mediante varias máquinas, y estableciendo el comportamiento global mediante su composición en paralelo. Este enfoque reduce el esfuerzo de validación, ya que la validez de las propiedades en el sistema deberían ser dependientes de la validez de las propiedades en cada componente. Sin embargo, este enfoque es amenazado por la complejidad del sistema especificado, dando lugar al problema de la explosión de estados, que puede impedir la aplicación de estas técnicas. En esta tesis presentamos un enfoque que intenta paliar este problema, proveyendo información cuantitativa respecto de la propiedad que se intentó validar sin éxito. Nuestro enfoque se sostiene sobre dos contribuciones distintas, donde cada una de ellas puede, además, ser aplicada en el contexto de problemas relacionados. Esta tesis se inspira en el modelado y model checking probabilísticos, que pueden proveer información cuantitativa respecto de la validez de una propiedad. Esta cuantificación nos sirve de validación parcial en el contexto del problema que nos interesa. Sin embargo, un enfoque composicional tiene sus propios problemas en un contexto probabilístico. Las anotaciones probabilísticas asociadas a eventos independientes precisan ser contrastadas con estimaciones obtenidas de la observación del comportamiento a modelar. Al agregar estas anotaciones, es preciso distinguir las fuentes de estas probabilidades; en otras palabras, las probabilidades de eventos independientes deberían estar asociadas al comportamiento de los componentes que generan este comportamiento. A su vez, es preciso mantener la relación entre la validez de los componentes de manera aislada, y la validez de los comportamientos en el sistema compuesto. Los formalismos disponibles al momento, sin embargo, no proveen la seguridad de que estos resultados de validez sean preservados durante la composición. La primera contribución de esta tesis es, entonces, una extensión probabilística al formalismo de Interface Automata. Esta extensión asegura la preservación de comportamiento tal como es observado por la lógica probabilística pCTL. La segunda parte de esta tesis apunta al análisis de estos modelos, en particular cuando un análisis exhaustivo no es factible, teniendo en cuenta que la complejidad del model checking probabilístico es aún mayor que en el caso clásico. Nuestra hipótesis en este trabajo es que una exploración parcial, pero sistemáticamente controlada, puede proveer cotas a los valores de interés con un costo computacional reducido. Los experimentos realizados sugieren que un análisis mediante este enfoque puede ser más efectivo que tanto el model checking exhaustivo como así también enfoques estadísticos relacionados.

Abstract:
System specifications have long been expressed through automatabased languages, which enable automated validation techniques such as model checking. Automata-based validation has been extensively used in the analysis of systems, where they have been able to provide yes/no answers to queries regarding their temporal properties. Additionally, a compositional approach to construction of software specifications reduces the specification effort, allowing the engineer to focus on specifying individual component behaviour; and then analyse the composite system behaviour. This also reduces the validation effort, since the validity of the composite specification should be dependent on the validity of the components. However, even in a compositional approach, automatic validation techniques usually cannot cope with systems under analysis that grow complex enough. Problems such as state space explosion seriously hamper the applicability of these approaches. In this thesis, we present an approach that can help cope with these absence of results by providing quantitative validation information related to the property being validated, even when the model checking approach is unable to handle the whole system. Our proposed technique stands on two different approaches, with each of them being applicable on its own to related problems. The inspiration is that probabilistic modelling and checking can provide quantitative information, which can in turn serve as partial validation when full checking is infeasible. Compositional construction, however, poses additional challenges in a probabilistic setting. Numerical annotations of probabilistically independent events must be contrasted against estimations or measurements, taking care of not compounding this quantification with exogenous factors, in particular other system components’ behaviour. The validity of compositionally constructed specifications requires that the validated probabilistic behaviour of each component continues to be preserved in the composite system. However, existing probabilistic automata-based formalisms do not support behaviour preservation of non-deterministic and probabilistic components over their composition. The first contribution of this thesis is a probabilistic extension to Interface Automata which preserves pCTL properties. This extension not only supports probabilistic behaviour but also allows for weaker prerequisites to interfacing composition, allowing for specification refinement of internal behaviour. The second part of our approach aims at analysing these probabilistically enriched models, obtaining quantitative information that can be related to the validity of the property under analysis, even when a complete analysis is infeasible. Computational complexity of estimating these metrics can be prohibitive, even more so than classic model checking. Our hypothesis is that a (carefully crafted) partial systematic exploration of a system model can provide better bounds for these quantitative model metrics at lower computation cost than exhaustive exploration. Our technique combines simulation, invariant inference and probabilistic model checking to produce a probabilistically relevant portion of the model, which is then exhaustively analysed. We report on experiments that suggest that metric estimation using this technique (for both fully probabilistic models and those exhibiting non-determinism) can be more effective than (full model) probabilistic and statistical model checking.

Rosner, Nicolás Leandro. "Técnicas distribuídas para verificación acotada eficiente" (2015-12-15) Facultad de Ciencias Exactas y Naturales. Universidad de Buenos Aires

pdf

Resumen Registro Cita

Resumen:
El análisis formal de artefactos de software suele dividirse en dos clases de enfoques: pesados y livianos. Los métodos pesados ofrecen plena certeza del resultado obtenido pero requieren usuarios expertos. Los métodos livianos son más fáciles de aprender y se materializan en herramientas totalmente automáticas, pero la validez de sus resultados es parcial. Por ejemplo, en las técnicas de verificación exhaustiva acotada, la validez del resultado devuelto por la herramienta automática siempre está limitada por alguna noción de alcance o tamaño máximo configurable por el usuario. Para incrementar el grado de confianza en el resultado, el usuario sólo debe aumentar ese alcance y volver a ejecutar la herramienta. Sin embargo, el costo computacional del análisis automático es casi siempre exponencial en dicho alcance. En esta tesis presentamos una serie de técnicas y herramientas cuyo objetivo es mejorar la escalabilidad del análisis exhaustivo acotado de artefactos de software. En particular, nos interesa poder aprovechar la disponibilidad de hardware de bajo costo (como por ejemplo clusters de PCs, existentes en muchas empresas e instituciones) para extender la frontera de lo tratable mediante esta clase de enfoques. Por una parte presentamos transcoping, un enfoque incremental para explorar problemas de verificación exhaustiva acotada en tamaños pequeños y extrapolar la información recolectada para asistir la toma automática de decisiones en tamaños mayores del mismo problema. Mostramos su aplicación al análisis distribuido de modelos Alloy, así como a la toma de decisiones en la generación de casos de test basada en invariantes híbridos. También presentamos Ranger, otra técnica distinta para distribuir el análisis de modelos Alloy, que divide el problema en subproblemas de menor complejidad linealizando el espacio de potenciales contraejemplos y partiéndolo en intervalos disjuntos. Por otra parte, construyendo sobre la noción de cotas ajustadas para campos de la técnica TACO, presentamos MUCHO-TACO, una técnica para distribuir la verificación de programas Java anotados con contratos JML, basada en la herramienta secuencial TACO. Por último presentamos BLISS, un conjunto de técnicas para refinar la búsqueda de estructuras válidas durante la ejecución simbólica, basadas en Symbolic PathFinder.

Abstract:
Formal analysis of software artifacts is often divided into two kinds of methods: heavyweight and lightweight. The former offer complete certainty in the result, but require interaction with highly trained expert users. The latter are easier to learn and supported by fully automated tools, but the validity of their results is typically partial. For instance, in bounded exhaustive analysis techniques, the validity of the result is always limited by some notion of scope or maximum size provided by the user. To increase the level of confidence of the result, the user can simply increase the scope of the analysis and run the tool again. However, the computational cost of such automated analyses is almost always exponential in said scope. In this thesis we present a series of techniques and tools with the common goal of improving the scalability of bounded exhaustive analysis of software artifacts. In particular, we are interested in leveraging the availability of low-cost hardware (such as PC clusters, which are currently available in many companies and institutions) in order to push the tractability barrier of bounded exhaustive analysis techniques. We present transcoping, an incremental approach that explores bounded exhaustive verification problems at small sizes, gathers information, then extrapolates it in order to make better-informed decisions at larger sizes of the same problems. We show its application to the distributed analysis of Alloy models, as well as to the generation of bounded exhaustive test suites using hybrid invariants. We then present Ranger, another technique to distribute the analysis of Alloy models which splits the problem into subproblems of lower complexity by linearizing the space of potential counterexamples and dividing it into disjoint intervals. Building on the notion of tight field bounds from the TACO technique, we present MUCHO-TACO, a technique for distributed verification of Java programs annotated with JML contracts, based on the sequential TACO tool. We also present BLISS, a set of techniques to improve the search for valid structures during symbolic execution for non-primitive inputs based on Symbolic PathFinder.

Diehl, Alexandra. "Visualización de datos geoespaciales aplicada a la meteorología" (2016-05-02) Facultad de Ciencias Exactas y Naturales. Universidad de Buenos Aires

pdf

Resumen Registro Cita

Resumen:
La visualización de datos geoespaciales cubre un gran espectro de técnicas visuales e interactivas para la representación, interacción y análisis de datos geoespaciales. Este tipo de datos se caracteriza por tener una referencia geográfica, también puede contener una componente temporal, y usualmente proviene de fuentes masivas y heterogéneas. El diseño de herramientas efectivas para asistir a los usuarios en el proceso de razonamiento analítico de datos complejos y dinámicos constituye un gran desafío. Un diseño efectivo comprende una combinación correcta de representaciones visuales, mecanismos interactivos, y procesamiento semiautomático. Una selección equilibrada de estos elementos depende del dominio específico de aplicación. Esto puede ser sólo alcanzado por un enfoque integral donde el usuario cumple un rol central, colaborando en cada paso de su diseño y evaluación. Diferentes factores influencian este proceso, por ejemplo, el flujo de trabajo de tareas específico del dominio de aplicación, los requerimientos del usuario, y la complejidad de los datos. La presente tesis conduce al lector a través de diferentes enfoques que abordan el desafío de diseñar soluciones de visualización geoespacial eficientes, con aplicaciones específicas para la meteorología. Estos enfoques combinan distintas estrategias de visualización analítica para asistir a los pronosticadores en el análisis del pronóstico operativo del estado del tiempo. Los pronosticadores necesitan realizar un análisis rápido de la información, en el día a día. Proponemos un diseño novedoso que balancea la experiencia del usuario y el análisis semiautomático. Este diseño permite al usuario identificar tendencias y anomalías, analizar incertidumbre, y detectar errores del modelo numérico en forma ágil. También analizamos la integración de tecnologías de juegos serios y visualización científica. Nuestro diseño incorpora técnicas de visualización y tecnologías de juegos serios, en particular de simuladores de vuelo. El mismo demuestra los beneficios que esta integración puede brindar a la interacción con datos geoespaciales por medio de una aplicación de visualización 3D que explora ambientes topográficos y datos atmosféricos. Hemos evaluado la factibilidad y eficiencia de ambos enfoques por medio de diferentes casos de estudio diseñados en estrecha colaboración con meteorólogos, expertos del dominio. Esta evaluación fue realizada usando una metodología de diseño participativa e iterativa. Las conclusiones discutidas en este trabajo abrirán nuevas oportunidades de investigación para el diseño de soluciones de visualización de datos geoespaciales eficientes en el área de meteorología, en el análisis del estado del tiempo y soporte para la toma de decisiones.

Abstract:
Geospatial data visualization covers a huge scope of visual techniques and interactive mechanisms for the representation, interaction and analysis of geospatial data. This kind of data is characterized for having a geographic reference, it can have a temporal component and often comes from massive and heterogeneous sources. The design of effective tools to assist users on analytical reasoning on these complex and dynamic data constitutes a big challenge. Effective design entails a right combination of visual representations, interactive mechanisms and semi-automatic processing. A carefully chosen selection of these elements depends on the specific domain of application. This can be achieved by an integral approach where the user plays a central role, collaborating in each step of the design and evaluation. Different factors influence this process, for example, the specific domain task workflow, user’s needs and data complexity. This thesis guides readers through different approaches that address the challenge of designing efficient geospatial visualization solutions with specific applications in meteorology. Our approaches face different visual analytical strategies to assist forecasters in the analysis of operational weather forecasts. Forecasters need to perform quick analysis of the data on a daily basis. We propose novel designs that balance user experience and semiautomated analysis. They allow the user to identify trends and anomalies, to analyze uncertainty, and to detect numerical model errors in an agile process. We also analyze the integration of serious games technologies and scientific visualization. Our design combines visualization techniques and serious games technologies, in particular flight simulators. It puts forward the benefits that this integration can bring to the interaction with geospatial data by means of a specific data model design and a 3D visualizer of topographic environments and weather information. We evaluated the feasibility and efficiency of our approaches by means of several case studies designed in close collaboration with meteorologists, who are the domain experts. This evaluation was performed using an iterative and participatory methodology. Conclusions discussed in this work will open new research opportunities to enhance the design of efficient geospatial visualization tools for meteorology, weather analysis and decision-making support.

http://digital.bl.fcen.uba.ar

Biblioteca Central Dr. Luis Federico Leloir - Facultad de Ciencias Exactas y Naturales - Universidad de Buenos Aires
Intendente Güiraldes 2160 - Ciudad Universitaria - Pabellón II - C1428EGA - Tel. (54 11) 4789-9293 int 34