Resumen:
Existe consenso en la comunidad académica y de ingenieros de software que es fundamental entender, modelar y describir el comportamiento del software complejo desde etapas tem-pranas del desarrollo. El paradigma de descripción declarativa, basado en el modelado de las propiedades y objetivos esenciales de los objetos y agentes, posee características especial-mente prometedoras para este tipo de desafíos. Sin embargo, las alternativas existentes en este paradigma son lógicas temporales que poseen limitaciones prácticas y teóricas. Asimis-mo, la verificación formal de propiedades sigue siendo en la actualidad uno de los mayores desafíos para la transferencia de tecnología de verificación de software como model checking. Los usuarios de estas técnicas deben enfrentar el desafío de expresar propiedades en el lenguaje formal usado en la herramienta de especificación. Dos de las aproximaciones más utilizadas son lógicas temporales como LTL, y notaciones operacionales basadas en autóma-tas. Ambas aproximaciones requieren usuarios “expertos” o con conocimientos avanzados para poder expresar, describir y validar la propiedad de interés. Todo esto indica la necesidad de contar con un lenguaje formal declarativo para expresar propiedades, que sea lo suficien-temente expresivo y que permita realizar tareas de validación de manera simple e intuitiva. En esto contexto, el objetivo global de esta tesis fue elaborar un enfoque de modelado declarativo, capaz de manejar distintos niveles de abstracción, con semántica precisa y clara, para modelar el comportamiento de sistemas reactivos. El objetivo específico fue el desarrollo de un lenguaje de modelado declarativo, basado en notaciones gráficas (escenarios), capaz de modelar y describir el comportamiento de sistemas reactivos. El lenguaje posee una semántica y sintaxis clara y precisa, con la posibilidad de realizar razonamiento automático, modelado incremental, y validación intuitiva de propiedades.
