Modelización y verificación automática de un proceso software

Abstract

En este artículo se presenta la modelización y verificación de los aspectos dinámicos y temporales de un proceso software convencional. La modelización de los aspectos dinámicos se representa mediante un metamodelo de diagramas de actividades de UML y la modelización de los aspectos temporales con un modelo de Red de Petri. Posteriormente se comprueban las propiedades funcionales y temporales con el lenguaje de lógica temporal CTL (Computational Tree Logic). Tanto para la modelización como para la verificación se utiliza AToM3, una herramienta que posibilita el metamodelado mediante la utilización de multiformalismos, y la verificación automática mediante técnicas de comprobación o model checking. En este trabajo ha sido posible analizar el comportamiento del proceso para determinar la coherencia y consistencia de las especificaciones efectuadas como resultado de los requerimientos del diseño, permitiendo detectar los posibles fallos del modelo y efectuar las correcciones correspondientes. Así mismo se destaca la importancia de contar con herramientas de metamodelación, multiformalismos y verificación integrados, como soportes fundamentales de apoyo a los métodos convencionales de análisis y diseño del proceso software.