Investigación

uestro interés está en el uso de técnicas automatizadas para apoyar el análisis de los artefactos utilizados en la ingeniería de software, estoy incluye documentación de requerimientos y diseño así como código fuente. Actualmente la mayor parte de nuestro trabajo se desarrolla dentro de las siguientes líneas de investigación:

Especificaciones basadas en escenarios

Notaciones basadas en escenarios, como los diagramas de secuencia de UML, son utilizadas usualmente en especificaciones de requerimientos. Un escenario es una historia parcial que describe cómo los componentes del sistema, el entorno y los usuarios interactúan. Su sencillez y la representación gráfica intuitiva facilitan la participación de “stakeholders”, la comunicación con estos y la documentación final de los requirimientos.
Nuestro interés se desprende de estas características deseables de un lenguaje de especificación y nos ha llevado a investigar diversas preguntas: ¿Cómo pueden los modelos de comportamiento ser sintetizados a partir de escenarios? ¿Qué tipo de modelos de comportamiento se pueden sintetizar cuando una se tiene una descripción parcial del sistema? ¿Cómo pueden las especificaciones basadas en escenarios ser combinadas con otros tipos de especificaciones, tales como requisitos declarativos y descripciones arquitectónicas? ¿Cómo puede una implementación (o un modelo de la implementación) chequearse con una especificación basada en el escenario? ¿Qué extensiones en términos de expresividad pueden definirse a lenguajes clásicos basados en escenarios? Algunas publicaciones representativas:[Synthesising Modal Transition Systems from Triggered Scenarios - TSE in press][Specification Patterns can be formal and still easy - SEKE10]

Abstracciones automatizadas para la validación

La validación tiene como objetivo determinar cuan adecuadamente un artefacto (por ejemplo, código o los requisitos y especificaciones de diseño) representa al mundo -tal es o como se pretende que sea.
La brecha entre el lenguaje formal usado para el modelado o la programación y el mundo, que es informal por naturaleza, hace de la validación una tarea difícil. Estamos interesados en estudiar y proponer las abstracciones del comportamiento del sistema que permita a un humano comprender algunos aspectos del artefacto analizado y, entonces, asistir a su validación. En particular nos interesan las conocidas como "Enabledness Preserving Abstractions" las cuales cocientan el espacio de estados concretos a fin de agruparlos en función del conjunto de acciones habilitadas.
Hemos estudiado la construcción automatizada de tales abstracciones de código C y las especificaciones basadas en contratos, y hemos demostrado que no sólo la construcción de tales abstracciones es factible, sino también que exhiben problemas no identificados hasta ahora en las especificaciones industriales y código real.
Algunas publicaciones representativas: [Automated Abstractions for Contract Validation, TSE12][Enabledness-based Program Abstractions for Behaviour Validation. TOSEM12]

Síntesis de controladores en Ingeniería de Software

El modelo “mundo-máquina” de Michael Jackson establece un marco en el que abordar los retos de la ingeniería de requerimientos. En este modelo, los requerimientos son aserciones prescriptivas acerca del mundo, expresadas en términos de fenómenos en la interfaz entre la máquina que queremos construir y el mundo en el que viven los problemas reales a resolver. Tales problemas son capturados con aserciones prescriptivas expresadas en términos de fenómenos del mundo (pero no necesariamente parte de la interfaz de mundo-máquina) llamadas objetivos y aserciones descriptivas de lo que suponemos que es verdad en el mundo.
En dicho contexto, una tarea clave en la ingeniería de requerimientos es comprender y documentar los objetivos y las características del dominio en el que éstos serán alcanzados, con el fin de formular una serie de requerimientos para la máquina que se construirá de tal manera que, asumiendo que la descripción y objetivos del dominio son válidos, los requerimientos de tal dominio implican los objetivos.
Por lo tanto, un problema clave de ingeniería de requerimientos se puede formular como un problema de síntesis. Esto es, dado un conjunto de supuestos descriptivos sobre el comportamiento del entorno y un conjunto de objetivos del sistema, construir un modelo operativo de la máquina de modo que su composición con el entorno logra los objetivos.
Este problema se adecúa perfectamente con el problema de síntesis de controladores. A pesar de haber sido ampliamente estudiada, la síntesis de controladores no ha sido desarrollada en profundidad en el contexto de la ingeniería de software. Nuestro interes es el de entender cómo adaptar y ampliar los resultados de síntesis de controladores para soportar las tareas de ingeniería de software relacionadas con los modelos basados ​​en eventos, a nivel de arquitectura y comportamiento. En particular, estudiamos aplicaciones de síntesis de controladores para la elaboración de modelos de comportamiento, incluyendo el uso de modelos de comportamiento parciales, asi como de sistemas adaptativos.

 

Algunas publicaciones representativas: [The Modal Transition System Control Problem,FM12][Synthesising Non-Anomalous Event-Based Controllers for Liveness Goals]

Modelado y Análisis de Requerimientos de Memoria Dinámica para Software Embebido

