Sistemas de información y de gestión

Los productos de software actuales requieren alta calidad, especialmente en el ámbito de sistemas críticos (sistemas de control en vehículos, aeronaves, equipamiento médico, etc). Las propiedades de calidad requeridas son tanto funcionales (corrección, por ejemplo) como no funcionales (tiempos de respuesta, consumo de memoria, seguridad y otros).

Las técnicas utilizadas para verificar estas propiedades varían desde métodos rigurosos, conocidos como métodos formales, hasta métodos más ad-hoc como testing de software.

Los primeros son mas precisos pero tienen graves problemas de escalabilidad (no usables aún en proyectos de mediana escala), requieren anotaciones y/o uso de herramientas avanzadas como asistentes de pruebas. En el otro extremo, el testing, es ampliamente usado, teniendo la desventaja que es un método incompleto, ya que generalmente permite verificar un subconjunto posible de escenarios.

Las técnicas de análisis estático (liviano), se basan en técnicas rigurosas pero de menor precisión, razonando sobre abstracciones de alto nivel (como type checking en compialadores). Las abstracciones son conservadoras por lo cual pueden generar falsos positivos (rechazar programas que no revelarán defectos en su ejecución).

En este proyecto se propone continuar con la línea de trabajo del grupo, desarrollando nuevos sistemas de tipos y modelos de análisis estático para encontrar defectos basados en propiedades más complejas verificables automáticamente. Además se pretende usar estas técnicas para complementar otras como testing, generando automáticamente casos de prueba para la eliminación o verificación de alertas generados por el sistema de análisis estático.

La temática fundamental del proyecto es el diseño, desarrollo y evaluación de técnicas de análisis automático de software, concretamente técnicas para la validación y verificación, basadas en constraint solving. Constraint solving es el proceso de decidir automáticamente, dada una fórmula en algún formalismo particular, si la misma es satisfactible o no, y admite diversos enfoques, entre los que se encuentran SAT (boolean satisfiability) y SMT (satisfiability modulo theories) solving. Diversos problemas complejos en el ámbito de la Ingeniería de Software se pueden reducir a alguna forma de constraint solving, como SAT o SMT. El objetivo general de este proyecto es contribuir a la calidad y confiabilidad de sistemas de software, mediante de la automatización de tareas propias de la validación y verificación de software, como el análisis de especificaciones, la generación automática de tests, la verificación, y la depuración. Esta temática incluye el desarrollo de formalismos para la descripción formal o rigurosa de diferentes aspectos del software, la definición de metodologías adecuadas de aplicación de estos formalismos, y especialmente técnicas automáticas de análisis basadas en SAT y/o SMT, que permitan soportar su uso y aplicación práctica. Esto último corresponde a la reducción de las tareas antes mencionadas a SAT/SMT solving, y depende fuertemente de la disponibilidad de herramientas de software potentes asociadas a estas técnicas; es un objetivo de este proyecto desarrollar prototipos de tales herramientas.

El crecimiento sostenido de la industria del software y su constante expansión a nuevos ámbitos, genera un estado de alerta y constante revisión de las metodologías de desarrollo de software utilizadas, como así también de los métodos de trabajo, la adopción de nuevas herramientas para automatizar y mejorar las actividades de gestión e ingeniería, como la planificación, el diseño y la implementación, involucradas en el proceso de producción de software. A pesar de las investigaciones y estudios realizados, existen aún numerosos casos en los que no se ha podido evitar que los errores de software lleguen a etapas de producción. Con este proyecto se propone mejorar la calidad de los sistemas de software que se desarrollan, continuando con la investigación y el estudio de técnicas y procesos de desarrollo de software con diferentes enfoques. La aplicación de transformaciones de modelos a la generación automática de API REST, la técnica de ejecución simbólica aplicada al análisis de código, las aplicaciones de testeo automatizado aplicadas en las pruebas de sistema web, y el análisis de los atributos de calidad deseables en herramientas de software educativo para el desarrollo del pensamiento computacional, son las propuestas de trabajo que surgen en el marco de este proyecto, con el objetivo central de aportar mejoras y soluciones para el perfeccionamiento de los procesos de desarrollo que provoquen un mejora en la calidad de los productos de software, minimizando las fallas y aumentando la confiabilidad.

