EventB2Maude : probabilistic modeling and statistical model checking for event-B with probabilistic rewrite theories and MultiVeStA

Computer based systems increase every day in complexity. This tendency demands more modeling and verification features from formal methods, in order to mathematically proof properties over these systems. One of these formal methods is Event-B, which has been extended in order to cope with probabilistic behavior. In order to contribute to the verification of probabilistic Event-B models, in this work a rewriting logic semantics for probabilistic Event-B has been proposed, and it allows to encode these models as probabilistic rewrite theories in PMaude. The encoding, implemented as the EventB2Maude tool, opens the door for new statistical model checking tools like MultiVeStA to be used over probabilistic Event-B specifications. Therefore, this work presents an integration between the EventB2Maude tool and MultiVeStA. Additionally, an introductory guide for using MultiVeStA with PMaude is also given. Finally, some case studies are presented to show how the integration works and validate that the integration was done correctly, by comparing the obtained results of the simulations with their expected value.

• Autores: Osorio Valencia, Daniel Fabian
• Tipo de recurso: Trabajo de grado de pregrado
• Fecha de publicación: 2023
• Institución: Pontificia Universidad Javeriana Cali
• Repositorio: Vitela
• Idioma: eng
• OAI Identifier: oai:vitela.javerianacali.edu.co:11522/2564
• Acceso en línea: https://vitela.javerianacali.edu.co/handle/11522/2564
• License: https://creativecommons.org/licenses/by-nc-nd/4.0/