Skip to main content
Erschienen in: International Journal on Software Tools for Technology Transfer 4/2014

01.08.2014 | TASE 12

Model-based test generation using extended symbolic grammars

verfasst von: Hai-Feng Guo, Mahadevan Subramaniam

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 4/2014

Einloggen

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

search-config
loading …

Abstract

A novel, model-based test case generation approach for validating reactive systems, especially those supporting richly structured data inputs and/or interactions, is presented. Given an executable system model and an extended symbolic grammar specifying plausible system inputs, the approach performs a model-based simulation to (i) ensure the consistency of the model with respect to the specified inputs, and (ii) generate corresponding test cases for validating the system. The model-based simulation produces a state transition diagram (STD) automatically justifying the model runtime behaviors within the test case coverage. The STD can further be transformed to produce an evolved symbolic grammar, which can then be used to incrementally generate a refined set of test cases. As a case study, we present a live sequence chart (LSC) model-based test generator, named LCT in short, for LSC simulation and consistency testing. The evolved symbolic grammar produced by the simulator can either be used to generate practical test cases for software testing, or be further refined by applying our model-based test generation approach again with additional test coverage criteria. We further show that LSCs can also be used to specify and test certain temporal system properties during the model simulation. Their satisfaction, reflected in the STD, can either be served as a directive for selective test generation, or a basis for further temporal property model checking.

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

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!

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!

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!

Fußnoten
1
Internal events are those not starting from objects with waved clouds such as Buyer or Seller.
 
2
Hidden events are those related to the structural syntax of LSCs, e.g., end of prechart, or entering a main chart.
 
3
A node is called a variant of another if both nodes have the same four-tuple running state except the renaming of symbolic terminals.
 
4
Iterative deepening instead of Prolog’s standard depth-first search is used for completeness. Rewriting and heuristics based selection of literals are used to aid termination.
 
