Tópicos para Tesis de Licenciatura

Tópicos para posibles tesis de Licenciatura:

Modelado

Estudio de una lógica temporal nueva, CSSL - una extensión del estandar industrial PSL, y su aplicación como forma de describir formalmente un sistema descrito informalmente con una combinación de casos de estudio, diagramas de secuencia, propiedades y máquinas de estado.

Síntesis de controladores

Feedback para problemas de control no realisables

La idea es la de explorar y aplicar tecnicas de debugging de especificaciones no realizables. Algunas de las tecnicas podrian ser: Extraccion de unrealisable cores, counter strategies, etc. El outcome esperado seria no solo un survey de las tecnicas existentes sino tambien la integracion de algunas de estas técnicas en MTSA para proveer feedback en caso de tener modelos no realizables.

Objetivos no funcionales

La idea es poder definir goals “no funcionales” dentro de SGR(1). Esencialmente lo que queremos es poder generar controladores con ciertas caracteristicas por fuera de los objetivos de la sintesis. Por ejemplo, quisieramos poder pedir el/los controlador/es mas concurrentes, mas “rapidos”, etc. El objetivo de la tesis es definir un lenguaje de alto nivel para especificar objetivos sobre los controladores de modo de restringir el tipo de soluciones que esperamos de un problema de control dado e implementar en MTSA dicho lenguaje.

Objetivos requeridos y deseados

La idea es poder definir goals requeridos y deseados. Creemos que para objetivos de safety esto es mas o menos sencillo de hacer, pero no esta claro como podriamos hacer esto para objetivos de liveness. El objetivo de esta tesis es entender las posibles formas de implemetar must-may goals sobre las diferentes posibles combinaciones de objetivos. Asi como implementar la tecnica en MTSA.

Dynamic adaptation

La idea es desarrollar una tecnica de sintesis de controladores que admita aprender sobre el modelo de dominio y recomputar la estrategia a seguir dinamicamente. Por ejemplo, se tiene un robot, aplicando una estrategia para conseguir un objetivo, pero mientras va descubriendo nuevos obstáculos y mientras puede sigue con su estrategia, mientras va refistrando lo que va descubriendo del mundo y periodicamente con la nueva informacion del mundo, la estrategia se re calcula. El objetivo de esta tesis es desarrollar la tecnica, implementarla usando MTSA y ademas hacer pruebas sobre robots reales o simulandolos con webots.

Estrategias de configuración para arquitecturas auto-configurables en robótica

Muchas de las arquitecturas para sistemas autónomos propuestas en la literatura tienen en su núcleo un componente capaz de generar en tiempo de ejecución estrategias para adaptar la arquitectura a los cambios en el ambiente, el sistema o los requerimientos. Estas técnicas no fuerzan ningún mecanismo para la construcción de estrategias de adaptación. La idea de esta tesis es aplicar técnicas de síntesis de controladores para la generación de estrategias de adaptación en arquitecturas auto-configurables. En particular, nos interesan sus aplicaciones en robótica. Para esto, vamos a explorar aplicaciones conocidas de técnicas de planning usando robots koala[1] , para luego adaptarlas y aplicarlas, en ambientes con robots koala reales y simulados, a técnicas de síntesis de controladores. Una muestra de las aplicaciones que esperamos adaptar, ver estos videos: [2] [3] [4] [5] .

Exploración en robótica para mapas parcialmente conocidos. 

En el área de robótica muchas veces necesitamos ofrecer garantías de que ciertos objetivos van a ser alcanzados. Sin embargo, en muchas situaciones los robots deben moverse en mapas totalmente desconocidos o parcialmente conocidos para satisfacer dichos objetivos.
Actualmente existen técnicas de síntesis de controladores discretos que resuelven bajo ciertas hipótesis este problema. Suponemos que el mapa se mantiene estático mientras el robot intenta satisfacer los objetivos como tmb la posibilidad de re ubicar el robot en el estado inicial en el caso de llegar a un dead-end en la exploración.
El objetivo de la tesis es lograr relajar estas suposiciones aceptando también mapas dinámicos (i.e. mapas que poseen objetos que se mueven mientras el robot ejecuta la misión de exploración. E.g. puentes levadizos, puertas abierta/cerrada, etc).

Modelos de enabledness

Comparador de modelos de enabledness

La idea es contar con una herramienta que tome dos modelos de enabledness y nos haga un resumen de las diferencias. En una primera versión en modo texto, las diferencias se calculan y se muestran en pantalla como una lista de ejes y estados distintos (no hay mucha diferencia con cualquier herramienta que compara grafos). En una segunda versión, se construye una herramienta visual, que aprovecha la información de enabledness e intenta ubicar los estados en lugares similares en ambos modelos para facilitar la comparación.

