Statistical Model Checking Meets Property-Based Testing

Bernhard K. Aichernig, Richard Alexander Schumi

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

Abstract

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.
Originalspracheenglisch
Titel10th IEEE International Conference on Software Testing, Verification and Validation (ICST 2017)
Herausgeber (Verlag)IEEE Computer Society
Seiten390-400
DOIs
PublikationsstatusVeröffentlicht - 2017
Veranstaltung10th IEEE International Conference on Software Testing, Verification and Validation - Tokyo, Japan
Dauer: 13 Mär 201717 Mär 2017
http://aster.or.jp/conference/icst2017/

Konferenz

Konferenz10th IEEE International Conference on Software Testing, Verification and Validation
KurztitelICST 2017
LandJapan
OrtTokyo
Zeitraum13/03/1717/03/17
Internetadresse

Fields of Expertise

  • Information, Communication & Computing

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

Dieses zitieren