Literatur
1.
Zurück zum Zitat Bernot, G., Gaudel, M., Marre, B.: Software testing based on formal specifications: a theory and a tool. Softw. Eng. J. 6(6), 387–405 (1991)CrossRef Bernot, G., Gaudel, M., Marre, B.: Software testing based on formal specifications: a theory and a tool. Softw. Eng. J. 6(6), 387–405 (1991)CrossRef
2.
Zurück zum Zitat Bertolino, A., Marchetti, E., Muccini, H.: Introducing a reasonably complete and coherent approach for model-based testing. Electron. Notes Theor. Comput. Sci. 116, 85–97 (2005)CrossRef Bertolino, A., Marchetti, E., Muccini, H.: Introducing a reasonably complete and coherent approach for model-based testing. Electron. Notes Theor. Comput. Sci. 116, 85–97 (2005)CrossRef
3.
Zurück zum Zitat Bohn, J., Damm, W., Wittke, H., Klose, J., Moik, A.: Modeling and validating train system applications using statemate and live sequence charts. In: Proceedings of Conference on Integrated Design and Process Technology (IDPT2002), Society for Design and Process Science (2002) Bohn, J., Damm, W., Wittke, H., Klose, J., Moik, A.: Modeling and validating train system applications using statemate and live sequence charts. In: Proceedings of Conference on Integrated Design and Process Technology (IDPT2002), Society for Design and Process Science (2002)
4.
Zurück zum Zitat Bontemps, Y., Heymans, P.: Turning high-level live sequence charts into automata. In: Proceedings of Scenarios and State Machines: Models Algorithms and tools, 24th International Conference on Software Engineering, May 2002, ACM (2003) Bontemps, Y., Heymans, P.: Turning high-level live sequence charts into automata. In: Proceedings of Scenarios and State Machines: Models Algorithms and tools, 24th International Conference on Software Engineering, May 2002, ACM (2003)
5.
Zurück zum Zitat Bontemps, Y., Heymans, P., Kugler, H.: Applying LSCs to the specification of an air traffic control system. In: Proceedings of Workshop on Scenarios and State Machines: Models, Algorithms and Tools (2003) Bontemps, Y., Heymans, P., Kugler, H.: Applying LSCs to the specification of an air traffic control system. In: Proceedings of Workshop on Scenarios and State Machines: Models, Algorithms and Tools (2003)
6.
Zurück zum Zitat Broy, M., Jonsson, B., Katoen, J., Leucker, M., Pretschner, A.: Model-based Testing of Reactive Systems. LNCS(3472), Springer (2005) Broy, M., Jonsson, B., Katoen, J., Leucker, M., Pretschner, A.: Model-based Testing of Reactive Systems. LNCS(3472), Springer (2005)
7.
Zurück zum Zitat Bunker, A., Gopalakrishnan, G., Slind, K.: Live sequence charts applied to hardware requirements specification and verification: a vci bus interface model. Softw. Tools Technol. Transf. 7(4), 250–341 (2005) Bunker, A., Gopalakrishnan, G., Slind, K.: Live sequence charts applied to hardware requirements specification and verification: a vci bus interface model. Softw. Tools Technol. Transf. 7(4), 250–341 (2005)
8.
Zurück zum Zitat Combes, P., Harel, D., Kugler, H.: Modeling and verification of a telecommunication application using live sequence charts and the play-engine tool. In: Peled, D.A., Tsay, Y.-K. (eds.) Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol. 3707, pp. 414–428. Springer, Berlin, Heidelberg (2005) Combes, P., Harel, D., Kugler, H.: Modeling and verification of a telecommunication application using live sequence charts and the play-engine tool. In: Peled, D.A., Tsay, Y.-K. (eds.) Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol. 3707, pp. 414–428. Springer, Berlin, Heidelberg (2005)
9.
Zurück zum Zitat Coppit, D., Lian, J.: Yagg: an easy-to-use generator for structured test inputs. In: Proceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering. ASE ‘05, pp. 356–359. Long Beach, CA, USA (2005) Coppit, D., Lian, J.: Yagg: an easy-to-use generator for structured test inputs. In: Proceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering. ASE ‘05, pp. 356–359. Long Beach, CA, USA (2005)
10.
Zurück zum Zitat Damm, W., Harel, D.: LSCs: breathing life into message sequence charts. In: Proceedings of 3rd IFIP International Conference on Formal Methods for Open Object-based Distributed Systems, pp. 293–312 (1999) Damm, W., Harel, D.: LSCs: breathing life into message sequence charts. In: Proceedings of 3rd IFIP International Conference on Formal Methods for Open Object-based Distributed Systems, pp. 293–312 (1999)
11.
Zurück zum Zitat Engels, A., Fiejs, L., Mauw, S.: Test generation for intelligent networks using model checking. In: Proceedings of Workshop on Tools and Algorithms for Construction and Analysis of Systems (TACAS), pp. 384–398 (1997) Engels, A., Fiejs, L., Mauw, S.: Test generation for intelligent networks using model checking. In: Proceedings of Workshop on Tools and Algorithms for Construction and Analysis of Systems (TACAS), pp. 384–398 (1997)
12.
Zurück zum Zitat Godefroid, P., Kiezun, A., Levin, M.Y.: Grammar-based whitebox fuzzing. In: Proceedings of the ACM SIGPLAN Conference on Programming Languages Design and Implementation (PLDI), pp. 206–215 (2008) Godefroid, P., Kiezun, A., Levin, M.Y.: Grammar-based whitebox fuzzing. In: Proceedings of the ACM SIGPLAN Conference on Programming Languages Design and Implementation (PLDI), pp. 206–215 (2008)
13.
Zurück zum Zitat Godefroid, P., Levin, M.Y., Molnar, D.A.: Sage: whitebox fuzzing for security testing. Commun. ACM 55(3), 40–44 (2012)CrossRef Godefroid, P., Levin, M.Y., Molnar, D.A.: Sage: whitebox fuzzing for security testing. Commun. ACM 55(3), 40–44 (2012)CrossRef
14.
Zurück zum Zitat Goedert, J., Cho, Y., Subramaniam, M., Guo, H.F., Xiao, L.: A framework for virtual interactive construction education (vice). Autom. Constr. 20, 76–87 (2011)CrossRef Goedert, J., Cho, Y., Subramaniam, M., Guo, H.F., Xiao, L.: A framework for virtual interactive construction education (vice). Autom. Constr. 20, 76–87 (2011)CrossRef
16.
Zurück zum Zitat Guo, H.F., Subramaniam, M.: Model-based test generation using evolutional symbolic grammar. In: International Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 111–118 (2012) Guo, H.F., Subramaniam, M.: Model-based test generation using evolutional symbolic grammar. In: International Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 111–118 (2012)
17.
Zurück zum Zitat Guo, H.F., Zheng, W., Subramaniam, M.: L2C2: logic-based LSC consistency checking. In: 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP) (2009) Guo, H.F., Zheng, W., Subramaniam, M.: L2C2: logic-based LSC consistency checking. In: 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP) (2009)
18.
Zurück zum Zitat Harel, D.: From play-in scenarios to code: an achievable dream. In: Proceedings of Fundamental Approaches to Software Engineering (FASE), pp. 22–34 (2000) Harel, D.: From play-in scenarios to code: an achievable dream. In: Proceedings of Fundamental Approaches to Software Engineering (FASE), pp. 22–34 (2000)
19.
Zurück zum Zitat Harel, D., Kugler, H.: Synthesizing state-based object systems from lsc specifications. Int. J. Found. Comput. Sci. 13(1), 5–51 (2002)CrossRefMATHMathSciNet Harel, D., Kugler, H.: Synthesizing state-based object systems from lsc specifications. Int. J. Found. Comput. Sci. 13(1), 5–51 (2002)CrossRefMATHMathSciNet
20.
Zurück zum Zitat Harel, D., Maoz, S., Segall, I.: Some results on the expressive power and complexity of LSCs. In: Avron, A., Dershowitz, N., Rabinovich, A. (eds.) Pillars of Computer Science. Lecture Notes in Computer Science, vol. 4800, pp. 351–366. Springer, Berlin, Heidelberg (2008) Harel, D., Maoz, S., Segall, I.: Some results on the expressive power and complexity of LSCs. In: Avron, A., Dershowitz, N., Rabinovich, A. (eds.) Pillars of Computer Science. Lecture Notes in Computer Science, vol. 4800, pp. 351–366. Springer, Berlin, Heidelberg (2008)
21.
Zurück zum Zitat Harel, D., Marelly, R.: Come, Let’s Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer, Berlin, Heidelberg (2003) Harel, D., Marelly, R.: Come, Let’s Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer, Berlin, Heidelberg (2003)
22.
Zurück zum Zitat Helke, S., Neustupny, T., Santen, T.: Automating test case generation from z specifications using isabelle. In: Proceedings of International Conference of Z Users (ZUM), pp. 52–71 (1997) Helke, S., Neustupny, T., Santen, T.: Automating test case generation from z specifications using isabelle. In: Proceedings of International Conference of Z Users (ZUM), pp. 52–71 (1997)
23.
Zurück zum Zitat Hong, H., Cha, S., Lee, I., Sokolsky, O., Ural, H.: Data flow testing as model checking. In: Proceedings of the International Conference on Software Engineering (ICSE), pp. 232–242 (2003) Hong, H., Cha, S., Lee, I., Sokolsky, O., Ural, H.: Data flow testing as model checking. In: Proceedings of the International Conference on Software Engineering (ICSE), pp. 232–242 (2003)
24.
Zurück zum Zitat Hong, H.S., Lee, I., Sokolsky, O., Ural, H.: A temporal logic based theory of test coverage and generation. In: Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS ’02, pp. 327–341 (2002) Hong, H.S., Lee, I., Sokolsky, O., Ural, H.: A temporal logic based theory of test coverage and generation. In: Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS ’02, pp. 327–341 (2002)
26.
27.
Zurück zum Zitat Klose, J., Toben, T., Westphal, B., Wittke, H.: Check it out: on the efficient formal verification of live sequence charts. In: 18th International Conference on Computer Aided Verification (CAV), pp. 219–233 (2006) Klose, J., Toben, T., Westphal, B., Wittke, H.: Check it out: on the efficient formal verification of live sequence charts. In: 18th International Conference on Computer Aided Verification (CAV), pp. 219–233 (2006)
28.
Zurück zum Zitat Krenn, W., Schlick, R., Aichernig, B.K.: Mapping UML to labeled transition systems for test-case generation. In: 8th International Symposium on Formal Methods for Components and Objects, pp. 186–207. Springer, Berlin, Heidelberg (2009) Krenn, W., Schlick, R., Aichernig, B.K.: Mapping UML to labeled transition systems for test-case generation. In: 8th International Symposium on Formal Methods for Components and Objects, pp. 186–207. Springer, Berlin, Heidelberg (2009)
29.
Zurück zum Zitat Kumar, R., Mercer, E.: Improving live sequence chart to automata translation for verification. Electron. Commun. EASST 10, 1–14 (2008) Kumar, R., Mercer, E.: Improving live sequence chart to automata translation for verification. Electron. Commun. EASST 10, 1–14 (2008)
30.
Zurück zum Zitat L\(\ddot{\rm a}\)mmel, R., Schulte, W.: Controllable combinatorial coverage in grammar-based testing. In: Testing of Communicating Systems. Lecture Notes in Computer Science, vol. 3964, pp. 19–38. Springer, Berlin, Heidelberg (2006) L\(\ddot{\rm a}\)mmel, R., Schulte, W.: Controllable combinatorial coverage in grammar-based testing. In: Testing of Communicating Systems. Lecture Notes in Computer Science, vol. 3964, pp. 19–38. Springer, Berlin, Heidelberg (2006)
31.
Zurück zum Zitat Legeard, B., Peureux, F., Utting, M.: Controlling test case explosion in test generation from b formal models. Softw. Test. Verif. Reliab. (STVR) 14(2), 81–103 (2004)CrossRef Legeard, B., Peureux, F., Utting, M.: Controlling test case explosion in test generation from b formal models. Softw. Test. Verif. Reliab. (STVR) 14(2), 81–103 (2004)CrossRef
32.
Zurück zum Zitat Liu, S., Li, L., Guo, H.F.: Generating test cases via model-based simulation. In: 13th IEEE International Conference on Information Reuse and Integration, pp. 17–24 (2012) Liu, S., Li, L., Guo, H.F.: Generating test cases via model-based simulation. In: 13th IEEE International Conference on Information Reuse and Integration, pp. 17–24 (2012)
33.
Zurück zum Zitat Majumdar, R., Xu, R.G.: Directed test generation using symbolic grammars. In: The ACM SIGSOFT Symposium on the Foundations of Software Engineering: Companion Papers, pp. 553–556 (2007) Majumdar, R., Xu, R.G.: Directed test generation using symbolic grammars. In: The ACM SIGSOFT Symposium on the Foundations of Software Engineering: Companion Papers, pp. 553–556 (2007)
34.
Zurück zum Zitat Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: a proof assistant for higher-order logic. Lecture Notes in Computer Science, vol. 2283. Springer, Berlin, Heidelberg (2002) Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: a proof assistant for higher-order logic. Lecture Notes in Computer Science, vol. 2283. Springer, Berlin, Heidelberg (2002)
35.
Zurück zum Zitat Offutt, J., Liu, S., Abdurazik, A., Ammann, P.: Generating test data from state based specifications. J. Softw. Test. Verif. Reliab. 13, 25–53 (2003)CrossRef Offutt, J., Liu, S., Abdurazik, A., Ammann, P.: Generating test data from state based specifications. J. Softw. Test. Verif. Reliab. 13, 25–53 (2003)CrossRef
36.
37.
Zurück zum Zitat Pemmasani, G., Guo, H.F., Dong, Y., Ramakrishnan, C., Ramakrishnan, I.: Online justification for tabled logic programs. In: The 7th International Symposium on Functional and Logic Programming, pp. 24–38 (2004) Pemmasani, G., Guo, H.F., Dong, Y., Ramakrishnan, C., Ramakrishnan, I.: Online justification for tabled logic programs. In: The 7th International Symposium on Functional and Logic Programming, pp. 24–38 (2004)
38.
Zurück zum Zitat Rothermel, G., Harrold, M.J.: A safe, efficient regression test selection technique. ACM Trans. Softw. Eng. Methodol. 6, 173–210 (1997)CrossRef Rothermel, G., Harrold, M.J.: A safe, efficient regression test selection technique. ACM Trans. Softw. Eng. Methodol. 6, 173–210 (1997)CrossRef
39.
Zurück zum Zitat Rothermel, G., Harrold, M.J., von Ronne, J., Hong, C.: Empirical studies of test suite reduction. J. Softw. Test. Verif. Reliab. 4, 219–249 (2002)CrossRef Rothermel, G., Harrold, M.J., von Ronne, J., Hong, C.: Empirical studies of test suite reduction. J. Softw. Test. Verif. Reliab. 4, 219–249 (2002)CrossRef
40.
Zurück zum Zitat Sirer, E.G., Bershad, B.N.: Using production grammars in software testing. In: 2nd Conference on Domain Specific Languages, pp. 1–13 (1999) Sirer, E.G., Bershad, B.N.: Using production grammars in software testing. In: 2nd Conference on Domain Specific Languages, pp. 1–13 (1999)
41.
Zurück zum Zitat Sun, J., Dong, J.S.: Model checking live sequence charts. In: The 10th IEEE International Conference on Engineering of Complex Computer Systems, pp. 529–538 (2005) Sun, J., Dong, J.S.: Model checking live sequence charts. In: The 10th IEEE International Conference on Engineering of Complex Computer Systems, pp. 529–538 (2005)
42.
Zurück zum Zitat Tan, L., Sokolsky, O., Lee, I.: Specification-based testing with linear temporal logic. In: Proceedings of IEEE International Conference on Information Reuse and Integration (IRI’04), pp. 493–498 (2004) Tan, L., Sokolsky, O., Lee, I.: Specification-based testing with linear temporal logic. In: Proceedings of IEEE International Conference on Information Reuse and Integration (IRI’04), pp. 493–498 (2004)
43.
Zurück zum Zitat Toben, T., Westphal, B.: On the expressive power of LSCs. In: The 32nd Conference on Current Trends in Theory and Practice of Computer Science, pp. 33–43 (2006) Toben, T., Westphal, B.: On the expressive power of LSCs. In: The 32nd Conference on Current Trends in Theory and Practice of Computer Science, pp. 33–43 (2006)
44.
Zurück zum Zitat Utting, M., Legeard, B.: Practical Model-Based Testing: A Tools Approach. Morgan-Kaufmann, San Francisco, CA, USA (2007) Utting, M., Legeard, B.: Practical Model-Based Testing: A Tools Approach. Morgan-Kaufmann, San Francisco, CA, USA (2007)
46.
Zurück zum Zitat Zheng, W.: Consistency checking on LSC specifications. Master Thesis, University of Nebraska at Omaha, Omaha (2009) Zheng, W.: Consistency checking on LSC specifications. Master Thesis, University of Nebraska at Omaha, Omaha (2009)
Metadaten
Titel
Model-based test generation using extended symbolic grammars
verfasst von
Hai-Feng Guo
Mahadevan Subramaniam
Publikationsdatum
01.08.2014
Verlag
Springer Berlin Heidelberg
Erschienen in
International Journal on Software Tools for Technology Transfer / Ausgabe 4/2014
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-014-0316-3

Weitere Artikel der Ausgabe 4/2014

International Journal on Software Tools for Technology Transfer 4/2014 Zur Ausgabe