skip to main content
10.1145/1291535.1291542acmconferencesArticle/Chapter ViewAbstractPublication PagesicseConference Proceedingsconference-collections
Article

Using LTL rewriting to improve the performance of model-checker based test-case generation

Published: 09 July 2007 Publication History

Abstract

Model-checkers have recently been suggested for automated software test-case generation. Several works have presented methods that create efficient test-suites using model-checkers. Ease of use and complete automation are major advantages of such approaches. However, the use of a model-checker comes at the price of potential performance problems. If the model used for test-case generation is complex, then model-checker based approaches can be very slow, or even not applicable at all. In this paper, we identify that unnecessary, redundant calls to the model-checker are one of the causes of bad performance. To overcome this problem, we suggest the use of temporal logic rewriting techniques, which originate from runtime verification research. This achieves a significant increase in the performance, and improves the applicability of model-checker based test-case generation approaches in general. At the same time, the suggested techniques achieve a reduction of the resulting test-suite sizes without degradation of the fault sensitivity. This helps to reduce the costs of the test-case execution.

References

[1]
P. Ammann and P. E. Black. A Specification-Based Coverage Metric to Evaluate Test Sets. In HASE '99: The 4th IEEE International Symposium on High-Assurance Systems Engineering, pages 239--248, Washington, DC, USA, 1999. IEEE Computer Society.
[2]
P. Ammann, W. Ding, and D. Xu. Using a Model Checker to Test Safety Properties. In Proceedings of the 7th International Conference on Engineering of Complex Computer Systems (ICECCS 2001), pages 212--221, Skovde, Sweden, 2001. IEEE.
[3]
P. E. Ammann, P. E. Black, and W. Majurski. Using Model Checking to Generate Tests from Specifications. In Proceedings of the Second IEEE International Conference on Formal Engineering Methods (ICFEM'98), pages 46--54. IEEE Computer Society, 1998.
[4]
H. Barringer, A. Goldberg, K. Havelund, and K. Sen. Program monitoring with Itl in eagle. In PADTAD'04, Parallel and Distributed Systems: Testing and Debugging, 2004.
[5]
P. E. Black. Modeling and Marshaling: Making Tests From Model Checker Counterexamples. In Proc. of the 19th Digital Avionics Systems Conference, pages 1.B.3-1-1.B.3--6 vol.1, 2000.
[6]
P. E. Black, V. Okun, and Y. Yesha. Mutation Operators for Specifications. In Proceedings of the Fifteenth IEEE International Conference on Automated Software Engineering (ASE'00), 2000.
[7]
J. R. Callahan, S. M. Easterbrook, and T. L. Montgomery. Generating Test Oracles Via Model Checking. Technical report, NASA/WVU Software Research Lab, 1998.
[8]
A. Cimatti, E. M. Clarke, F. Giunchiglia, and M. Roveri. NUSMV: A New Symbolic Model Verifier. In CAV '99: Proceedings of the 11th International Conference on Computer Aided Verification, pages 495--499, London, UK, 1999. Springer-Verlag.
[9]
E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Logic of Programs, Workshop, pages 52--71, London, UK, 1982. Springer-Verlag.
[10]
G. Fraser and F. Wotawa. Property relevant software testing with model-checkers. SIGSOFT Softw. Eng. Notes, 31(6):1--10, 2006.
[11]
G. Fraser and F. Wotawa. Redundancy based test-suite reduction. In Proceedings of the 10th International Conference on Fundamental Approaches to Software Engineering (FASE 2007), volume 4422 of Lecture Notes in Computer Science, pages 291--305. Springer, 2007. To Appear.
[12]
A. Gargantini and C. Heitmeyer. Using Model Checking to Generate Tests From Requirements Specifications. In ESEC/FSE'99: 7th European Software Engineering Conference, Held Jointly with the 7th ACM SIGSOFT Symposium on the Foundations of Software Engineering, volume 1687, pages 146--162, Toulouse, France, September 1999. Springer.
[13]
D. L. George Devaraj, Mats P. E. Heimdahl. Condition Based Coverage Criteria: To use or not to use that is the question. To be published, 2005.
[14]
G. Hamon, L. de Moura, and J. Rushby. Generating Efficient Test Sets with a Model Checker. In Proceedings of the Second International Conference on Software Engineering and Formal Methods (SEFM'04), pages 261--270, 2004.
[15]
M. J. Harrold, R. Gupta, and M. L. Soffa. A methodology for controlling the size of a test suite. ACM Trans. Softw. Eng. Methodol, 2(3):270--285, 1993.
[16]
K. Havelund and G. Rosu. Monitoring java programs with Java pathexplorer. Electr. Notes Theor. Comput. Sci., 55(2), 2001.
[17]
K. Havelund and G. Rosu. Monitoring programs using rewriting. In ASE '01: Proceedings of the 16th IEEE international conference on Automated software engineering, page 135, Washington, DC, USA, 2001. IEEE Computer Society.
[18]
K. Havelund and G. Rosu. Efficient monitoring of safety properties. Int. J. Softw. Tools Technol. Transf., 6(2):158--173, 2004.
[19]
M. P. Heimdahl, S. Rayadurgam, W. Visser, G. Devaraj, and J. Gao. Auto-Generating Test Sequences using Model Checkers: A Case Study. In Third International International Workshop on Formal Approaches to Software Testing, volume 2931 of Lecture Notes in Computer Science, pages 42--59. Springer Verlag, October 2003.
[20]
M. P. E. Heimdahl and G. Devaraj. Test-Suite Reduction for Model Based Tests: Effects on Test Quality and Implications for Testing. In ASE, pages 176--185. IEEE Computer Society, 2004.
[21]
M. P. E. Heimdahl, G. Devaraj, and R. Weber. Specification Test Coverage Adequacy Criteria = Specification Test Generation Inadequacy Criteria? In HASE, pages 178--186. IEEE Computer Society, 2004.
[22]
J. A. Jones and M. J. Harrold. Test-suite reduction and prioritization for modified condition/decision coverage. IEEE Trans. Softw. Eng., 29(3):195--209, 2003.
[23]
I. L. Li Tan, Oleg Sokolsky. Specification-based testing with linear temporal logic. In Proceedings of IEEE International Conference on Information Reuse and Integration (IRI'04), pages 493--498, 2004.
[24]
Y.-S. Ma, J. Offutt, and Y. R. Kwon. Mujava: an automated class mutation system. Softw. Test. Verif. Reliab., 15(2):97--133, 2005.
[25]
N. Markey and P. Schnoebelen. Model checking a path (preliminary report). In Proc. Concurrency Theory (CONCUR'2003), Marseille, France, volume 2761 of Lect. Notes Comp. Sci, pages 251--265. Springer, Aug. 2003.
[26]
V. Okun, P. E. Black, and Y. Yesha. Testing with Model Checker: Insuring Fault Visibility. In N. E. Mastorakis and P. Ekel, editors, Proceedings of 2002 WSEAS International Conference on System Science, Applied Mathematics & Computer Science, and Power Engineering Systems, pages 1351--1356, 2003.
[27]
A. Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science, 31 October-2 November, Providence, Rhode Island, USA, pages 46--57. IEEE, 1977.
[28]
S. Rayadurgam and M. P. E. Heimdahl. Coverage Based Test-Case Generation Using Model Checkers. In Proceedings of the 8th Annual IEEE International Conference and Workshop on the Engineering of Computer Based Systems (ECBS 2001), pages 83--91, Washington, DC, April 2001. IEEE Computer Society.
[29]
G. Rosu and K. Havelund. Rewriting-based techniques for runtime verification. Automated Software Engg., 12(2):151--197, 2005.
[30]
G. Rothermel, M. J. Harrold, J. Ostrin, and C. Hong. An empirical study of the effects of minimization on the fault detection capabilities of test suites. In ICSM '98: Proceedings of the International Conference on Software Maintenance, page 34, Washington, DC, USA, 1998. IEEE Computer Society.

Cited By

View all
  • (2021)Model-based test case generation and prioritization: a systematic literature reviewSoftware and Systems Modeling10.1007/s10270-021-00924-821:2(717-753)Online publication date: 7-Sep-2021
  • (2017)Model-based automatic test case generation for automotive embedded software testingInternational Journal of Automotive Technology10.1007/s12239-018-0011-619:1(107-119)Online publication date: 3-Oct-2017
  • (2015)An Implementation Framework for Optimizing Test Case Generation Using Model CheckingStructured Object-Oriented Formal Language and Method10.1007/978-3-319-17404-4_1(3-16)Online publication date: 17-Apr-2015
  • Show More Cited By

Index Terms

  1. Using LTL rewriting to improve the performance of model-checker based test-case generation

    Recommendations

    Comments

    Information & Contributors

    Information

    Published In

    cover image ACM Conferences
    A-MOST '07: Proceedings of the 3rd international workshop on Advances in model-based testing
    July 2007
    127 pages
    ISBN:9781595938503
    DOI:10.1145/1291535
    Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

    Sponsors

    In-Cooperation

    Publisher

    Association for Computing Machinery

    New York, NY, United States

    Publication History

    Published: 09 July 2007

    Permissions

    Request permissions for this article.

    Check for updates

    Author Tags

    1. LTL rewriting
    2. automated software testing
    3. test-case generation with model-checkers

    Qualifiers

    • Article

    Conference

    ISSTA07
    Sponsor:

    Upcoming Conference

    ICSE 2025

    Contributors

    Other Metrics

    Bibliometrics & Citations

    Bibliometrics

    Article Metrics

    • Downloads (Last 12 months)2
    • Downloads (Last 6 weeks)0
    Reflects downloads up to 19 Feb 2025

    Other Metrics

    Citations

    Cited By

    View all
    • (2021)Model-based test case generation and prioritization: a systematic literature reviewSoftware and Systems Modeling10.1007/s10270-021-00924-821:2(717-753)Online publication date: 7-Sep-2021
    • (2017)Model-based automatic test case generation for automotive embedded software testingInternational Journal of Automotive Technology10.1007/s12239-018-0011-619:1(107-119)Online publication date: 3-Oct-2017
    • (2015)An Implementation Framework for Optimizing Test Case Generation Using Model CheckingStructured Object-Oriented Formal Language and Method10.1007/978-3-319-17404-4_1(3-16)Online publication date: 17-Apr-2015
    • (2013)Effectively using search-based software engineering techniques within model checking and its applicationsProceedings of the 1st International Workshop on Combining Modelling and Search-Based Software Engineering10.5555/2662572.2662592(67-70)Online publication date: 19-May-2013
    • (2010)A Formal Logic Approach to Constrained Combinatorial TestingJournal of Automated Reasoning10.1007/s10817-010-9171-445:4(331-358)Online publication date: 1-Dec-2010
    • (2009)Increasing Diversity in Coverage Test Suites Using Model CheckingProceedings of the 2009 Ninth International Conference on Quality Software10.1109/QSIC.2009.36(211-218)Online publication date: 24-Aug-2009
    • (2009)Experiments on the test case length in specification based test case generation2009 ICSE Workshop on Automation of Software Test10.1109/IWAST.2009.5069037(18-26)Online publication date: May-2009
    • (2009)Issues in using model checkers for test case generationJournal of Systems and Software10.1016/j.jss.2009.05.01682:9(1403-1418)Online publication date: 1-Sep-2009
    • (2009)On the order of test goals in specification-based testingThe Journal of Logic and Algebraic Programming10.1016/j.jlap.2009.01.00478:6(472-490)Online publication date: Jul-2009
    • (2008)Ordering Coverage Goals in Model Checker Based TestingProceedings of the 2008 IEEE International Conference on Software Testing Verification and Validation Workshop10.1109/ICSTW.2008.31(31-40)Online publication date: 9-Apr-2008
    • Show More Cited By

    View Options

    Login options

    View options

    PDF

    View or Download as a PDF file.

    PDF

    eReader

    View online with eReader.

    eReader

    Figures

    Tables

    Media

    Share

    Share

    Share this Publication link

    Share on social media