Resumen

Los sistemas de computación están sustituyendo paulatinamente a tareas que, de forma tradicional y debido a su carácter crítico, se han realizado manualmente. Esta explosión de nuevas aplicaciones ha sido posible gracias a la mejora de los dispositivos hardware que finalmente automatizan los procesos, y al desarrollo de la industria del software que ha producido nuevas tecnologías de programación de nivel intermedio y alto, con un poder expresivo mucho mayor, capaces de resolver problemas de gran magnitud.

De forma simultánea a este crecimiento en la demanda de servicios software, se han desarrollado las denominadas técnicas formales, que tienen como objetivo mejorar la calidad y fiabilidad del software que se proporciona al usuario. Estas técnicas hacen uso del lenguaje matemático para minimizar el número de errores, garantizando que el software satisface un conjunto de propiedades que se consideran críticas para su campo de aplicación. Aunque en un principio, el uso de las técnicas formales fue cuestionado por su dudosa aplicación práctica, hoy día, su uso está ampliamente aceptado, de manera que el desarrollo de cualquier producto suele ir acompañado de su modelado y/o análisis mediante alguna técnica formal. Esto se debe, fundamentalmente, al desarrollo de técnicas de modelado y análisis potentes, así como de herramientas que soportan estas técnicas y que han probado extensamente su utilidad en la práctica.

Quizás el método conocido como model checking es el que más ha influido en esta integración progresiva de las técnicas formales en el desarrollo del software, fundamentalmente de software concurrente o distribuido. La amplia difusión del model checking y su evidente éxito a nivel industrial se debe a que combina de manera equilibrada la formalización matemática, tanto de las propiedades como del sistema software que se pretende analizar, y el carácter práctico, puesto que el model checking es una técnica algorítmica orientada a la construcción de herramientas que lleven a cabo de forma automática la tarea compleja de la verificación del software.

La tendencia actual en el área de las técnicas formales es, por lo tanto, la búsqueda de nuevos formalismos, o la extensión de los ya existentes, teniendo en cuenta aspectos diferentes del software que clásicamente no se han considerado. Por ejemplo, la mayoría de los sistemas que aparecen en el mundo real no son completamente discretos, sino que tienen alguna componente, normalmente asociada a algún dispositivo físico, que se comporta de forma continua. Este tipo de sistemas se denominan híbridos, y se caracterizan porque en ciertos momentos se comportan de forma discreta, mientras que, en otros, evolucionan siguiendo una dinámica continua (no numerable). Otro aspecto interesante de los sistemas reales es que, en muchos casos, tienen un comportamiento aleatorio, de manera que incorporan algún parámetro de incertidumbre, existiendo alguna función que define su evolución probabilística. Para modelar y analizar sistemas híbridos y/o probabilísticos, es necesario incorporar nuevos parámetros en las técnicas formales que hagan referencia a estos aspectos.

Aunque las principales aplicaciones de las técnicas formales son el modelado y verificación, pueden encontrarse nuevos campos en los se demuestra su utilidad. En concreto, el problema de la síntesis automática puede abordarse desde el punto de vista de las técnicas formales. Por ejemplo, la técnica de model checking puede verse como un método de búsqueda exhaustiva automática de estados, o secuencias de estados, que satisfacen una propiedad, la cual puede interpretarse como un objetivo. En este caso, las técnicas formales pueden proporcionar nuevas soluciones a problemas, como es el caso de la síntesis de controladores y la optimización, que se han abordado desde otras perspectivas. En esta misma línea, la aparición de nuevos escenarios de aplicación software, como es la ya mencionada adaptación automatizada de componentes, en el contexto de los servicios software, puede resolverse mediante el uso no estándar de técnicas formales existentes, o definiendo nuevos marcos formales que permitan la construcción correcta de adaptadores software.

El presente proyecto tiene dos objetivos técnicos. Por un lado, mejorar la calidad del software, que puede contener componentes continuas, y factores de incertidumbre, extendiendo la técnica de model checking de forma apropiada: mediante la definición de nuevos lenguajes de modelado, que sean capaces de describir las nuevas características; mediante la extensión de los algoritmos de model checking, para que tengan en cuenta los aspectos continuos y de probabilidad; y mediante la extensión de herramientas de model checking existentes que implementen estas propuestas.

Por otro lado, el segundo objetivo técnico es el estudio de nuevas aplicaciones no estándares del model checking en el contexto de la síntesis y optimización de controladores y adaptadores software, así como el desarrollo de nuevos marcos formales que resuelvan el problema de la adaptación dinámica del software para la recepción correcta de servicios por parte de usuarios.

