Modelado y verificación de programas Event-B usando Maude

Abstract

[ES] La mayoría de herramientas de modelado en Ingeniería del Software carecen de mecanismos de verificación de propiedades basados en métodos formales, aunque existen muchas alternativas que incluyen métodos formales ligeros (que no requieren aprender formalismos matemáticos complejos para el modelado). La propuesta líder en Europa es el lenguaje Event-B, soportado por la plataforma Rodin. Event-B es una extensión del lenguaje B, desarrollado en la década de los 90. Diversas compañías europeas como SAP, RATP (Ferrocarril Francia), Systérel o innoQ utilizan Event-B desde hace años para diseñar sus sistemas. El lenguaje Event-B utiliza métodos formales internamente pero queda mucho trabajo por realizar para integrar dichos métodos de una forma simple que potencie la eficiencia. Actualmente muchas herramientas para Event-B traducen programas Event-B a programas Java o Prolog pero nadie ha definido la semántica de Event-B de forma rigurosa. El objetivo de esta tesis de máster es estudiar y comprender la semántica de los modelos descritos en Event-B y vislumbrar un mecanismo de traducción de programas de Event-B al lenguaje Maude.