RT Conference Proceedings
T1 Towards an Extensible Architecture and Tool Support for Model-based Verification.
A1 Delgado Camacho, David Eduardo
A1 Burgueño-Caballero, Lola
A1 Cámara-Moreno, Javier
A1 Troya-Castilla, Javier
K1 Ingeniería del software
K1 Soporte lógico - Verificación
AB Model-based software engineering (MBSE) brings models to the center of software and system design. Models are powerful abstractions used to support all phases of the software development life cycle of complex software. As these models grow larger and their complexity increases, they need to be verified and validated to preserve their correctness. One possible way to do so is by means of the use of formal methods. However, the availability of MBSE tools with support for validation and verificationis limited, and they usually require the cumbersome deployment of software burdened by dependencies, preventing the adoptionof these tools. This paper presents a web-based architecture designed to support the definition of domain models and provide translation capabilities to different verification formalisms. As a proof of concept for our architecture, we have developed a tool prototype that is light-weight, runs in the browser and supports: (i) definition of domain models represented as class diagrams and (ii) partial translation of class diagrams into the Alloy specification language, enabling verification of structuraldomain properties. We show how we have used this tool to verify properties for the public bus management system in the city of Málaga, Spain.
YR 2023
FD 2023
LK https://hdl.handle.net/10630/27653
UL https://hdl.handle.net/10630/27653
LA eng
NO David Delgado, Lola Burgueño, Javier Cámara, Javier Troya. "Towards an Extensible Architecture and Tool Support for Model-based Verification" In Proc. of the 26th International Conference on Model Driven Engineering Languages and Systems Companion Proceedings. 2023
NO This work was partially funded by Universidad de Málaga (Campus Internacional de Excelencia), and the Spanish Government under projects PID2021-125527NB-I00 and TED2021-130523B-I00.Universidad de Málaga. Campus de Excelencia Internacional Andalucía Tech.
DS RIUMA. Repositorio Institucional de la Universidad de Málaga
RD 20 ene 2026