article

Incremental test case generation using bounded model checking: an application to automatic rating

Authors:

Grzegorz Anielak,

Grzegorz Jakacki,

Sławomir LasotaAuthors Info & Claims

International Journal on Software Tools for Technology Transfer (STTT), Volume 17, Issue 3

Pages 339 - 349

https://doi.org/10.1007/s10009-014-0317-2

Published: 01 June 2015 Publication History

Abstract

In this paper we focus on the task of rating solutions to a programming exercise. State-of-the-art rating methods generally examine each solution against an exhaustive set of test cases, typically designed manually. Hence an issue of completeness arises. We propose the application of bounded model checking to the automatic generation of test cases. The experimental evaluation we have performed reveals a substantial increase in accuracy of ratings at a cost of a moderate increase in computation resources needed. Most importantly, application of model checking leads to the finding of errors in solutions that would previously have been classified as correct.

References

[1]

Angeletti, D., Giunchiglia, E., Narizzano, M., Puddu, A., Sabina, S.: Using bounded model checking for coverage analysis of safety-critical software in an industrial setting. J. Autom. Reason. 45(4), 397---414 (2010)

Digital Library

[2]

Anielak, G.: Sprawdzanie równowa¿ności programów przy u¿yciu ograniczonej weryfikacji modelowej. Master's thesis, University of Warsaw. (In Polish) (2012)

[3]

Ball, T.: A theory of predicate-complete test coverage and generation. In: FMCO, pp. 1---22 (2004)

[4]

Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 118---149 (2003)

[5]

Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: K. Jensen, A. Podelski (eds.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004), Lecture Notes in Computer Science, vol. 2988, pp. 168---176. Springer, Berlin (2004)

[6]

Clarke Jr, E.M., Grumberg, O., Peled, D.A.: Model checking. MIT Press, Cambridge (1999)

[7]

Dias-Neto, A.C., Travassos, G.H.: Model-based testing approaches selection for software projects. Inf. Softw. Technol. 51(11), 1487---1504 (2009)

Digital Library

[8]

Eén, N., Sörensson, N.: An extensible sat-solver. In: E. Giunchiglia, A. Tacchella (eds.) SAT, Lecture Notes in Computer Science, vol. 2919, pp. 502---518. Springer, Berlin (2003)

[9]

Fraser, G., Wotawa, F., Ammann, P.: Issues in using model checkers for test case generation. J. Syst. Softw. 82(9), 1403---1418 (2009)

Digital Library

[10]

Fraser, G., Wotawa, F., Ammann, P.E.: Testing with model checkers: a survey. Softw. Test. Verif. Reliab. 19(3), 215---261 (2009)

[11]

Hierons, R.M., Bogdanov, K., Bowen, J.P., Cleaveland, R., Derrick, J., Dick, J., Gheorghe, M., Harman, M., Kapoor, K., Krause, P., Lüttgen, G., Simons, A.J.H., Vilkomir, S., Woodward, M.R., Zedan, H.: Using formal specifications to support testing. ACM Comput. Surv. 41(2), 9:1---9:76 (2009)

Digital Library

[12]

Holzer, A., Schallhart, C., Tautschnig, M., Veith, H.: Query-driven program testing. In: N. Jones, M. Mller-Olm (eds.) Verification, Model Checking, and Abstract Interpretation, Lecture Notes in Computer Science, vol. 5403, pp. 151---166 (2009)

Digital Library

[13]

Kim, M., Kim, Y., Kim, H.: Unit testing of flash memory device driver through a sat-based model checker. In: ASE 2008. 23rd IEEE/ACM International Conference on Automated Software Engineering (2008)

Digital Library

[14]

Kim, M., Kim, Y., Kim, H.: A comparative study of software model checkers as unit testing tools: an industrial case study. IEEE Trans. Softw. Eng. 37(2), 146---160 (2011)

Digital Library

[15]

Kroening, D., Clarke, E., Yorav, K.: Behavioral consistency of C and Verilog programs using bounded model checking. In: Proceedings of DAC 2003, pp. 368---371. ACM Press, New York (2003)

Digital Library

[16]

Lee, D.A., Yoo, J., Lee, J.S.: Equivalence checking between function block diagrams and C programs using HW-CBMC. In: Proceedings of the 30th International Conference on Computer Safety, Reliability, and Security, SAFECOMP'11, pp. 397---408. Springer, Berlin (2011)

Digital Library

[17]

Shukur, Z., Burke, E., Foxley, E.: The automatic assessment of formal specification coursework. J. Comput. High. Educ. 11(1), 86---119 (1999)

[18]

Utting, M., Legeard, B.: Practical Model-Based Testing: A Tools Approach. Morgan-Kaufmann, Burlington (2007)

Cited By

Gadelha MMenezes RCordeiro L(2021)ESBMC 6.1: automated test case generation using bounded model checkingInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-020-00571-223:6(857-861)Online publication date: 1-Dec-2021
https://dl.acm.org/doi/10.1007/s10009-020-00571-2
Stahlbauer AKreis MFraser GDumas MPfahl DApel SRusso A(2019)Testing scratch programs automaticallyProceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3338906.3338910(165-175)Online publication date: 12-Aug-2019
https://dl.acm.org/doi/10.1145/3338906.3338910

Incremental test case generation using bounded model checking: an application to automatic rating
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Software defect analysis
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods

Recommendations

ESBMC 6.1: automated test case generation using bounded model checking
Abstract
ESBMC is an SMT-based bounded model checker that provides a bit-precise verification of both C and C++ programs. Bounded model checking (BMC) was developed to provide faster results when finding property violations; BMC achieves this by limiting ...
Test Case Generation from Mutants Using Model Checking Techniques
ICSTW '11: Proceedings of the 2011 IEEE Fourth International Conference on Software Testing, Verification and Validation Workshops

Mutation testing is a powerful testing technique: a program is seeded with artificial faults and tested. Undetected faults can be used to improve the test bench. The problem of automatically generating test cases from undetected faults is typically not ...
A unified framework for evaluating test criteria in model-checking-assisted test case generation

Testing is often cited as one of the most costly operations in testing dependable systems (Heimdahl et al. 2001 ). A particular challenging task in testing is test-case generation. To improve the efficiency of test-case generation and reduce its cost, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image International Journal on Software Tools for Technology Transfer (STTT)

International Journal on Software Tools for Technology Transfer (STTT) Volume 17, Issue 3

June 2015

119 pages

ISSN:1433-2779

EISSN:1433-2787

Issue’s Table of Contents

Copyright © Copyright © 2015 Springer-Verlag Berlin Heidelberg.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 June 2015

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 03 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Gadelha MMenezes RCordeiro L(2021)ESBMC 6.1: automated test case generation using bounded model checkingInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-020-00571-223:6(857-861)Online publication date: 1-Dec-2021
https://dl.acm.org/doi/10.1007/s10009-020-00571-2
Stahlbauer AKreis MFraser GDumas MPfahl DApel SRusso A(2019)Testing scratch programs automaticallyProceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3338906.3338910(165-175)Online publication date: 12-Aug-2019
https://dl.acm.org/doi/10.1145/3338906.3338910

View Options

View options

Figures

Tables

Media

View Issue’s Table of Contents