2026-06-01T10:35:51Zhttps://riuma.uma.es/rest/oai/request

oai:riuma.uma.es:10630/276532026-02-03T12:11:23Zcom_10630_2254col_10630_37959

Towards an Extensible Architecture and Tool Support for Model-based Verification. Delgado Camacho, David Eduardo Burgueño-Caballero, Lola Cámara-Moreno, Javier Troya-Castilla, Javier Ingeniería del software Soporte lógico - Verificación 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 verification is limited, and they usually require the cumbersome deployment of software burdened by dependencies, preventing the adoption of 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 structural domain 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. 2023-09-25T09:04:24Z 2023-09-25T09:04:24Z 2023-09-25T09:04:24Z 2023 conference output 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 https://hdl.handle.net/10630/27653 eng 20th Workshop on Model Driven Engineering, Verification and Validation (celebrado junto con 26th International Conference on Model Driven Engineering Languages and Systems (MODELS 2023)) Vasteras, Suecia 01/10/2023-06/10/2023 http://creativecommons.org/licenses/by-nc-nd/4.0/ open access Attribution-NonCommercial-NoDerivatives 4.0 Internacional