Statistical Model Checking Meets Property-Based Testing

Bernhard K. Aichernig, Richard Alexander Schumi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.
Original languageEnglish
Title of host publication10th IEEE International Conference on Software Testing, Verification and Validation (ICST 2017)
PublisherIEEE Computer Society
Pages390-400
DOIs
Publication statusPublished - 2017
Event10th IEEE International Conference on Software Testing, Verification and Validation (ICST 2017) - Tokyo, Japan
Duration: 13 Mar 201717 Mar 2017
http://aster.or.jp/conference/icst2017/

Conference

Conference10th IEEE International Conference on Software Testing, Verification and Validation (ICST 2017)
Abbreviated titleICST 2017
CountryJapan
CityTokyo
Period13/03/1717/03/17
Internet address

Fields of Expertise

  • Information, Communication & Computing

Fingerprint Dive into the research topics of 'Statistical Model Checking Meets Property-Based Testing'. Together they form a unique fingerprint.

Cite this