nach oben

Software Quality Journal

Erschienen in:

01.06.2008

Using model-checkers to generate and analyze property relevant test-cases

verfasst von: Gordon Fraser, Franz Wotawa

Erschienen in: Software Quality Journal | Ausgabe 2/2008

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Verification is applied to software as a proof method with respect to its requirements. Software testing is necessary because 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.

Vorheriger Artikel Guest Editor’s Introduction to the Special Section on the 2nd Workshop on Advances in Model-based Software Testing (A-MOST’06)

Nächster Artikel Using communication coverage criteria and partial model generation to assist software integration testing

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Acree, A. T., Budd, T. A., DeMillo, R. A., Lipton, R. J., & Sayward, F. G. (1979). Mutation analysis. Tech. rep., School of Information and Computer Science, Georgia Inst. of Technology, Atlanta, GA.

Ammann, P., & Black, P. E. (1999). A specification-based coverage metric to evaluate test sets. In: HASE ’99: The 4th IEEE Iiternational symposium on high-assurance systems engineering (pp. 239–248). Washington, DC, USA: IEEE Computer Society.

Ammann, P., Black, P. E., & Ding, W. (2002). Model Checkers in Software Testing. Tech. rep., National Institute of Standards and Technology.

Ammann, P. E., Black, P. E., & Majurski, W. (1998). Using model checking to generate tests from specifications. In: Proceedings of the second IEEE international conference on formal engineering methods (ICFEM’98)(pp. 46–54). IEEE Computer Society.

Ammann, P., Ding, W., & Xu, D. (2001). Using a model checker to test safety properties. In: Proceedings of the 7th international conference on engineering of complex computer systems (ICECCS 2001)(pp. 212–221). Sweden: IEEE, Skovde.

Bharadwaj, R., & Heitmeyer, C. L. (1999). Model checking complete requirements specifications using abstraction. Automated Software Engineering, 6(1), 37–68.CrossRef

Black, P. E. (2000). Modeling and marshaling: Making tests from model checker counterexamples. In: Proceedings of the 19th digital avionics systems conference(pp 1.B.3–1–1.B.3–6 vol.1).

Black, P. E., Okun, V., & Yesha, Y. (2000). Mutation operators for specifications. In: Proceedings of the fifteenth IEEE international conference on automated software engineering (ASE’00)(pp. 81–88). Washington, DC, USA: IEEE Computer Society.

Callahan, J., Schneider, F., & Easterbrook, S. (1996). Automated software testing using model-checking. In: Proceedings 1996 SPIN workshop, also WVU technical report NASA-IVV-96-022.

Cimatti, A., Clarke, E. M., Giunchiglia, F., & Roveri, M. (1999). NUSMV: A new symbolic model verifier. In: CAV ’99: Proceedings of the 11th international conference on computer aided verification(pp. 495–499). London: Springer-Verlag.

Clarke, E. M., & Emerson, E. A. (1982). Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of Programs, Workshop(pp. 52–71). London, UK: Springer-Verlag.

DeMillo, R. A., Lipton, R. J., & Sayward, F. G. (1978). Hints on test data selection: Help for the practicing programmer. Computer, 11, 34–41.CrossRef

Fraser, G., & Wotawa, F. (2006). Property relevant software testing with model-checkers. SIGSOFT Software Engineering Notes, 31(6), 1–10.CrossRef

Gargantini, A., & Heitmeyer, C. (1999). 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 vol 1687(pp. 146–162). Toulouse, France: Springer.

Hamon, G,, deMoura, L., & Rushby, J. (2004). Generating efficient test sets with a model checker. In: Proceedings of the second international conference on software engineering and formal methods (SEFM’04), pp. 261–270.

Hamon, G., deMoura, L., & Rushby, J. (2005). Automated test generation with SAL. Technical report, computer science laboratory, SRI International.

Havelund, K., & Rosu, G. (2001). Monitoring Java programs with Java PathExplorer. Electronic Notes in Theoretical Computer Science, 55(2), 200–217.CrossRef

Heimdahl, M. P., Rayadurgam, S., Visser, W., Devaraj, G., & Gao, J. (2003). Auto-generating test sequences using model checkers: A case study. In: Third international workshop on formal approaches to software testing, lecture notes in computer science vol 2931(pp. 42–59). Springer Verlag.

Kirby, J. (1987). Example NRL/SCR software requirements for an automobile cruise control and monitoring system. Technical Report TR-87-07, Wang Institute of Graduate Studies.

Li Tan, I. L. Oleg Sokolsky. (2004). Specification-based testing with linear temporal logic. In: Proceedings of IEEE international conference on information reuse and integration (IRI’04), pp. 493–498.

Markey, N., & Schnoebelen, P. (2003). Model checking a path (preliminary report). In: Proceeding of concurrency theory (CONCUR’2003), Marseille, France, Springer, Lect.Notes Comp. Sci, vol 2761, pp. 251–265

Offutt, A. J., Xiong, Y., & Liu, S. (1999). Criteria for generating specification-based tests. In: ICECCS ’99: Proceedings of the 5th international conference on engineering of complex computer systems, IEEE computer society, Washington, DC, USA, pp. 119–129.

Okun, V., Black, P. E., Yesha, Y. (2003). Testing with model checker: Insuring fault visibility. In: N. E. Mastorakis, P. Ekel (Eds.), Proceedings of 2002 WSEAS international conference on system science, applied mathematics & computer science, and power engineering systems(pp. 1351–1356).

Pnueli, A. (1977). The temporal logic of programs. In: 18th annual symposium on foundations of computer science, 31 October-2 November, Providence, Rhode Island, USA, IEEE, pp. 46–57.

Rayadurgam, S., & Heimdahl, M. P. E. (2001). 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), IEEE computer society, Washington, DC, pp. 83–91.

Whalen, M. W., Rajan, A., Heimdahl, M. P., & Miller, S. P. (2006). Coverage metrics for requirements-based testing. In: ISSTA’06: Proceedings of the 2006 international symposium on software testing and analysis, ACM Press, New York, NY, USA, pp. 25–36.

Titel: Using model-checkers to generate and analyze property relevant test-cases
verfasst von: Gordon Fraser
Franz Wotawa
Publikationsdatum: 01.06.2008
Verlag: Springer US
Erschienen in: Software Quality Journal / Ausgabe 2/2008
Print ISSN: 0963-9314
Elektronische ISSN: 1573-1367
DOI: https://doi.org/10.1007/s11219-007-9031-6

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft"

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 2/2008

Using communication coverage criteria and partial model generation to assist software integration testing

A measurement framework for assessing the maturity of requirements engineering process

In this issue

Test frame updating in CPM testing of Prolog programs

Integrating fuzzy theory and hierarchy concepts to evaluate software quality

Software process improvement in small and medium software enterprises: a systematic review

Premium Partner