TY - GEN
T1 - Statistical Model Checking for P
AU - Durán, Francisco
AU - Pozas, Nicolás
AU - Ramírez, Carlos
AU - Rocha, Camilo
N1 - Publisher Copyright:
© 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.
PY - 2023
Y1 - 2023
N2 - 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 P ’s framework to include statistical model checking of quantititive temporal logic formulas. The distributed statistical model checking for discrete event simulators has been integrated into the P framework for Monte Carlo validation of P programs against QuaTEx quantitative temporal logic formulas. For this, 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 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 P.
AB - 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 P ’s framework to include statistical model checking of quantititive temporal logic formulas. The distributed statistical model checking for discrete event simulators has been integrated into the P framework for Monte Carlo validation of P programs against QuaTEx quantitative temporal logic formulas. For this, 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 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 P.
KW - MultiVeStA
KW - QuaTEx
KW - Statistical model checking
KW - programming language
UR - http://www.scopus.com/inward/record.url?scp=85174441169&partnerID=8YFLogxK
U2 - 10.1007/978-3-031-43681-9_3
DO - 10.1007/978-3-031-43681-9_3
M3 - Conference contribution
AN - SCOPUS:85174441169
SN - 9783031436802
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 40
EP - 56
BT - Formal Methods for Industrial Critical Systems - 28th International Conference, FMICS 2023, Proceedings
A2 - Cimatti, Alessandro
A2 - Titolo, Laura
PB - Springer Science and Business Media Deutschland GmbH
T2 - 28th International Conference on Formal Methods in Industrial Critical Systems, FMICS 2023
Y2 - 20 September 2023 through 22 September 2023
ER -