Another publication has been accepted at MEMOCODE’16.
Bernhard K. Aichernig and Richard Schumi. Towards Integrating Statistical Model Checking into Property-Based Testing. In 14th ACM/IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE, Kanpur, India, Nov. 18–20, 2016. IEEE Computer Society, 2016. In Press. (PDF)
In recent years statistical model checking (SMC) became increasingly popular, mainly because it does not suffer from one of the major problems that limits traditional model checking, the so called state-space-explosion problem. SMC solves this problem by simulating a stochastic model for finitely many executions. There exist a number of SMC tools, but they require the user to learn a specific modelling language and a particular (temporal) logic to express properties. In this paper we propose a more flexible application of SMC, where both the model and the properties can be defined in a programming language. The technique builds upon the well-known property-based testing approach. We use the programming language C\# and its associated tool FsCheck to demonstrate our approach. A stochastic counter serves as illustrating example.