Abstract
\(\textsf {P}\) is a programming language equipped with a unified framework for modeling, specifying, implementing, testing, and verifying complex distributed systems. This language is based on the actor model, and its framework includes a compiler toolchain for code generation, bounded randomized testing, and reachability analysis. This paper presents an extension of \(\textsf {P}\)’s framework to include statistical model checking of quantititive temporal logic formulas. The distributed statistical model checking for discrete event simulators \(\textsf {MultiVeStA}\) has been integrated into the P framework for Monte Carlo validation of \(\textsf {P}\) programs against \(\textsf {QuaTEx}\) quantitative temporal logic formulas. For this, \(\textsf {P}\)’s compiler has been modified to generate instrumentation code enabling the observation of a program’s attributes without direct, manual intervention of the code. As a result, distributed incremental statistical model checking is now available for \(\textsf {P}\) via probabilistic sampling. As the experiments show, some of them reported here, these new verification capabilities scale up and complement the ones already available for \(\textsf {P}\).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Agha, G., Meseguer, J., Sen, K.: PMaude: rewrite-based specification language for probabilistic object systems. Electron. Not. Theoret. Comput. Sci. 153(2), 213–239 (2006). Proceedings of the Third Workshop on Quantitative Aspects of Programming Languages (QAPL 2005)
Agha, G.A.: Actors: a Model of Concurrent Computation in Distributed Systems (Parallel Processing, Semantics, Open, Programming Languages, Artificial Intelligence). Ph.D. thesis, University of Michigan, USA (1985)
AlTurki, M., Meseguer, J., Gunter, C.A.: Probabilistic modeling and analysis of DoS protection for the ASV protocol. In: SecReT@LICS/CSF 2008, Electronic Notes in Theoretical Computer Science, vol. 234, pp. 3–18. Elsevier (2008)
Andrews, T., Qadeer, S., Rajamani, S.K., Rehof, J., Xie, Y.: Zing: a model checker for concurrent software. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 484–487. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27813-9_42
Deligiannis, P., Senthilnathan, A., Nayyar, F., Lovett, C., Lal, A.: Industrial-strength controlled concurrency testing for c# programs with coyote. In: Sankaranarayanan, S., Sharygina, N. (eds.) TACAS 2023. LNCS, vol. 13994, pp. 433–452. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-30820-8_26
Desai, A., Gupta, V., Jackson, E.K., Qadeer, S., Rajamani, S.K., Zufferey, D. : P: safe asynchronous event-driven programming. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013, Seattle, WA, USA, June 16–19, 2013, pp. 321–332. ACM (2013)
Eckhardt, J., Mühlbauer, T., Meseguer, J., Wirsing, M.: Statistical model checking for composite actor systems. In: Martí-Oliet, N., Palomino, M. (eds.) WADT 2012. LNCS, vol. 7841, pp. 143–160. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37635-1_9
Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker. In: WRLA2002, Electronic Notes in Theoretical Computer Science, vol. 71, pp. 162–187. Elsevier (2002)
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6(5), 512–535 (1994)
Hewitt, C., Bishop, P.B., Steiger, R.: A universal modular ACTOR formalism for artificial intelligence. In: Proceedings of the 3rd International Joint Conference on Artificial Intelligence, Standford, CA, USA, 20–23 August 1973, pp. 235–245. William Kaufmann (1973)
P Developers. P’s web site (2023). https://p-org.github.io/P/. Accessed 10 May 2023
Sebastio, S., Vandin, A.: Multivesta: statistical model checking for discrete event simulators. ValueTools 2013, pp. 310–315, Brussels, BEL, 2013. ICST (Institute for Computer Sciences, Social-Informatics and Telecommunications Engineering)
ter Beek, M.H., Legay, A., Lluch-Lafuente, A., Vandin, A.: Statistical analysis of probabilistic models of software product lines with quantitative constraints. In: Proceedings of the 19th International Conference on Software Product Line, SPLC 2015, Nashville, TN, USA, 20–24 July 2015, pp. 11–15. ACM (2015)
ter Beek, M.H., Legay, A., Lluch-Lafuente, A., Vandin, A.: A framework for quantitative modeling and analysis of highly (re)configurable systems. IEEE Trans. Software Eng. 46(3), 321–345 (2020)
Acknowledgments
The authors would like to thank D. Giannakopoulou and C. Muñoz for fruitful discussions on these ideas, and the anonymous referees for their very helpful comments that helped in improving the paper. This work was partially supported by Amazon Research Awards (Fall 2021) Project “Probabilistic and Symbolic Tools for P Program Verification”, and projects TED2021-130666B-I00 and PID2021-125527NB-I00 funded by the Spanish government.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Durán, F., Pozas, N., Ramírez, C., Rocha, C. (2023). Statistical Model Checking for \(\textsf {P}\). In: Cimatti, A., Titolo, L. (eds) Formal Methods for Industrial Critical Systems. FMICS 2023. Lecture Notes in Computer Science, vol 14290. Springer, Cham. https://doi.org/10.1007/978-3-031-43681-9_3
Download citation
DOI: https://doi.org/10.1007/978-3-031-43681-9_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-43680-2
Online ISBN: 978-3-031-43681-9
eBook Packages: Computer ScienceComputer Science (R0)