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.