Verificación automática del comportamiento activo de uml usando métodos formales

Abstract

El lenguaje unificado de modelado (UML) posee ventajas incuestionables como técnica visual de modelado, lo que ha hecho que su aplicación creciese rápidamente desde el momento de su nacimiento, A las características propias de UML hay que unirle que existen en el mercado numerosas herramientas que ayudan en su utilización (Rational Rose, Argo UML, Rhapsody ...) pero, desafortunadamente ninguna de ellas garantiza la corrección de la especificación. Sin embargo, está comúnmente aceptado que la detección errores en las fases tempranas del desarrollo reduce el coste y el tiempo de desarrollo de manera sustancial, ya que los errores detectados no son transmitidos ni amplificados en las fases posteriores. Por ello, sería de gran utilidad una herramienta que permitiese la integración de este método semi-formal de desarrollo con algún método formal que posibilite la verificación del sistema. En este trabajo se presenta una herramienta denominada TABU (Tool for Active Behaviour of UML) que realiza esta integración, proporcionando un marco formal para la verificación del comportamiento activo de UML. La herramienta realiza una transformación automática, completa y sin intervención del usuario, del comportamiento activo recogido en UML a una especificación en SMV, centrándose principalmente en sistemas reactivos. Para todo ello, utiliza como formato de entrada XMI (XML Metadata Interchange), lo que la hace independiente de la herramienta utilizada para la especificación del sistema. Por otro lado, la herramienta presenta un asistente versátil que guía al usuario en la escritura de propiedades a verificar, utilizando lógicas temporales. La verificación se realiza de manera que el usuario no necesite disponer de conocimientos ni de lenguajes formales, ni de lógicas temporales para aprovechar su potencia, algo que tradicionalmente ha supuesto un obstáculo difícil de superar a la hora de decidirse por el uso de méto