Este proyecto se plantea como un proyecto motriz cuya relevancia para el sector industrial andaluz queda patente por las cartas de apoyo de las empresas que se adjuntan al documento. La empresa AT4 wireless colaborará en el proyecto en la modalidad de subcontratación para desarrollar parte de la infraestructura de certificación de servicios y protocolos para redes LTE. La empresa ADIF (Administrador de Infraestructuras Ferroviarias) hará el seguimiento de los trabajos en los sistemas de control ferroviario, y facilitará al grupo el uso de su Laboratorio TIC en el Centro de Tecnologías Ferroviarias de Málaga. La empresa Novasoft está interesada en los desarrollos relativos a la generación de adaptadores dinámicos de servicios. Y la empresa Vodafone realizará el seguimiento de los resultados en el campo de la telefonía móvil.

 

Summary

Computer systems are gradually replacing tasks that due to its critical nature have been conducted manually. This explosion of new applications has been possible thanks to the improvement of hardware devices that eventually automate processes, and the development of the software industry that has produced new intermediate and high level programming technologies, with a much greater expressive power, able to solve problems of great magnitude.

Simultaneous with this growth in demand for software services, we have developed the so-called formal techniques that aim to improve the quality and reliability of the software that is provided to the user. These techniques make use of mathematical language to minimize the number of errors, ensuring that the software meets a set of properties that are considered critical to its scope. Although initially, the use of formal techniques was criticized for its dubious practical application, today, its use is widely accepted, so that the development of any product is usually accompanied by his modeling and / or analysis by any formal technique. This is due mainly to the development of modeling techniques and powerful analysis and tools that support these techniques and have been proven extensively its usefulness in practice.

Perhaps the method known as model checking is the most influential in the progressive integration of formal techniques in software development, software fundamentally concurrent or distributed. The ubiquity of model checking and its apparent success at industrial level is because a balanced way mathematical formalization, and properties of both software system to be analyzed, and practicality, since the model checking is an algorithmic technique aimed at building tools to carry out automatically the complex task of software verification.

The current trend in the formal techniques area is thus finding new formalism, or extension of existing, considering different aspects of the software that classically have not been considered. For example, most of the systems listed in the real world are not completely discrete but have some component, usually associated with a physical device which acts continuously. Such systems are called hybrids, and are characterized at times behave discreetly, while in others, evolve through continuous dynamics (uncountable). Another interesting aspect of real systems is that in many instances, have a random behavior, so that incorporate some uncertainty parameter, having a function that defines probabilistic evolution. To model and analyze hybrid and / or probabilistic systems, it is necessary to incorporate new techniques in formal parameters that refer to these aspects.

Although the main applications of the techniques are formal modeling and verification, it can be found that in new fields demonstrated its usefulness. Specifically, the problem of automated synthesis may be approached from the standpoint of formal techniques. For example, the model checking techniques can be seen as an automated and exhaustive search method of states that satisfy a property which can be interpreted as a target. In this case, the formal techniques can provide new solutions to problems, such as the controlled synthesis and optimization have been addressed from other perspectives. Along the same lines, the emergence of new software application scenarios, such as the aforementioned automated component adaptation, in the context of software services can be solved by using standard not existing formal techniques, or defining new formal frameworks allow the construction of software adapters correct.

This project has two technical objectives. On the one hand, improve software quality, which may contain continuous components, and uncertainties, extending the model checking technique appropriately: by defining new modeling languages, which are able to describe the new features, using the extension of model checking algorithms, to take into account the continuous and probability, and by extending existing model checking tools to implement these proposals.

On the other hand, the second technical objective is the study of new non-standard applications of model checking in the context of the synthesis and optimization of software drivers and adapters, as well as the development of new formal frameworks that solve the problem of dynamic adaptation software for correct reception of services by users.

This project is proposed as a driving project whose relevance to Andalusian industrial sector is evidenced by the letters of support from companies that are attached to the document. The company AT4 wireless will work on the project in the form of subcontracting to develop part of the certification infrastructure services and protocols for LTE networks. The company ADIF (Railway Infrastructure Administrator) will monitor the work on railway control systems and provide the group using their TIC Railway Technology Center of Malaga. The company NOVASOFT is interested in the developments relating to the dynamic generation of service adapters. And the company Vodafone will track the results in the field of mobile telephony.

 

Proyecto financiado por

Documento de la Propuesta