En este proyecto se toma como eje de investigación, la construcción del pensamiento computacional en el marco de la enseñanza de las ciencias naturales en la escuela primaria. Se busca comprender las posibilidades y limitaciones de la enseñanza de las ciencias de la computación en las prácticas de enseñanza de las ciencias naturales que realizan los docentes de nivel primario, además de la selección y uso de software educativo, y la evakuación de la calidad de dichas herramientas. La investigación se plantea como un estudio cualitativo, descriptivo-interpretativo. Dentro del plan de acción se espera: a) diseñar y evaluar propuestas de enseñanza de las ciencias naturales, en forma colaborativa con los docentes de nivel primario, que aporten a la construcción del pensamiento computacional. c) evaluar calidad de herramientas y aplicaciones de software educativo c) participar en el desarrollo de nuevas aplicaciones educativas o extensión de las existentes, apuntadas a la construcción de PC,  d) vincular los procesos de investigación con los procesos de innovación en la enseñanza de las ciencias naturales y de la computación, mediante la consolidación de un equipo de estudios interdisciplinario.

Hasta hace algunas décadas, la forma más usual de comprender y/o caracterizar el comportamiento del software era a través de su correspondiente función o relación de cómputo input/output. Sin embargo, es cada vez más frecuente entender el comportamiento de sistemas de otra manera, especialmente con el auge actual de Sistemas Reactivos y Concurrentes. Muchos sistemas poseen un comportamiento que no depende exclusivamente de una serie de datos iniciales, sino que tienen un comportamiento dinámico asociado a la ocurrencia de eventos y la reacción a los mismos, y la interacción con el ambiente en los que se encuentran. Más aún algunos sistemas, como por ejemplo, sistemas de control en vehículos, aviones, de control industrial y otros, constituyen sistemas críticos ya que cualquier error lógico pueden causar daños materiales o peor aún, poner en riesgo la vida de las personas que directa o indirectamente son usuarios de estos dispositivos.

Debido a la complejidad intrínseca que conlleva este tipo de sistemas, existe una creciente demanda por parte de la industria de metodologías que permitan a los desarrolladores aumentar la confianza en el diseño y la construcción de los mismos.

Este proyecto pretende el desarrollo e integración de herramientas que permitan la verificación de propiedades de componentes y/o modelos de software para poder lograr garantías como ausencia de ciertos tipos de errores y cumplimiento de ciertas normas de comportamiento. Las técnicas utilizadas incluyen desde lógicas y teorías específicas, sistemas de tipos avanzados, modelos matemáticos y uso de heurísticas a medida.

Los sistemas críticos son aquellos  sistemas de computación utilizados en áreas  en  las cuales  las fallas, o los eventos inesperados, pueden ocasionar grandes  perdidas de dinero; o quizás peor aún, daños a vidas humanas. Esta clase de sistemas  juegan un rol importante en actividades esenciales de la sociedad tales como la medicina y las comunicaciones. Los sistemas críticos, cada vez son más usuales en la vida real, algunos ejemplos de estos son los sistemas de aviones, sistemas para automóviles y sistemas utilizados en telefonía móvil.  Para minimizar las fallas, y las perdidas materiales o humanas ocasionadas por  el funcionamiento incorrecto de dichos sistemas, se utilizan técnicas de tolerancia a fallas. Estas técnicas permiten que los sistemas continúen funcionando aún bajo la ocurrencia de fallas, o eventos inesperados. Existen diversas técnicas para lograr  tolerancia a fallas utilizando, por ejemplo, redundancia a diferentes niveles de abstracción, como, por ejemplo, al nivel de hardware. .

El objetivo del presente proyecto es estudiar tanto marcos teóricos, que permitan la construcción de sistemas tolerantes a fallas, como también herramientas automáticas que hagan posible la utilización de estos formalismos en escenarios complejos. Para lograr estos objetivos, será necesario considerar  casos de estudios de diferente complejidad, y además que sean relevantes  en la práctica. Ejemplos de estos son: bombas de insulina, protocolos de comunicación, sistemas de vuelo y sistemas utilizados con fines médicos.