Enabledness Con Category Partition

El objetivos es generar modelo de enabledness donde las etiquetas correspondan a llamados a métodos con alguna restricción sobre los valores de los argumentos (por ejemplo, "insert(x) con x>5"). La idea es calcular las restricciones sobre los parámetros de manera automática mediante alguna técnica de análisis de programas que permita encontrar "categorías" de valores interesantes. El proyecto implicaría aprender primero hacer un relevamiento de técnicas automáticas para generación de casos de test basados en category partition (y cosas similares), luego tomar/adaptar/extender estas para usarlas en el contexto de generación de modelos de enabledness. Sería particularmente interesante terminar usando la herramienta ( KLEE ) La idea es contar con una herramienta que tome dos modelos de enabledness y nos haga un resumen de las diferencias. En una primera versión en modo texto, las diferencias se calculan y se muestran en pantalla como una lista de ejes y estados distintos (no hay mucha diferencia con cualquier herramienta que compara grafos). En una segunda versión, se construye una herramienta visual, que aprovecha la información de enabledness e intenta ubicar los estados en lugares similares en ambos modelos para facilitar la comparación.

Verificación cuantitativa de modelos y software

Verificación cuantitativa de código fuente

La idea es aplicar parte de la teoría de verificación cuantitativa (probabilística) directamente sobre artefactos de código fuente, pudiendo probar entonces propiedades sobre el software y no solamente sobre un modelo de éste. Inicialmente, se modificaría el verificador de código Java JavaPathfinder , y en principio sólo para manejar propiedades de reachability . Un segundo posible tema de tesis en esta misma tónica es obtener estos mismos resultados con herramientas orientadas a la verificación de código .NET.

Verificación guiada de modelos

La verificación probabilística es esencialmente monolítica. Debido a los procedimientos que se utilizan, se necesita una descripción completa del sistema a analizar, no descompuesta en componentes. Esto es un serio limitante debido a que la cantidad de estados crece exponencialmente respecto de la cantidad de estados de sus componentes. En el área de verificación clásica, existen mecanismos on-the-fly que construyen la descripción completa a medida que se va explorando. La idea es realizar una exploración similar a la de estos métodos, pero guiados por la información probabilística de los modelos, buscando minimizar/maximizar medidas de exploración relacionadas con estas probabilidades.

Generación de contraejemplos

En el ámbito de verificación clásica, al chequear si una propiedad se cumple, si se obtiene una respuesta negativa, puede obtenerse un contraejemplo para la misma. Este contraejemplo es una traza que demuestra cómo se viola la propiedad. En el caso de la verificación probabilística no es tan simple; puede darse el caso que ninguna traza única contenga suficiente probabilidad para negar la propiedad, pero que la misma sea aún falsa. Entonces, un contraejemplo probabilístico es en realidad un árbol de probabilidades donde cierta suma de trazas es testigo del no cumplimiento de la propiedad. Estos contraejemplos no son fáciles de conseguir, y además contienen información que no es relevante para la propiedad. La idea es desarrollar heurísticas para conseguir contraejemplos "simples" y otras para aislar la información relevante a la propiedad, abstrayendo lo que no resulte de interés.

Sistemas de Transiciones Modales (MTS)

Thorough Model Checking

Hace tiempo que venimos desarrollando una herramienta para la especificación y análisis de MTSs ( MTSA ). Esta herramienta tiene un procedimiento aproximado para computar el valor de una formula (de la lógica temporal lineal) en un MTS. El algoritmo "preciso", denominado thorough model-checking, es computacionalmente caro y es un caso particular de un algoritmo existente. La idea de este proyecto sería implementar thorough model checking en MTSA. Para eso será necesario entender el algoritmo general, entender como adaptarlo a MTS, entender la representación de MTSs en MTSA e implementar el algoritmo en MTSA.

Automated Legal Drafting (en el marco de FormaLex)

Especificación formal del lenguaje FL

Nuestro lenguaje de especificación legal podría beneficiarse con una definición formal y rigurosa, de manera tal de precisar un poco más su semántica.

Casos de estudio reales

Nos interesa utilizar nuestro lenguaje y herramientas para tratar casos reales y ver qué defectos encontramos. Tesista actual: Hernán Rojek Moriceau

Instanciación

Manejar la instanciación de agentes para poder hacer queries y simulaciones.

Manejo de permisos excepcionales

