Statistical Model Checking Meets Property-Based Testing

Bernhard K. Aichernig, Richard Alexander Schumi

Research output: Chapter in Book/Report/Conference proceedingConference contributionResearchpeer-review

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

Fingerprint

Model checking
Testing
Stochastic models
Statistical Models
Computer programming languages
Explosions
Statistics

Fields of Expertise

  • Information, Communication & Computing

Cite this

Aichernig, B. K., & Schumi, R. A. (2017). Statistical Model Checking Meets Property-Based Testing. In 10th IEEE International Conference on Software Testing, Verification and Validation (ICST 2017) (pp. 390-400). IEEE Computer Society. https://doi.org/10.1109/ICST.2017.42

Statistical Model Checking Meets Property-Based Testing. / Aichernig, Bernhard K.; Schumi, Richard Alexander.

10th IEEE International Conference on Software Testing, Verification and Validation (ICST 2017). IEEE Computer Society, 2017. p. 390-400.

Research output: Chapter in Book/Report/Conference proceedingConference contributionResearchpeer-review

Aichernig, BK & Schumi, RA 2017, Statistical Model Checking Meets Property-Based Testing. in 10th IEEE International Conference on Software Testing, Verification and Validation (ICST 2017). IEEE Computer Society, pp. 390-400, 10th IEEE International Conference on Software Testing, Verification and Validation (ICST 2017), Tokyo, Japan, 13/03/17. https://doi.org/10.1109/ICST.2017.42
Aichernig BK, Schumi RA. Statistical Model Checking Meets Property-Based Testing. In 10th IEEE International Conference on Software Testing, Verification and Validation (ICST 2017). IEEE Computer Society. 2017. p. 390-400 https://doi.org/10.1109/ICST.2017.42
Aichernig, Bernhard K. ; Schumi, Richard Alexander. / Statistical Model Checking Meets Property-Based Testing. 10th IEEE International Conference on Software Testing, Verification and Validation (ICST 2017). IEEE Computer Society, 2017. pp. 390-400
@inproceedings{4a770e830b044f88b03004925bdf5ff9,
title = "Statistical Model Checking Meets Property-Based Testing",
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.",
author = "Aichernig, {Bernhard K.} and Schumi, {Richard Alexander}",
year = "2017",
doi = "10.1109/ICST.2017.42",
language = "English",
pages = "390--400",
booktitle = "10th IEEE International Conference on Software Testing, Verification and Validation (ICST 2017)",
publisher = "IEEE Computer Society",
address = "United States",

}

TY - GEN

T1 - Statistical Model Checking Meets Property-Based Testing

AU - Aichernig, Bernhard K.

AU - Schumi, Richard Alexander

PY - 2017

Y1 - 2017

N2 - 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.

AB - 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.

U2 - 10.1109/ICST.2017.42

DO - 10.1109/ICST.2017.42

M3 - Conference contribution

SP - 390

EP - 400

BT - 10th IEEE International Conference on Software Testing, Verification and Validation (ICST 2017)

PB - IEEE Computer Society

ER -