A formal analysis of requirements-based testing

Part of book or chapter of book English OPEN
Pecheur, Charles ; Raimondi, Franco ; Brat, Guillaume (2009)

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 (21)
    21 references, page 1 of 3

    [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 veri cation of spin, nusmv, and pddl domains. Technical report, NASA, March 2009.

    [3] J. J. Chilenski. An investigation of three forms of the modi ed 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 modi ed condition/decision coverage to software testing. Software Engineering Journal, pages 193{200, 1994.

    [5] A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri. NuSMV: a new symbolic model veri er. In Proc. of International Conference on Computer-Aided Veri cation, 1999.

    [6] E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. Mit Press, 1999.

    [7] M. Clavel, F. Duran, S. Eker, P. Lincoln, N. Mart -Oliet, J. Meseguer, and J. F. Quesada. The Maude system. In P. Narendran and M. Rusinowitch, editors, Rewriting Techniques and Applications, 10th International Conference, RTA'99, Trento, Italy, July 2{4, 1999, volume 1631 of Lecture Notes in Computer Science, pages 240{243. Springer-Verlag, 1999.

    [8] M. B. Dwyer, G. S. Avrunin, and J. C. Corbett. Property speci cation patterns for nite-state veri cation. In M. Ardis, editor, Proceedings of the 2nd Workshop on Formal Methods in Software Practice (FMSP'98), pages 7{15, New York, 1998. ACM Press.

    [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 fth international planning competition. Technical report, Dept. of Electronics and Automation, University of Brescia, August 2005.

  • Metrics
    views in OpenAIRE
    views in local repository
    downloads in local repository

    The information is available from the following content providers:

    From Number Of Views Number Of Downloads
    Middlesex University Research Repository - IRUS-UK 0 33
Share - Bookmark