Transformar (automáticamente) F(kill) + P(self-defense killing) en F(kill unless self-defense).

Ampliación del lenguaje FL

Por ejemplo, para contemplar que los diamantes que hablen del mismo intervalo en una fórmula no necesariamente hablen de la misma instancia. Manejar sincronización/aliasing de eventos.

Automatic Resource Usage Analysis

El grupo viene desarrollando una línea de trabajo de inferencia y verificación de consumo de memoria dinámica en programas Java y C#. Las siguientes tesis proponen extender o completar algunas de estas técnicas. En http://www.dependex.dc.uba.ar/wiki/index.php/JConsume2 se puede encontrar información adicional y trabajo previo.

 

Verificación modular de consumo de programas Java

Incluye la definición (parcial) de un lenguaje de contratos de consumo, junto con la generación de condiciones de verificación para el envió a un demostrador de teoremas y la integración con las técnicas de inferencia de consumo actuales.

Integrar las técnicas de análisis de consumo a un entorno de desarrollo

Desarrollar un plug-in que permita la integración de las distintas herramientas de análisis. En particular se espera que los programadores puedan visualizar la salida de estas herramientas e introducir anotaciones en el código (desde resumenes de métodos hasta invariantes de ciclos, información sobre tiempo de vida de objetos, etc.) para poder asistir el proceso de inferencia.

Análisis de consumo de programas .NET

Tenemos un desarrollo parcial del un verificador para .NET (basado en Code Contracts). Queremos extenderlo con técnicas de inferencia automática para reducir el número de anotaciones requeridas e inferir contratos automáticamente. Nos interesa aplicarlo en aplicaciones móviles. En http://lafhis.dc.uba.ar/misc/resourcecontracts/ pueden encontrar trabajo previo.

Análisis de consumo de memoria en programas C

Se busca diseñar e implementar una técnica que permita inferir automaticamente el consumo de memoria de programas C. Además de los desafios propios de la inferencia, en este caso es importante poder modelar adecuadamente la memoria que es recolectada de forma manual.

Traducción de programas que manipulan punteros a programas aritméticos

El objetivo es partir de un programa Java arbitrario y obtener un programa que en término de consumo de memoria sea similar pero que solamente manipule números enteros

Verificación Modular de Programas

Manteniendo invariantes por construcción usando Dynamic Frames

El uso de Dynamic Frames esta asociado a lidiar con el problema conocido como el framing problem, que está relacionado con especificar el efecto de un método en un estado pero sin afectar el ocultamiento (information hiding). Existen varios lenguajes que adoptan esta metodología. La idea es aprovechar lenguajes con este soporte para probar automáticamente ciertos invariantes estructurales (ser una lista, un arbol, etc). En https://sites.google.com/site/acycliclanguage/ existe un propotipo que muestra algunos avances sobre esta ideas que luego fueron formalizadas en este paper [6]. El objetivo de la tesis es desarrollar un prototipo que implemente las ideas planteadas en el paper (usando de base el lenguaje Dafny) y extender el trabajo para poder probar invariantes en estructuras mas complejas.

Extensión del lenguaje Pest

Pest [7] es un lenguaje imperativo sencillo pensado con fines académicos y para experimentar con lenguajes. Pest fue pensado para facilitar la verificación modular más que para facilitar la programación, es por ello que cualquier extensión de Pest, debe ser cuidadosamente estudiada. En esta tesis proponemos extender Pest para permitir la introducción de estructuras de datos pero de una forma controlada. Para ellos se propone el estudio de mecanismos de ownership u otro tipo, por ejemplo para controlar el problema del aliasing.

Bounded Verification

El objetivo es aportar nuevos resultados que permitan obtener mejoras de escalabilidad y usabilidad de forma tal que puedan incorporarse herramientas de verificación acotadas a ambientes industriales de desarrollo. Algunos temas:

Combinando análisis dataflow con SAT-Solving

El análisis dataflow se usa para inferir automáticamente propiedades sobre el programa (en general, una abstracción del estado del programa) mediante la recolección y acumulación de la información que fluye por el grafo de control del mismo. Algunos ejemplos de instancias de análisis dataflow son: variable vivas, expresiones disponibles, definiciones alcanzables, etc. Creemos que el análisis dataflow puede ser una excelente forma de aproximar el espacio de estados del programa y aprovechar esto para realizar una reducción importante de la codificación SAT del mismo. Algunas de estas ideas fueron exploradas en [pedir paper SEFM11]. El objetivo es implementar técnicas dataflow que puedan ser aprovechas para reducir las representaciones lógicas de programas y luego reducir el espacio de busqueda del SAT-Solver,

