Verificación en Alloy de modelos y metamodelos específicos del dominio

Abstract

La verificación de modelos de sistemas de software es una actividad clave para mejorar la calidad del producto final. Numerosos lenguajes específicos del dominio han sido creados para favorecer la definición de modelos ajustados a un dominio o área particular. Sin embargo, la verificación de estos modelos, frecuentemente es dejada de lado como actividad complementaria al modelado. Esta línea de investigación, desarrollo e innovación se orienta a generalizar un mecanismo basado en Alloy, para la especificación y verificación de modelos y metamodelos específicos del dominio. Alloy es un lenguaje formal, soportado por una amigable herramienta de verificación y validación. Las características de Alloy pueden ser aprovechadas para establecer un enfoque que permita garantizar la calidad de los modelos de sistemas de software específicos.