Resumen:
QMaude: quantitative specification and verification in rewriting logic

Fecha

2023-09-12

Editor

Sistedes

Publicado en

Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023)

Licencia Creative Commons

Resumen

In formal verification, qualitative and quantitative aspects are both relevant, and high-level formalisms are convenient to naturally specify the systems under study and their properties. In this paper, we present a framework for describing probabilistic models on top of nondeterministic specifications in the highly-expressive language Maude, based on rewriting logic. Quantitative properties can be checked and calculated on them using both probabilistic and statistical methods with external tools like PRISM, Storm, MultiVeSta, and custom implementations as backends. At the same time, the underlying nondeterministic system can be verified using the qualitative model-checking and deductive tools already available in Maude.

Descripción

Acerca de Rubio, Rubén

Palabras clave

Probabilistic Model Checking, Statistical Model Checking, Rewriting Logic, Maude
Página completa del ítem
Notificar un error en este resumen
Mostrar cita
Mostrar cita en BibTeX
Descargar cita en BibTeX