RT Conference Proceedings
T1 QMaude: Quantitative Specification and Verification in Rewriting Logic
A1 Rubio Cuéllar, Rubén Rafael
A1 Martí Oliet, Narciso
A1 Pita Andreu, María Isabel
A1 Verdejo López, José Alberto
A2 Chechik, Marsha
A2 Katoen, Joost-Pieter
A2 Leucker, Martin
AB 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.
SN 978-3-031-27480-0
SN 978-3-031-27481-7
SN 0302-9743
YR 2023
FD 2023
LK https://hdl.handle.net/20.500.14352/101033
UL https://hdl.handle.net/20.500.14352/101033
LA eng
NO Rubio, R., Martí-Oliet, N., Pita, I., Verdejo, A. (2023). QMaude: Quantitative Specification and Verification in Rewriting Logic. In: Chechik, M., Katoen, JP., Leucker, M. (eds) Formal Methods. FM 2023. Lecture Notes in Computer Science, vol 14000. Springer, Cham. https://doi.org/10.1007/978-3-031-27481-7_15
NO Ministerio de Ciencia e Innovación (España) 
NO Ministerio de Universidades (España)
DS Docta Complutense
RD 6 abr 2025