Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

QMaude: Quantitative Specification and Verification in Rewriting Logic

  • Conference paper
  • First Online:
Formal Methods (FM 2023)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 14000))

Included in the following conference series:

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    When the system is controlled by a strategy, the Kripke structure is refined as explained in [46, 48].

  2. 2.

    The results and the scripts to reproduce them are available at maude.ucm.es/qmaude.

  3. 3.

    PVesta is not included in the comparison because its actual convergence criterion differs from the one explained in its paper [2] and used by MultiVeSta and scheck.

References

  1. Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. 28(1), 6:1-6:39 (2018). https://doi.org/10.1145/3158668

    Article  MathSciNet  Google Scholar 

  2. Agha, G.A., Meseguer, J., Sen, K.: PMaude: rewrite-based specification language for probabilistic object systems. In: Cerone, A., Wiklicky, H. (eds.) Proceedings of the Third Workshop on Quantitative Aspects of Programming Languages, QAPL 2005, Edinburgh, UK, 2–3 April 2005. Electronic Notes in Theoretical Computer Science, vol. 153, no. 2, pp. 213–239. Elsevier (2006). https://doi.org/10.1016/j.entcs.2005.10.040

  3. Alpuente, M., Ballis, D., Sapiña, J.: Static correction of Maude programs with assertions. J. Syst. Softw. 153, 64–85 (2019). https://doi.org/10.1016/j.jss.2019.03.061

    Article  Google Scholar 

  4. AlTurki, M., Meseguer, J.: PVeStA: a parallel statistical model checking and quantitative analysis tool. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 386–392. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22944-2_28

    Chapter  Google Scholar 

  5. Alturki, M.A., Kanovich, M.I., Kirigin, T.B., Nigam, V., Scedrov, A., Talcott, C.L.: Statistical model checking of distance fraud attacks on the Hancke-Kuhn family of protocols. In: Lie, D., Mannan, M. (eds.) CPS-SPC 2018, pp. 60–71. ACM (2018). https://doi.org/10.1145/3264888.3264895

  6. Alturki, M.A., Roşu, G.: Statistical model checking of RANDAO’s resilience to pre-computed reveal strategies. In: Sekerinski, E., et al. (eds.) FM 2019. LNCS, vol. 12232, pp. 337–349. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-54994-7_25

    Chapter  Google Scholar 

  7. Andrei, O., Fernández, M., Kirchner, H., Melançon, G., Namet, O., Pinaud, B.: PORGY: strategy-driven interactive transformation of graphs. In: Echahed, R. (ed.) Proceedings 6th International Workshop on Computing with Terms and Graphs, TERMGRAPH 2011, Saarbrücken, Germany, 2nd April 2011. EPTCS, vol. 48, pp. 54–68 (2011). https://doi.org/10.4204/EPTCS.48.7

  8. Baier, C., de Alfaro, L., Forejt, V., Kwiatkowska, M.: Model checking probabilistic systems. In: Handbook of Model Checking, pp. 963–999. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-10575-8_28

    Chapter  MATH  Google Scholar 

  9. Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  10. Bentea, L., Ölveczky, P.C.: A probabilistic strategy language for probabilistic rewrite theories and its application to cloud computing. In: Martí-Oliet, N., Palomino, M. (eds.) WADT 2012. LNCS, vol. 7841, pp. 77–94. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37635-1_5

    Chapter  Google Scholar 

  11. Bournez, O., Kirchner, C.: Probabilistic rewrite strategies. applications to ELAN. In: Tison, S. (ed.) RTA 2002. LNCS, vol. 2378, pp. 252–266. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45610-4_18

    Chapter  MATH  Google Scholar 

  12. Budde, C.E., Dehnert, C., Hahn, E.M., Hartmanns, A., Junges, S., Turrini, A.: JANI: quantitative model and tool interaction. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 151–168 (2017). https://doi.org/10.1007/978-3-662-54580-5_9

  13. Clavel, M., et al.: Maude Manual v3.2.1 (2022). http://maude.lcc.uma.es/maude321-manual-html/maude-manual.html

  14. Clavel, M., et al.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71999-1

    Book  MATH  Google Scholar 

  15. Clavel, M., Palomino, M., Riesco, A.: Introducing the ITP tool: a tutorial. J. Univers. Comput. Sci. 12(11), 1618–1650 (2006). https://doi.org/10.3217/jucs-012-11-1618

    Article  Google Scholar 

  16. Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A storm is coming: a modern probabilistic model checker. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592–600. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63390-9_31

    Chapter  Google Scholar 

  17. Dijkstra, E.W.: On the Role of Scientific Thought, pp. 60–66. Texts and Monographs in Computer Science, Springer (1982). https://doi.org/10.1007/978-1-4612-5695-3_12

  18. Durán, F., Rocha, C., Álvarez, J.M.: Tool interoperability in the Maude formal environment. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 400–406. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22944-2_30

    Chapter  Google Scholar 

  19. Durán, F., et al.: Programming and symbolic computation in Maude. J. Log. Algebraic Methods Program. 110, 100497 (2020). https://doi.org/10.1016/j.jlamp.2019.100497

    Article  MathSciNet  MATH  Google Scholar 

  20. Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker. In: Gadducci, F., Montanari, U. (eds.) Proceedings of the Fourth International Workshop on Rewriting Logic and its Applications, WRLA 2002, Pisa, Italy, 19–21 September 2002. Electronic Notes in Theoretical Computer Science, vol. 71, pp. 162–187. Elsevier (2004). https://doi.org/10.1016/S1571-0661(05)82534-4

  21. Ellison, C., Rosu, G.: An executable formal semantics of C with applications. In: Field, J., Hicks, M. (eds.) Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, 22–28 January 2012, pp. 533–544. ACM (2012). https://doi.org/10.1145/2103656.2103719

  22. FaDoSS: Examples of the Maude strategy language (2022). https://fadoss.github.io/strat-examples

  23. Garavel, H., Tabikh, M.-A., Arrada, I.-S.: Benchmarking implementations of term rewriting and pattern matching in algebraic, functional, and object-oriented languages. In: Rusu, V. (ed.) WRLA 2018. LNCS, vol. 11152, pp. 1–25. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-99840-4_1

    Chapter  Google Scholar 

  24. González-Burgueño, A., Aparicio-Sánchez, D., Escobar, S., Meadows, C.A., Meseguer, J.: Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA. In: Barthe, G., Sutcliffe, G., Veanes, M. (eds.) LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, 16–21 November 2018. EPiC Series in Computing, vol. 57, pp. 400–417. EasyChair (2018). https://doi.org/10.29007/c4xk

  25. Gordon, A.D., Henzinger, T.A., Nori, A.V., Rajamani, S.K.: Probabilistic programming. In: Herbsleb, J.D., Dwyer, M.B. (eds.) FOSE 2014, pp. 167–181. ACM (2014). https://doi.org/10.1145/2593882.2593900

  26. Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6(5), 512–535 (1994). https://doi.org/10.1007/BF01211866

    Article  MATH  Google Scholar 

  27. IETF: Hypertext Transfer Protocol version 2 (HTTP/2). RFC 7540, RFC Editor (2015). https://www.rfc-editor.org/rfc/rfc7540.txt

  28. IETF: HTTP/3. RFC 9114, RFC Editor (2022). https://www.rfc-editor.org/rfc/rfc9114.txt

  29. Knuth, D.E., Yao, A.C.: The complexity of nonuniform random number generation. In: Traub, J.F. (ed.) Algorithms and Complexity: New Directions and Recent Results, pp. 357–428. Academic Press (1976)

    Google Scholar 

  30. Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol. 4486, pp. 220–270. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-72522-0_6

    Chapter  Google Scholar 

  31. Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_47

    Chapter  Google Scholar 

  32. Lee, D., Carpenter, B., Li, P., et al.: Stan (2017). https://doi.org/10.5281/zenodo.1101116

  33. Liu, S., Ölveczky, P.C., Zhang, M., Wang, Q., Meseguer, J.: Automatic analysis of consistency properties of distributed transaction systems in Maude. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 40–57. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17465-1_3

    Chapter  Google Scholar 

  34. MathWorks: MATLAB R2022a. The MathWorks Inc., Natick, Massachusetts (2022)

    Google Scholar 

  35. Meseguer, J.: Twenty years of rewriting logic. J. Log. Algebr. Program. 81(7–8), 721–781 (2012). https://doi.org/10.1016/j.jlap.2012.06.003

    Article  MathSciNet  MATH  Google Scholar 

  36. Meseguer, J., Sasse, R., Wang, H.J., Wang, Y.: A systematic approach to uncover security flaws in GUI logic. In: 2007 IEEE Symposium on Security and Privacy (S &P 2007), Oakland, California, USA, 20–23 May 2007, pp. 71–85. IEEE Computer Society (2007). https://doi.org/10.1109/SP.2007.6

  37. Ölveczky, P.C.: Real-time Maude and its applications. In: Escobar, S. (ed.) WRLA 2014. LNCS, vol. 8663, pp. 42–79. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-12904-4_3

    Chapter  Google Scholar 

  38. Pappagallo, A., Massini, A., Tronci, E.: Monte Carlo based statistical model checking of cyber-physical systems: a review. Information 11(12), 588 (2020). https://doi.org/10.3390/info11120588

    Article  Google Scholar 

  39. Riesco, A., Verdejo, A., Martí-Oliet, N., Caballero, R.: Declarative debugging of rewriting logic specifications. J. Log. Algebraic Methods Program. 81(7–8), 851–897 (2012). https://doi.org/10.1016/j.jlap.2011.06.004

    Article  MathSciNet  MATH  Google Scholar 

  40. Rocha, C., Cadavid, H., Muñoz, C., Siminiceanu, R.: A formal interactive verification environment for the plan execution interchange language. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol. 7321, pp. 343–357. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-30729-4_24

    Chapter  Google Scholar 

  41. Rubio, R.: Language bindings for Maude (2021). https://fadoss.github.io/maude-bindings

  42. Rubio, R.: Maude simulator for MultiVeSta (2021). https://github.com/fadoss/multivesta-maude

  43. Rubio, R.: Maude as a library: an efficient all-purpose programming interface. In: Bae, K. (ed.) WRLA 2022. LNCS, vol. 13252, pp. 274–294. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-12441-9_14

  44. Rubio, R.: An overview of the Maude strategy language and its applications. In: Bae, K. (ed.) WRLA 2022. LNCS, vol. 13252, pp. 65–84. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-12441-9_4

  45. Rubio, R.: Unified Maude model-checking tool (2022). https://github.com/fadoss/umaudemc

  46. Rubio, R., Martí-Oliet, N., Pita, I., Verdejo, A.: Model checking strategy-controlled systems in rewriting logic. Autom. Softw. Eng. 29(1), 1–62 (2021). https://doi.org/10.1007/s10515-021-00307-9

    Article  MATH  Google Scholar 

  47. Rubio, R., Martí-Oliet, N., Pita, I., Verdejo, A.: The semantics of the Maude strategy language. Tech. rep. 01/21, Departamento de Sistemas Informáticos y Computación, Universidad Complutense de Madrid (2021).https://eprints.ucm.es/67449/

  48. Rubio, R., Martí-Oliet, N., Pita, I., Verdejo, A.: Strategies, model checking and branching-time properties in Maude. J. Log. Algebr. Methods Program. 123, 100700 (2021). https://doi.org/10.1016/j.jlamp.2021.100700

    Article  MathSciNet  MATH  Google Scholar 

  49. Rubio, R., Riesco, A.: Theorem proving for Maude specifications using Lean. In: Zhang, M., Riesco, A. (eds.) Formal Methods and Software Engineering. ICFEM 2022. LNCS, vol. 13478, pp. 263–280. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-17244-1_16

  50. Salvatier, J., Wiecki, T.V., Fonnesbeck, C.: Probabilistic programming in Python using PyMC3. PeerJ Comput. Sci. 2, e55 (2016). https://doi.org/10.7717/peerj-cs.55

    Article  Google Scholar 

  51. Sebastio, S., Vandin, A.: MultiVeStA: statistical model checking for discrete event simulators. In: Horváth, A., Buchholz, P., Cortellessa, V., Muscariello, L., Squillante, M.S. (eds.) 7th International Conference on Performance Evaluation Methodologies and Tools, ValueTools 2013, Torino, Italy, 10–12 December 2013, pp. 310–315. ICST/ACM (2013). https://doi.org/10.4108/icst.valuetools.2013.254377

  52. Shankesi, R., AlTurki, M., Sasse, R., Gunter, C.A., Meseguer, J.: Model-checking DoS amplification for VoIP session initiation. In: Backes, M., Ning, P. (eds.) ESORICS 2009. LNCS, vol. 5789, pp. 390–405. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04444-1_24

    Chapter  Google Scholar 

  53. Spedicato, G.A.: Discrete time Markov chains with R. R J. 9(2), 84 (2017). https://doi.org/10.32614/rj-2017-036

Download references

Acknowledgments

Research partially supported by the Spanish AEI through project ProCode (PID2019-108528RB-C22/AEI/10.13039/501100011033). Rubén Rubio was partially supported by the Spanish Ministry of Universities through grants FPU17/02319 and EST21/00536.

Author information

Authors and Affiliations

  1. Facultad de Informática, Universidad Complutense de Madrid, Madrid, Spain

    Rubén Rubio, Narciso Martí-Oliet, Isabel Pita & Alberto Verdejo

Authors
  1. Rubén Rubio
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Narciso Martí-Oliet
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Isabel Pita
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Alberto Verdejo
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Rubén Rubio .

Editor information

Editors and Affiliations

  1. University of Toronto, Toronto, ON, Canada

    Marsha Chechik

  2. RWTH Aachen University, Aachen, Germany

    Joost-Pieter Katoen

  3. University of Lübeck, Lübeck, Germany

    Martin Leucker

Rights and permissions

Reprints and permissions

Copyright information

© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

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

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-27481-7_15

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-27480-0

  • Online ISBN: 978-3-031-27481-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation