skip to main content
article

Property relevant software testing with model-checkers

Published: 01 November 2006 Publication History

Abstract

Verification is applied to software as a proof method with respect to its requirements. Software testing is necessary due to the fact that verification is often infeasible. Automation is desirable since the complexity and the effort involved are significant. However, automated software testing is commonly used to ensure confidence in the conformance of an implementation to an abstract model, not to its requirement properties. In this paper, we introduce the notion of property relevance of test-cases. Property relevant test-cases can be used to determine property violations. It is shown how to detect the properties relevant to a test-case. New coverage criteria based on property relevance are introduced. Automated generation of test-suites satisfying these criteria is also presented. Finally, feasibility is illustrated with an empirical evaluation.

References

[1]
A. T. Acree, T. A. Budd, R. A. DeMillo, R. J. Lipton, and F. G. Sayward. Mutation analysis. Technical report, School of Information and Computer Science, Georgia Inst. of Technology, Atlanta, Ga., Sept. 1979.]]
[2]
P. Ammann and P. E. Black. A Specification-Based Coverage Metric to Evaluate Test Sets. In HASE, pages 239--248. IEEE Computer Society, 1999.]]
[3]
P. Ammann, P. E. Black, and W. Ding. Model Checkers in Software Testing. Technical report, National Institute of Standards and Technology, 2002.]]
[4]
P. Ammann, P. E. Black, and W. Majurski. Using Model Checking to Generate Tests from Specifications. In ICFEM, 1998.]]
[5]
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, pages 212--221, June 2001.]]
[6]
R. Bharadwaj and C. L. Heitmeyer. Model Checking Complete Requirements Specifications Using Abstraction. Automated Software Engineering, 6(1):37--68, 1999.]]
[7]
P. E. Black. Modeling and Marshaling: Making Tests From Model Checker Counterexamples. In Proceedings of the 19th Digital Avionics Systems Conferences (DASC), volume 1, pages 1B3/1--1B3/6, 2000.]]
[8]
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.]]
[9]
J. Callahan, F. Schneider, and S. Easterbrook. Automated Software Testing Using Model-Checking. In Proceedings 1996 SPIN Workshop, August 1996. Also WVU Technical Report NASA-IVV-96-022.]]
[10]
J. R. Callahan, S. M. Easterbrook, and T. L. Montgomery. Generating Test Oracles Via Model Checking. Technical report, NASA/WVU Software Research Lab, 1998.]]
[11]
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.]]
[12]
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.]]
[13]
R. A. DeMillo, R. J. Lipton, and F. G. Sayward. Hints on Test Data Selection: Help for the Practicing Programmer. Computer, 11:34--41, 1978.]]
[14]
A. Gargantini and C. Heitmeyer. Using Model Checking to Generate Tests From Requirements Specifications. In M. L. O. Nierstrasz, editor, Software Engineering - 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. Springer-Verlag GmbH, September 1999.]]
[15]
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.]]
[16]
G. Hamon, L. de Moura, and J. Rushby. Automated Test Generation with SAL. Technical report, Computer Science Laboratory, SRI International, 2005.]]
[17]
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.]]
[18]
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.]]
[19]
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.]]
[20]
S. Kandl, R. Kirner, and P. Puschner. Development of a framework for automated systematic testing of safety-critical embedded systems. In Proc. Workshop on Intelligent Solutions in Embedded Systems (WISES'06), 2006.]]
[21]
J. Kirby. Example NRL/SCR Software Requirements for an Automobile Cruise Control and Monitoring System. Technical Report TR-87-07, Wang Institute of Graduate Studies, 1987.]]
[22]
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), 2004.]]
[23]
A. J. Offutt, Y. Xiong, and S. Liu. Criteria for generating specification-based tests. In ICECCS, pages 119-. IEEE Computer Society, 1999.]]
[24]
V. Okun, P. E. Black, and Y. Yesha. Testing with Model Checker: Insuring Fault Visibility. In Proceedings of 2002 WSEAS International Conference on System Science, Applied Mathematics & Computer Science, and Power Engineering Systems, pages 1351--1356, 2003.]]
[25]
A. Pnueli. The temporal logic of programs. In FOCS, pages 46--57. IEEE, 1977.]]
[26]
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. IEEE Computer Society, April 2001.]]
[27]
M. W. Whalen, A. Rajan, M. P. Heimdahl, and S. P. Miller. Coverage metrics for requirements-based testing. In ISSTA'06: Proceedings of the 2006 international symposium on Software testing and analysis, pages 25--36, New York, NY, USA, 2006. ACM Press.]]

