Remember Me
Or use your Academic/Social account:


Or use your Academic/Social account:


You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.


Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message


Verify Password:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Pecheur, Charles; Raimondi, Franco; Brat, Guillaume (2009)
Publisher: Association for Computing Machinery
Languages: English
Types: Part of book or chapter of book
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.
  • The results below are discovered through our pilot algorithms. Let us know how we are doing!

    • [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.
    • [11] K. J. Hayhurst, D. S. Veerhusen, J. Chilenski, and L. K. Riersn. A practical tutorial on modi ed condition/decision coverage. Technical Report TM-2001-210876, NASA Langley Research Center, 2001.
    • [12] G. J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5), 1997.
    • [13] H. S. Hong, I. Lee, O. Sokolsky, and H. Ural. A temporal logic based theory of test coverage and generation. In TACAS '02: Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 327{341, London, UK, 2002.
    • [14] L. Khatib, N. Muscettola, and K. Havelund. Veri cation of plan models using UPPAAL. Lecture Notes in Computer Science, 1871, 2001.
    • [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] M. Purandare and F. Somenzi. Vacuum cleaning ctl formulae. In CAV '02: Proceedings of the 14th International Conference on Computer Aided Veri cation, pages 485{499, London, UK, 2002. Springer-Verlag.
    • [17] RTCA. Software Considerations in Airborne Systems and Equipment Certi cation, 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. Speci cation-based testing with linear temporal logic. In Proceedings of the IEEE International Conference on Information Reuse and Integration (IRI04). IEEE Society, 2004.
    • [21] M. W. Whalen, A. Rajan, M. P. E. 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, 2006. ACM Press.
  • No related research data.
  • No similar publications.

Share - Bookmark

Funded by projects

  • RCUK | UbiVal: Fundamental Approa...

Cite this article