Explora I+D+i UPV

Volver atrás Servicio de I+D

Técnicas y herramientas para la verificación y certificación de la terminación de programas

Institut Universitari Valencià d'investigació en Intel·ligència Artificial

Imprimir
Compartir
¿Quieres contarnos tu reto? Pincha aquí y te ayudamos a encontrar una solución
Uno de los problemas prácticos más interesantes desde el punto de vista científico y tecnológico es el de la terminación de los programas y sistemas de cómputo. Cuando un programa no es terminante, esta circunstancia se manifiesta en el sistema software que lo ejecuta (por lo general sin que el usuario sea consciente de que su origen reside en este tipo de error) en forma de bloqueos del sistema que exigen reiniciarlo, total o parcialmente. En este sentido, la verificación automática de propiedades de terminación es de claro interés industrial. La utilización de conceptos, métodos y técnicas procedentes de la programación basada en reglas en la construcción, análisis y verificación de software y sistemas de cómputo, cuenta ya con una larga historia, aunque sigue gozando de considerable popularidad y en los últimos años ha recibido un renovado interés procedente de distintas áreas de la ingeniería informática. En este campo, hemos desarrollado nuevas técnicas que son de aplicación a la verificación y certificación de propiedades de terminación de programas y sistemas computacionales: órdenes, métodos algebraicas, utilización de lógicas y algoritmos asociados, resolución de restricciones aritméticas, transformaciones, etc. Esta tecnología ha sido implementada en diversas herramientas que pueden utilizarse mediante interfaces basadas en servicios web.
Responsable científico

Lucas Alba Salvador

Participantes

Gutiérrez Gil Raúl, Alarcón Jiménez Beatriz, Navarro Marset Rafael Andrés, Lucas Alba Salvador

Aplicaciones

  • Verificación y certificación de la terminación de distintas variantes de sistemas basados en reglas.
  • Verificación y certificación de la terminación de programas Maude.
  • Resolución eficiente de restricciones aritméticas. //
  • Verification and certification of termination of different kinds of rule-based systems.
  • Verification and certification of termination of Maude programs.
  • Efficient resolution of arithmetic constraints.

Ventajas técnicas

  • Técnicas y herramientas desarrolladas sobre bases formales sólidas. // Techniques and tools developed on a solid formal basis.

Beneficios que aporta

  • Verificación y certificación automática de la terminación de programas y sistemas de cómputo.
  • Resolución automática de restricciones aritméticas. // Automatic verification and certification of termination properties of programs and computational systems. Efficient resolution of arithmetic constraints.

Experiencia relevante

  • El grupo ELP, creado en 1989, está identificado en el registro de grupos de investigacion consolidados de la Generalitat Valenciana desde Octubre de 2000 (clave GR-00143). La actividad del grupo se ha relacionado principalmente con los lenguajes de programación multiparadigma y los métodos rigurosos para el desarrollo del software, focalizando en la programación basada en reglas y el uso de técnicas de interpretación abstracta y técnicas de transformación para la optimización de la ejecución de los programas. Los lenguajes basados en reglas han sido también la base para la programación inductiva y para la representación de modelos complejos, pero a su vez, comprensibles, resultantes de la extracción de conocimiento a partir de datos (minería de datos). El grupo ELP ha participado en más de 30 proyectos competitivos financiados con fondos europeos, nacionales y comunitarios. Su actividad investigadora se ha desarrollado a menudo en conexión con grupos afines radicados en universidades extranjeras, incluyendo Alemania (RWTH Aachen, U. de Kiel), Australia (Monash U.), Austria (Technische Universitat Wien), Estados Unidos (U. of Illinois at Urbana-Champaign, National Research Laboratory, Portland State U., Washington, Stanford), Francia (-'Ecole Polytechnique, U. Grenoble, U. Niza, U. de Paris Sud), Italia (U. di Pisa, U. di Siena, U. di Udine) y Reino Unido (U. Bristol). El grupo ha participado en diversos proyectos con empresas donde se ha transferido el conocimiento del grupo o se ha desarrollado tecnología específica. El abanico de sectores en los que el grupo ha trabajado incluye, lógicamente, empresas de informática y consultoría, pero también empresas que van desde del ámbito de la distribución a la gestión hospitalaria. // The group ELP, created in 1989, was recognized as a consolidated group of the Valencian Government in October 2000 (reference GR-00143). The group's activities have mainly focused on multi-paradigm programming languages and rigurous methods for software development, with particular focus on rule--based programming, and the use of abstract interpretation and program transformation techniques for the optimization of program execution. Rule-based languages have been also used for inductive programming and complex model representation that are also comprehensible as a result of knowledge discovering (data mining). The ELP group has participated in more than 30 competitive research projects funded by the EU, the Spanish Research Funding Agency, and other European foundations. The group keeps a good record of international collaborations. Including Germany (RWTH Aachen, U. Kiel), Australia (Monash U.), Austria (Technische Universit-"at Wien), USA (U. of Illinois at Urbana-Champaign, National Research Laboratory, Portland State U., Washington, Stanford), France (-'Ecole Polytechnique, U. Grenoble, U. Niza, U. Paris Sud), Italy (U. di Pisa, U. di Siena, U. di Udine) and UK (U. Bristol). The Group also keeps a good record of collaboration with industry, including IT companies as well as hospital management and distribution companies.