Cited By

View all
  • (2022)Structural Coverage of LTL Requirements for Learning-based Testing2022 International Conference on IT and Industrial Technologies (ICIT)10.1109/ICIT56493.2022.9989218(1-6)Online publication date: 3-Oct-2022
  • (2017)Uncertainty-Wise Testing of Cyber-Physical Systems10.1016/bs.adcom.2017.06.001(23-94)Online publication date: 2017
  • (2015)Perspectives on White-Box Testing: Coverage, Concurrency, and Concolic Execution2015 IEEE 8th International Conference on Software Testing, Verification and Validation (ICST)10.1109/ICST.2015.7102600(1-11)Online publication date: Apr-2015
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM SIGSOFT Software Engineering Notes
ACM SIGSOFT Software Engineering Notes  Volume 31, Issue 6
November 2006
182 pages
ISSN:0163-5948
DOI:10.1145/1218776
Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 November 2006
Published in SIGSOFT Volume 31, Issue 6

Check for updates

Author Tags

  1. model-checker based testing
  2. property relevance
  3. requirements traceability
  4. software testing
  5. test-suite analysis

Qualifiers

  • Article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

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

Other Metrics

Citations

Cited By

View all
  • (2022)Structural Coverage of LTL Requirements for Learning-based Testing2022 International Conference on IT and Industrial Technologies (ICIT)10.1109/ICIT56493.2022.9989218(1-6)Online publication date: 3-Oct-2022
  • (2017)Uncertainty-Wise Testing of Cyber-Physical Systems10.1016/bs.adcom.2017.06.001(23-94)Online publication date: 2017
  • (2015)Perspectives on White-Box Testing: Coverage, Concurrency, and Concolic Execution2015 IEEE 8th International Conference on Software Testing, Verification and Validation (ICST)10.1109/ICST.2015.7102600(1-11)Online publication date: Apr-2015
  • (2015)Bridging the gap between test cases and requirements by abstract testingInnovations in Systems and Software Engineering10.1007/s11334-015-0245-711:4(233-242)Online publication date: 1-Dec-2015
  • (2013)Security Testing with Fault-Models and PropertiesProceedings of the 2013 IEEE Sixth International Conference on Software Testing, Verification and Validation10.1109/ICST.2013.74(501-502)Online publication date: 18-Mar-2013
  • (2013)Regression testing minimization, selection and prioritization: a surveySoftware Testing, Verification and Reliability10.1002/stvr.43022:2(67-120)Online publication date: 11-Oct-2013
  • (2012)Regression testing minimization, selection and prioritization: a surveySoftware Testing, Verification & Reliability10.1002/stv.43022:2(67-120)Online publication date: 1-Mar-2012
  • (2010)Abstract TestingProceedings of the 2010 Seventh International Conference on the Quality of Information and Communications Technology10.1109/QUATIC.2010.14(89-96)Online publication date: 29-Sep-2010
  • (2008)Automatic Test Case Generation for Safety-Related Embedded SystemsSAE International Journal of Passenger Cars - Electronic and Electrical Systems10.4271/2008-01-01141:1(18-25)Online publication date: 14-Apr-2008
  • (2008)Using model-checkers to generate and analyze property relevant test-casesSoftware Quality Journal10.1007/s11219-007-9031-616:2(161-183)Online publication date: 1-Jun-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