Especificación y verificación avanzada de software

En la actual "Sociedad de la Información" cada vez hay más tareas realizadas de forma automática o semi-automática por productos software. Más aún, una parte de dichas tareas tienen requerimientos de seguridad críticos (por ejemplo, es posible asegurar que las transacciones entre cliente y servidor serán siempre privadas?; el proceso terminará siempre?, etc.). En este contexto, resulta crucial incorporar procesos que garanticen que el software desarrollado cumple una serie de requisitos. Para ello, se pueden usar métodos experimentales basados en testeo (los cuales no suelen poder asegurar al 100% que los requisitos se cumplen) o bien métodos de verificación formal basados en el uso de modelos, la incorporación de asertos en el código, etc. En este segundo caso, sí es posible conseguir una garantía total acerca de la corrección del software. En nuestro grupo, nos centramos en el uso de modelos basados en las "redes de Petri" para la especificación formal de determinados procesos (concretamente, son especialmente adecuadas para formalizar tareas que involucren concurrencia, comunicación entre procesos, sincronización, etc). La principal ventaja de usar dichos modelos formales es que existe un buen número de herramientas software que permiten su análisis y verificación de forma semi-automática. Otra tecnología empleada en el grupo se basa en el uso de JML (Java Modelling Language), un lenguaje para la definición de asertos que se incorporan en los programas Java y permiten testear diferentes propiedades de los mismos (bien en tiempo de ejecución o de forma estática). Por ejemplo, JML puede emplearse para incluir asertos sobre condiciones de seguridad en software crítico, de forma que si las condiciones se violan, la ejecución del código se aborte.

Aplicaciones

  • Las técnicas formales de especificación permiten detectar errores en las fases iniciales del desarrollo de software, disminuyendo así considerablemente el elevado coste de eliminar los errores en la fase de explotación.
  • Por otro lado, las técnicas de verificación basadas en JML pueden contribuir significativamente a mejorar la calidad del software y a certificar, en algunos casos, que éste cumple determinados requisitos sobre su funcionamiento, seguridad, etc.

Ventajas técnicas

  • Las técnicas formales tienen una serie de ventajas indudables con respecto a las técnicas más tradicionales basadas en testeo y experimentación, ya que permiten "certificar" (en algunos casos con una fiabilidad del 100%) que el software desarrollado cumple con una serie de requisitos (de seguridad, de terminación...).

Beneficios que aporta

  • Software más fiable y certificado
  • Muchas de las técnicas mencionadas tienen un coste de aplicación muy bajo (por ejemplo, la inclusión de asertos JML en aplicaciones Java puede realizarse por parte de los propios programadores de forma sencilla).

Experiencia relevante

  • Desde su creación, el grupo está orientado al desarrollo de técnicas relacionadas con las temáticas tratadas aquí, lo que viene avalado por el número y calidad de las publicaciones de los miembros del equipo, así como por los proyectos de I+D+i en los que hemos participado.