Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Model-based testing of probabilistic systems
Gerhold M., Stoelinga M. Formal Aspects of Computing30 (1):77-106,2018.Type:Article
Date Reviewed: Apr 18 2018

Gerhold and Stoelinga’s paper proposes an interesting framework to test probabilistic systems based on the concepts of soundness and completeness. The crux of their argument is “the conformance relation for probabilistic input/output conformance” (ioco), which informs “exactly when an implementation should pass a test.” Soundness here means a proper implementation is that which passes a test suite, while completeness means the framework is capable of detecting each deviation from a specification sufficiently precisely, at least for large samples.

The authors show “how to automatically derive, execute, and evaluate probabilistic test cases” as per the mode requirement. Three illustrative case studies are presented, namely, “Knuth and Yao’s dice application, the binary exponential backoff protocol, and the FireWire leadership protocol.” The implementation of the test evaluation processes turns out to be functionally and statistically correct.

This is a nicely written paper that I would certainly recommend for postgraduates and researchers in statistics and computer science.

Reviewer:  Soubhik Chakraborty Review #: CR145981 (1807-0383)
Bookmark and Share
  Featured Reviewer  
 
Model Checking (D.2.4 ... )
 
 
Probabilistic Algorithms (Including Monte Carlo) (G.3 ... )
 
Would you recommend this review?
yes
no
Other reviews under "Model Checking": Date
Systems and software verification: model-checking techniques and tools
B ., Bidoit M., Finkel A., Laroussinie F., Petit A., Petrucci L., Schnoebelen P., McKenzie P., Springer-Verlag New York, Inc., New York, NY, 1999.  190, Type: Book (9783540415237)
Sep 30 2002
Module checking
Kupferman O., Vardi M., Wolper P. Information and Computation 164(2): 322-344, 2001. Type: Article
Mar 1 2002
SMC: a symmetry-based model checker for verification of safety and liveness properties
Sistla A., Gyuris V., Emerson E. ACM Transactions on Software Engineering and Methodology 9(2): 133-166, 2000. Type: Article
Sep 1 2000
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy