QMaude: Quantitative Specification and Verification in Rewriting Logic

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.
Agencia Estatal de Investigación
Ministerio de Universidades
Depto. de Sistemas Informáticos y Computación
Fac. de Informática
TRUE
pub