Rubio Cuéllar, Rubén RafaelMartí Oliet, NarcisoPita Andreu, María IsabelVerdejo López, José AlbertoChechik, MarshaKatoen, Joost-PieterLeucker, Martin2024-02-092024-02-092023Rubio, 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_15978-3-031-27480-0978-3-031-27481-70302-974310.1007/978-3-031-27481-7_15https://hdl.handle.net/20.500.14352/101033In 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.engAttribution-NonCommercial-NoDerivatives 4.0 Internationalhttp://creativecommons.org/licenses/by-nc-nd/4.0/conference paperrestricted accessRewriting logicProbabilistic model checkingStatistical model checkingMaudeLenguajes de programaciónLógica simbólica y matemática (Matemáticas)Probabilidades (Matemáticas)1203.23 Lenguajes de Programación1102.14 Lógica Simbólica1208.03 Aplicación de la Probabilidad