A formal analysis of requirements-based testing

ABSTRACT

The aim of requirements-based testing is to generate test cases from a set of requirements for a given system or piece of software. In this paper we propose a formal semantics for the generation of test cases from requirements by revising and extending the results presented in previous works (e.g.: [21, 20, 13]). We give a syntactic characterisation of our method, defined inductively over the syntax of LTL formulae, and prove that this characterisation is sound and complete, given some restrictions on the formulae that can be used to encode requirements. We provide various examples to show the applicability of our approach.

REFERENCES

• 1: R. Armoni, L. Fix, A. Flaisher, O. Grumberg, N. Piterman, A. Tiemeyer, and M. Y. Vardi. Enhanced vacuity detection in linear temporal logic. In CAV 2003, Boulder, CO, USA, volume 2725 of Lecture Notes in Computer Science, pages 368--380. Springer, 2003.
• 2: G. Brat, C. Pecheur, and F. Raimondi. A formal analysis of requirements-based testing and its applications to the verification of spin, nusmv, and pddl domains. Technical report, NASA, March 2009.
• 3: J. J. Chilenski. An investigation of three forms of the modified condition decision coverage (MCDC) criterion. Technical report DOT/FAA/AR-01/18DOT/FAA/AR-01/18, Federal Aviation Administration, 2001.
• 4: J. J. Chilenski and S. P. Miller. Applicability of modified condition/decision coverage to software testing. Software Engineering Journal, pages 193--200, 1994.
• 5: Alessandro Cimatti , Edmund M. Clarke , Fausto Giunchiglia , Marco Roveri, NUSMV: A New Symbolic Model Verifier, Proceedings of the 11th International Conference on Computer Aided Verification, p.495-499, July 06-10, 1999
• 6: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 7: Manuel Clavel , Fransisco Durán , Steven Eker , Patrick Lincoln , Narciso Martí-Oliet , José Meseguer , Jose F. Quesada, The Maude System, Proceedings of the 10th International Conference on Rewriting Techniques and Applications, p.240-243, July 02-04, 1999
• 8: Matthew B. Dwyer , George S. Avrunin , James C. Corbett, Property specification patterns for finite-state verification, Proceedings of the second workshop on Formal methods in software practice, p.7-15, March 04-05, 1998, Clearwater Beach, Florida, United States [doi>10.1145/298595.298598]
• 9: C. Eisner et al. Reasoning with temporal logic on truncated paths. In Proceedings of CAV '03, volume 2725 of Lecture Notes in Computer Science. Springer Verlag, 2003.
• 10: A. Gerevini and D. Long. Plan constraints and preferences in pddl3: The language of the fifth international planning competition. Technical report, Dept. of Electronics and Automation, University of Brescia, August 2005.
• 11: Hayhurst Kelly J. , Veerhusen Dan S. , Chilenski John J. , Rierson Leanna K., A Practical Tutorial on Modified Condition/Decision Coverage, NASA Langley Technical Report Server, 2001
• 12: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 13: Hyoung Seok Hong , Insup Lee , Oleg Sokolsky , Hasan Ural, A Temporal Logic Based Theory of Test Coverage and Generation, Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.327-341, April 08-12, 2002
• 14: Lina Khatib , Nicola Muscettola , Klaus Havelund, Verification of Plan Models Using UPPAAL, Proceedings of the First International Workshop on Formal Approaches to Agent-Based Systems-Revised Papers, p.114-122, April 05-07, 2000
• 15: J. Penix, C. Pecheur, and K. Havelund. Using model checking to validate AI planner domain models. In Proceedings of the 23rd Annual Software Engineering Workshop, NASA Goddard, 1998.
• 16: Mitra Purandare , Fabio Somenzi, Vacuum Cleaning CTL Formulae, Proceedings of the 14th International Conference on Computer Aided Verification, p.485-499, July 27-31, 2002
• 17: RTCA. Software Considerations in Airborne Systems and Equipment Certification, 1992.
• 18: S. W. Squyres et al. The Opportunity Rover's Athena Science Investigation at Meridiani Planum, Mars. Science, 306:1698--1703, 2004.
• 19: S. W. Squyres et al. The Spirit Rover's Athena Science Investigation at Gusev Crater, Mars. Science, 305:794--799, 2004.
• 20: L. Tan, O. Sokolsky, and I. Lee. Specification-based testing with linear temporal logic. In Proceedings of the IEEE International Conference on Information Reuse and Integration (IRI04). IEEE Society, 2004.
• 21: Michael W. Whalen , Ajitha Rajan , Mats P.E. Heimdahl , Steven P. Miller, Coverage metrics for requirements-based testing, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA [doi>10.1145/1146238.1146242]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

General Terms:
Verification

Keywords:
coverage metrics, requirements-based testing