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

Simple item page
dc.contributor.advisorRocha Niño, Hernán Camilo
dc.contributor.authorOsorio Valencia, Daniel Fabian
dc.date.accessioned2024-06-14T16:35:41Z
dc.date.available2024-06-14T16:35:41Z
dc.date.issued2023
dc.description.abstractengComputer 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.
dc.format.extent81 p.
dc.format.mimetypeapplication/pdf
dc.identifier.urihttps://vitela.javerianacali.edu.co/handle/11522/2564
dc.language.isoeng
dc.publisherPontificia Universidad Javeriana Cali
dc.rights.accessrightshttp://purl.org/coar/access_right/c_abf2
dc.rights.creativecommonshttps://creativecommons.org/licenses/by-nc-nd/4.0/
dc.rights.urihttps://creativecommons.org/licenses/by-nc-nd/4.0/
dc.thesis.disciplineFacultad de Ingeniería y Ciencias. Ingeniería de Sistemas y Computación
dc.thesis.grantorPontificia Universidad Javeriana Cali
dc.thesis.levelPregrado
dc.thesis.nameIngeniero de Sistemas y Computación
dc.titleEventB2Maude : probabilistic modeling and statistical model checking for event-B with probabilistic rewrite theories and MultiVeStAeng
dc.type.coarhttp://purl.org/coar/resource_type/c_7a1f
dc.type.localTesis/Trabajo de grado - Monografía - Pregrado
dc.type.redcolhttps://purl.org/redcol/resource_type/TP
Files
Original bundle
Now showing 1 - 3 of 3
Thumbnail Image
Name:
EventB2Maude.pdf.pdf
Size:
1.45 MB
Format:
Adobe Portable Document Format
Download
Thumbnail Image
Name:
Articulo_cientifico.pdf
Size:
247.52 KB
Format:
Adobe Portable Document Format
Download
No Thumbnail Available
Name:
Licencia_autorizacion.pdf
Size:
193.51 KB
Format:
Adobe Portable Document Format
Download
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
1.71 KB
Format:
Item-specific license agreed to upon submission
Description:
Download
Collections
Ingeniería de Sistemas y Computación