Actualmente convivimos con miles de millones de dispositivos electrónicos corriendo varios subsistemas de software. Estos sistemas suelen fallar aunque no siempre los problemas se deben a errores funcionales. Existen casos donde un sistema, a pesar de su correcta concepción, pueda ejecutar de forma degradada o incluso fallar por no poseer los recursos necesarios para su funcionamiento. En otros casos, un sistema puede estar utilizando una cantidad de recursos excesiva para la tarea que cumple. Por ejemplo, los teléfonos inteligentes, a pesar de ser cada vez más potentes, poseen una capacidad de procesamiento, memoria y energía limitadas, además de necesitar comunicarse de formar permanentemente con otros dispositivos, incurriendo en costos que es necesario controlar. Incluso en ambientes completamente diferentes, tales como clusters o granjas de computadoras (cloud computing), donde los recursos parecerían en principio ilimitados, la sustentabilidad del negocio radica justamente en poder administrar los recursos de forma eficiente.
El análisis cuantitativo de los diferentes recursos computacionales pasa a ser de vital importancia tanto para ejecutar aplicaciones de forma correcta como para poder dimensionar adecuadamente el hardware necesario para una determinada tarea o servicio.
Apuntamos al desarrollo de un conjunto de técnicas de análisis estático y dinámico, escalables y usables, que permitan el análisis cuantitativo de recursos. Nos interesan técnicas de inferencia y verificación de certificados de consumo de recursos, así como técnicas de testing dirigidas por el uso de recursos. Uno de los principales focos esta en analizar información concerniente al consumo de memoria. Este interés particular radica en que, a diferencia de otro tipo de recursos, este evoluciona de forma no monótona con respecto al tiempo, debido a los administradores de memoria que reciclan los objetos que dejan de ser usados por la aplicación.

 

Algunas publicaciones representativas:[Quantitative dynamic-memory analysis for Java,CCPE11][Symbolic Polynomial Maximization over Convex Sets and its Application to Memory Requirement Estimation,VLSI09]

Modelado de comportamiento parcial

A pesar de haber mostrado ser eficiente en el descubrimiento de errores sutiles en requerimientos y diseño, la adopción industrial de técnicas de modelado y análisis de comportamiento, es escasa.
Creemos que una de las causas de la falta de adopción es que las técnicas tradicionales de modelado de comportamiento requieren descripciones completas del comportamiento (fijado un nivel de abstracción) previo a cualquier análisis. Por ejemplo, se asume que una máquina de estado debe describir de manera el comportamiento de un sistema (o componente del mismo) respecto a un alfabeto pre-fijado de acciones.
Esta presunción de completitud es limitante en el contexto de las mejores prácticas de procesos de desarrollo de software, que incluyen el desarrollo iterativo, la adopción de casos de uso y técnicas basadas en escenarios y análisis basados en punto de vista o actores; prácticas que requieren modelado y análisis en la presencia de información parcial sobre el comportamiento del sistema.
Creemos que hay mucho que ganar al cambiar el enfoque en la ingeniería de software de los modelos tradicionales de comportamiento a modelos de comportamiento parciales. Estos últimos son aquellos que son capaces de distinguir el comportamiento para el cual se conoce si es requerido o prohibido, de comportamiento para el cual que aún no se sabe si es deseable (porque no se le preguntó al stakeholder o simplemente es anti-económico decidirlo ahora).
Nuestro objetivo general es desarrollar los fundamentos, técnicas y herramientas que permitan la construcción automatizada de modelos de comportamiento parciales a partir de múltiples fuentes de especificaciones parciales. Queremos proveer feedback temprano a través del análisis automatizado de modelos de comportamiento parcial, y tambiern dar soporte al desarrollo incremental e iterativo de estos modelos parciales. Algunas publicaciones representativas:[Weak Alphabet Merging of Partial Behaviour Models,TOSEM12][Distribution of Modal Transition Systems,FM12]

Verificación y diagnóstico automatizados

Las técnicas de verificación que han sido desarrolladas en la última década han mostrado ser efectivas en el descubrimiento de problemas en artefactos formales que se construyen a lo largo del proceso de desarrollo de un sistema (por ejemplo código, requerimientos y especificaciones de diseño) y puesta en producción (por ejemplo, configuraciones de red e infraestructura). Sin embargo, la verificación proporciona prácticamente ninguna ayuda para comprender las causas de los problemas descubiertos, y menos aún para solucionarlos. Cuando falla la verificación, nos quedamos con ejemplos de cómo se produce esa falla, pero no con una comprensión de por qué. Pasar del síntoma detectado automáticamente a la causa en el artefacto bajo análisis y su posterior arreglo es un problema difícil para el cual existe póco soporte automático.
El soporte automatizado para el diagnóstico y la reparación podría reducirs significativamente el esfuerzo humano involucrado en el desarrollo de software. Una herramienta que proponga explicaciones plausibles y soluciones correctas para los problemas identificados en las actividades de verificación permitiría a los ingenieros concentrarse en las decisiones clave y no en la tediosa búsqueda de errores y su corrección. El problema de “explicar” un conjunto de ejemplos (e.g. trazas que fallan) en términos de una teoría dada (e.g. un programa y su especificacion) y adaptar la teoría para evitar los ejemplos, es abordado por la disciplina denominada aprendizaje simbólico, una disciplina de la Inteligencia Artificial que ha experimentado una revolución en la última década. Sin embargo, el uso de estos métodos de aprendizaje no ha penetrado la ingeniería de software a pesar de que la correspondencia entre la tarea de aprendizaje y las tareas de verificación-diagnóstico-reparación es directa: La teoría es el artefacto construido, desplegado o ejecutado, mientras que el síntoma es el resultado de la verificación.
Actualmente estamos investigando la combinación de verificación y técnicas de aprendizaje simbólico (más específicamente model checking y programación lógica inductiva) para evolucionar, elaborar y fijar las especificaciones de requerimientos.
Algunas publicaciones representativas:[Generating obstacle conditions for requirements completeness,ICSE12][Deriving Non-Zeno Behavior Models from Goal Models using ILP,FACS10]

Español