More Web Proxy on the site http://driver.im/

research-article

Towards integrating statistical model checking into property-based testing

Authors:

Bernhard K. Aichernig,

Richard SchumiAuthors Info & Claims

MEMOCODE '16: Proceedings of the 14th ACM-IEEE International Conference on Formal Methods and Models for System Design

Pages 71 - 76

Published: 18 November 2016 Publication History

Abstract

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.

References

[1]

B. K. Aichernig and R. Schumi, "Property-based testing with FsCheck by deriving properties from business rule models," in ICSTW. IEEE, 2016, pp. 219--228.

[2]

M. AlTurki and J. Meseguer, "PVESTA: A parallel statistical model checking and quantitative analysis tool," in CALCO, ser. LNCS, vol. 6859. Springer, 2011, pp. 386--392.

Digital Library

[3]

A. Arnold, B. Boyer, and A. Legay, "Contracts and behavioral patterns for SoS: The EU IP DANSE approach," in AiSoS, ser. EPTCS, vol. 133. Open Publishing Association, 2013, pp. 47--66.

[4]

B. Boyer, K. Corre, A. Legay, and S. Sedwards, "PLASMA-lab: A flexible, distributable statistical model checking library," in QEST, ser. LNCS, vol. 8054. Springer, 2013, pp. 160--164.

Digital Library

[5]

P. E. Bulychev, A. David, K. G. Larsen, M. Mikucionis, D. B. Poulsen, A. Legay, and Z. Wang, "UPPA AL-SMC: Statistical model checking for priced timed automata," in QAPL, ser. EPTCS, vol. 85. Open Publishing Association, 2012, pp. 1--16.

[6]

K. Claessen and J. Hughes, "QuickCheck: A lightweight tool for random testing of Haskell programs," in ICFP. ACM, 2000, pp. 268--279.

Digital Library

[7]

A. David, K. G. Larsen, A. Legay, M. Mikucionis, D. B. Poulsen, and S. Sedwards, "Statistical model checking for biological systems," International Journal on Software Tools for Technology Transfer, vol. 17, no. 3, pp. 351--367, Jun. 2015.

Digital Library

[8]

Z. Govindarajulu, Sequential statistics. World Scientific, 2004.

[9]

T. Hérault, R. Lassaigne, F. Magniette, and S. Peyronnet, "Approximate probabilistic model checking," in VMCAI, ser. LNCS, vol. 2937. Springer, 2004, pp. 73--84.

[10]

J. Hughes, "QuickCheck testing for fun and profit," in PADL, ser. LNCS, vol. 4354. Springer, 2007, pp. 1--32.

Digital Library

[11]

C. Jégourel, A. Legay, and S. Sedwards, "A platform for high performance statistical model checking - PLASMA," in TACAS, ser. LNCS, vol. 7214. Springer, 2012, pp. 498--503.

Digital Library

[12]

A. S. Kalaji, R. M. Hierons, and S. Swift, "Generating feasible transition paths for testing from an extended finite state machine (EFSM)." in ICST. IEEE, 2009, pp. 230--239.

Digital Library

[13]

M. Z. Kwiatkowska, G. Norman, and D. Parker, "PRISM 4.0: Verification of probabilistic real-time systems," in CAV, ser. LNCS, vol. 6806. Springer, 2011, pp. 585--591.

Digital Library

[14]

A. Legay, B. Delahaye, and S. Bensalem, "Statistical model checking: An overview," in RV, ser. LNCS, vol. 6418. Springer, 2010, pp. 122--135.

Digital Library

[15]

A. Legay and L.-M. Traonouez, "Statistical model checking with change detection," Sep. 2015, working paper or preprint. {Online}. Available: https://hal.archives-ouvertes.fr/hal-01242138

[16]

R. Nilsson, ScalaCheck: The Definitive Guide, ser. IT Pro. Artima Incorporated, 2014.

[17]

M. Papadakis and K. Sagonas, "A PropEr integration of types and function specifications with property-based testing," in Erlang. ACM, 2011, pp. 39--50.

Digital Library

[18]

C. Runciman, M. Naylor, and F. Lindblad, "SmallCheck and lazy SmallCheck: Automatic exhaustive testing for small values," in Haskell. ACM, 2008, pp. 37--48.

Digital Library

[19]

K. Sen, M. Viswanathan, and G. A. Agha, "VESTA: A statistical model-checker and analyzer for probabilistic systems," in QEST. IEEE, 2005, pp. 251--252.

Digital Library

[20]

Y. Wada and S. Kusakabe, "Performance evaluation of a testing framework using QuickCheck and Hadoop," Journal of Information Processing, vol. 20, no. 2, pp. 340--346, 2012.

[21]

A. Wald, Sequential analysis. Courier Corporation, 1973.

[22]

H. L. S. Younes, "Ymer: A statistical model checker," in CAV, ser. LNCS, vol. 3576. Springer, 2005, pp. 429--433.

Digital Library

Cited By

Aichernig BBauerstätter PJöbstl EKann SKorošec RKrenn WMateis CSchlick RSchumi R(2019)Learning and statistical model checking of system response timesSoftware Quality Journal10.1007/s11219-018-9432-827:2(757-795)Online publication date: 1-Jun-2019
https://dl.acm.org/doi/10.1007/s11219-018-9432-8

Towards integrating statistical model checking into property-based testing
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Software defect analysis

Recommendations

Hardware implementation of BLTL property checkers for acceleration of statistical model checking
ICCAD '13: Proceedings of the International Conference on Computer-Aided Design

Statistical model checking is a method to analyze systems where values of variables may have some uncertainty or variations. It can be used to check whether some desired properties are satisfied with specified probability under such uncertainty. In ...
Active property checking
EMSOFT '08: Proceedings of the 8th ACM international conference on Embedded software

Runtime property checking (as implemented in tools like Purify or Valgrind) checks whether a program execution satisfies a property. Active property checking extends runtime checking by checking whether the property is satisfied by all program ...
Statistical model checking of Timed Rebeca models

The actor-based language, Timed Rebeca, was introduced to model distributed and asynchronous systems with timing constraints and message passing communication. A toolset was developed for automated translation of Timed Rebeca models to Erlang. The ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

MEMOCODE '16: Proceedings of the 14th ACM-IEEE International Conference on Formal Methods and Models for System Design

November 2016

196 pages

ISBN:9781509027910

General Chair:
Jean-Pierre Talpin
INRIA, France

Sponsors

Publisher

IEEE Press

Publication History

Published: 18 November 2016

Check for updates

Qualifiers

Research-article

Conference

MEMOCODE'16

Sponsor:

MEMOCODE'16: 14th ACM-IEEE ACM-IEEE International Conference on Formal Methods and Models for System Design

November 18 - 20, 2016

Kanpur, India

Acceptance Rates

Overall Acceptance Rate 34 of 82 submissions, 41%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
12
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Aichernig BBauerstätter PJöbstl EKann SKorošec RKrenn WMateis CSchlick RSchumi R(2019)Learning and statistical model checking of system response timesSoftware Quality Journal10.1007/s11219-018-9432-827:2(757-795)Online publication date: 1-Jun-2019
https://dl.acm.org/doi/10.1007/s11219-018-9432-8

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents