Statistical Model Checking Meets Property-Based Testing

Bernhard K. Aichernig, Richard Alexander Schumi

Publikation: Beitrag in Buch/Bericht/KonferenzbandBeitrag in einem KonferenzbandBegutachtung


In recent years, statistical model checking (SMC) has become increasingly
popular, because it scales well to larger stochastic models and is
relatively simple to implement. SMC solves the model checking problem by
simulating the model for finitely many executions and uses hypothesis
testing to infer if the samples provide statistical evidence for or
against a property. Being based on simulation and statistics, SMC avoids the
state-space explosion problem well-known from other model checking
algorithms. In this paper we show how SMC can be easily integrated into a
property-based testing framework, like FsCheck for C#. As a
result we obtain a very flexible testing and simulation environment,
where a programmer can define models and properties in a familiar
programming language. The advantages: no external modelling language
is needed and both stochastic models and implementations can be checked.
In addition, we have access to the powerful test-data generators of a
property-based testing tool. We demonstrate the feasibility of our approach
by repeating three experiments from the SMC literature.
Titel10th IEEE International Conference on Software Testing, Verification and Validation (ICST 2017)
Herausgeber (Verlag)IEEE Computer Society
PublikationsstatusVeröffentlicht - 2017
Veranstaltung10th IEEE International Conference on Software Testing, Verification and Validation: ICST 2017 - Tokyo, Japan
Dauer: 13 Mär 201717 Mär 2017


Konferenz10th IEEE International Conference on Software Testing, Verification and Validation
KurztitelICST 2017

Fields of Expertise

  • Information, Communication & Computing


Untersuchen Sie die Forschungsthemen von „Statistical Model Checking Meets Property-Based Testing“. Zusammen bilden sie einen einzigartigen Fingerprint.

Dieses zitieren