Sinergía entre SAT-solver y SMT-Solvers:

Integración con entornos de desarrollo y análisis

Máquinas Virtuales Reflexivas

Basandose en TruffleMate (https://github.com/charig/truffleMate), el prototipo de máquina virtual reflexiva (http://dl.acm.org/citation.cfm?id=2814241) existente que optimiza su ejecución mediante Graal, un compilador por método que usa la técnica de partial evaluation.

Optimizar Máquinas Virtuales Reflexivas con compiladores por trazas

Diseñar y construir otro prototipo de una máquina virtual reflexiva para un lenguaje dinámico pero basado en un compilador por en trazas de ejecución.
Evaluar las diferencias y similitudes, tanto en performance como en complejidad de desarrollo, con el prototipo existente (TruffleMate) .
Analizar y explorar posibles nuevas optimizaciones. En especial analizar si alguna característica del tipo compilador favorece/perjudica el modelo de VM adaptativa propuesto.

Máquinas Virtuales Reflexivas para Lenguajes Funcionales 

Explorar la idea de máquinas virtuales reflexivas en el contexto de lenguajes de programación funcionales.
Evaluar las capacidades de adaptabilidad de la VM en este nuevo dominio.
Evaluar el desempeño de los compiladores dinámicos para optimizar los modelos de VM adaptativos en el contexto de los lenguajes funcionales.

Máquinas Virtuales Reflexivas Multi Threading

Explorar desde diversos enfoques (factibilidad, aplicabilidad, eficiencia, etc.) la incorporación de capacidades reflexivas en entornos multi-threading.

Testing Automático

Un nuevo generador de casos de tests para Java basado en ejecución simbólica
Construir un generador de casos de tests partiendo de la base del motor de ejecución simbólica que hoy está disponible en EvoSuite (http://www.evosuite.org) para conseguir en aplicaciones Java las mismas funcionalidades que en la herramienta Pex (C#) o KLEE (C99).

Extender DroidMate con ejecución simbólica dinámica     
La ejecución simbólica dinámica (DSE) es una técnica muy popular tanto  fuzzing como para testing de unidad. El objetivo es reutilizar los motores de ejecución simbólica existentes y aplicarlos sobre la herramienta de generación de casos de tests para aplicaciones Android llamada DroidMate (https://www.st.cs.uni-saarland.de/droidmate/).

Generación de Casos de Tests para Aplicaciones JNI    
Las aplicaciones JNI combinan código Java y código "nativo" (C, assembler, x86). El objetivo de esta tesis es extender la herramienta de generación automática EvoSuite (http://www.evosuite.org) de modo de guiar la generación para lograr mayor cubrimiento en la capa "nativa" de la aplicación.

Generación de Casos de Tests usando Enabledness-Preserving Abstractions (EPA)    
Los asbtraccciones que preservan enabledness (EPAs) son una técnica útil para medir la conformidad de un test suite que apunta a testear un object protocol (por ejemplo, un Socket). El objetivo de este trabajo es extender el generador de casos de tests EvoSuite (http://www.evosuite.org) usando criterios de recubrimiento de EPA. 

Arquitecturas

Técnicas Avanzadas de Modularización    
La Programación Orientada a Aspectos propone mecanismos avanzados de modularización para capturar conceptos que de otras maneras quedan desparramados por el código sin una correcta abstracción. La tesis propone investigar nuevas técnicas que soporten aspectos en la etapa de modelado, asi como la construcción de abstracciones necesarias para la correcta implementación de los aspectos. Otros temas relacionados: Interferencia entre aspectos. Detección Automática y Generación de Estrategias para resolución de conflictos.

Modelado Dinámico en Arquitecturas de Software    
La descripción arquitectónica de un sistema de software puede verse bajo distintas vistas que especifican la interacción entre sus principales artefactos.  Los lenguajes utilizados para describir vistas arquitectónicas suelen pasar del diseño directo a código, ausentándose así la posiblidad de explorar y analizar el comportamiento. La tesis se propone investigar alternativas para modelar el comportamiento con alto nivel de abstracción dentro del universo de arquitecturas de software.

Utilización de Lenguajes Declarativos para la Validación Formal de Protocolos de Software de manera dinámica.    
Una vez especificado el protocolo que expone un dado artefacto de software no cualquier orden en la ejecución de sus métodos puede ser válida.  La tesis propone buscar una alternativa de modelado declarativa para explorar soluciones a este problema, y poder especificar los requerimientos válidos desde una perspectiva dinámica.

Español