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

01.02.2015 | Regular Paper

Testing abstract behavioral specifications

verfasst von: Peter Y. H. Wong, Richard Bubel, Frank S. de Boer, Miguel Gómez-Zamalloa, Stijn de Gouw, Reiner Hähnle, Karl Meinke, Muddassar Azam Sindhu

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 1/2015

Einloggen

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

search-config
loading …

Abstract

We present a range of testing techniques for the Abstract Behavioral Specification (ABS) language and apply them to an industrial case study. ABS is a formal modeling language for highly variable, concurrent, component-based systems. The nature of these systems makes them susceptible to the introduction of subtle bugs that are hard to detect in the presence of steady adaptation. While static analysis techniques are available for an abstract language such as ABS, testing is still indispensable and complements analytic methods. We focus on fully automated testing techniques including black-box and glass-box test generation as well as runtime assertion checking, which are shown to be effective in an industrial setting.

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!

Literatur
1.
Zurück zum Zitat Albert, E., Arenas, P., Gómez-Zamalloa, M.: Towards testing concurrent objects in CLP. In: Agostino Dovier and Vítor Santos Costa, editors, Technical Communications of the 28th International Conference on Logic Programming (ICLP’12), vol. 17 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 98–108, Dagstuhl, Germany. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2012) Albert, E., Arenas, P., Gómez-Zamalloa, M.: Towards testing concurrent objects in CLP. In: Agostino Dovier and Vítor Santos Costa, editors, Technical Communications of the 28th International Conference on Logic Programming (ICLP’12), vol. 17 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 98–108, Dagstuhl, Germany. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2012)
2.
Zurück zum Zitat Albert, E., Gómez-Zamalloa, M., Rojas, J.M., Puebla, G.: Compositional CLP-based test data generation for imperative languages. In: LOPSTR 2010 Revised Selected Papers, vol. 6564 of LNCS. Springer-Verlag (2011) Albert, E., Gómez-Zamalloa, M., Rojas, J.M., Puebla, G.: Compositional CLP-based test data generation for imperative languages. In: LOPSTR 2010 Revised Selected Papers, vol. 6564 of LNCS. Springer-Verlag (2011)
3.
Zurück zum Zitat Allan, C., Avgustinov, P., Christensen, A.S., Hendren, L., Kuzins, S., Lhoták, O., de Moor, O., Sereni, D., Sittampalam, G., Tibble, J.: Adding trace matching with free variables to AspectJ. In: Proceedings of the 20th annual ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, OOPSLA ’05, pp. 345–364. ACM, New York (2005) Allan, C., Avgustinov, P., Christensen, A.S., Hendren, L., Kuzins, S., Lhoták, O., de Moor, O., Sereni, D., Sittampalam, G., Tibble, J.: Adding trace matching with free variables to AspectJ. In: Proceedings of the 20th annual ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, OOPSLA ’05, pp. 345–364. ACM, New York (2005)
4.
Zurück zum Zitat Bartetzko, Detlef, Fischer, Clemens, Möller, Michael, Wehrheim, Heike: Jass-Java with assertions. Electron. Notes Theor. Comput. Sci. 55(2), 103–117 (2001)CrossRef Bartetzko, Detlef, Fischer, Clemens, Möller, Michael, Wehrheim, Heike: Jass-Java with assertions. Electron. Notes Theor. Comput. Sci. 55(2), 103–117 (2001)CrossRef
5.
Zurück zum Zitat Chen, F., Roşu, G.: Mop: an efficient and generic runtime verification framework. In: Proceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems and applications, OOPSLA ’07, pp. 569–588. ACM, New York (2007) Chen, F., Roşu, G.: Mop: an efficient and generic runtime verification framework. In: Proceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems and applications, OOPSLA ’07, pp. 569–588. ACM, New York (2007)
6.
Zurück zum Zitat Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model verifier. In: Proceedings of CAV 1999, vol. 1633 of LNCS (1999) Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model verifier. In: Proceedings of CAV 1999, vol. 1633 of LNCS (1999)
7.
Zurück zum Zitat Clarke, D., Diakov, N., Hähnle, R., Johnsen, E.B., Schaefer, I., Schäfer, J., Schlatte, R., Wong, P.Y.H.: Modeling spatial and temporal variability with the HATS abstract behavioral modeling language. In: Bernardo, M., Issarny, V. (eds.) ormal Methods for Eternal Networked Software Systems, vol. 6659 of Lecture Notes in Computer Science, pp. 417–457. Springer-Verlag, Berlin (2011) Clarke, D., Diakov, N., Hähnle, R., Johnsen, E.B., Schaefer, I., Schäfer, J., Schlatte, R., Wong, P.Y.H.: Modeling spatial and temporal variability with the HATS abstract behavioral modeling language. In: Bernardo, M., Issarny, V. (eds.) ormal Methods for Eternal Networked Software Systems, vol. 6659 of Lecture Notes in Computer Science, pp. 417–457. Springer-Verlag, Berlin (2011)
8.
Zurück zum Zitat Colombo, C., Pace, G.J., Schneider, G.: LARVA–safer monitoring of real-time Java Programs (Tool Paper). In: Proceedings of the 2009 Seventh IEEE International Conference on Software Engineering and Formal Methods, SEFM ’09, pp. 33–37, Washington, DC, USA. IEEE Computer Society (2009) Colombo, C., Pace, G.J., Schneider, G.: LARVA–safer monitoring of real-time Java Programs (Tool Paper). In: Proceedings of the 2009 Seventh IEEE International Conference on Software Engineering and Formal Methods, SEFM ’09, pp. 33–37, Washington, DC, USA. IEEE Computer Society (2009)
9.
Zurück zum Zitat de Boer, F.S., de Gouw, S., Johnsen, E.B., Wong, P.Y.H.: Run-time assertion checking of data- and protocol-oriented properties of java programs: an industrial case study. LNCS Transactions on Aspect-Oriented Software Development (TAOSD). Special Issue on Runtime Verification and Analysis. To appear (2013) de Boer, F.S., de Gouw, S., Johnsen, E.B., Wong, P.Y.H.: Run-time assertion checking of data- and protocol-oriented properties of java programs: an industrial case study. LNCS Transactions on Aspect-Oriented Software Development (TAOSD). Special Issue on Runtime Verification and Analysis. To appear (2013)
10.
Zurück zum Zitat de Boer, F.S., de Gouw, S., Wong, P.Y.H.: Run-time verification of coboxes. In: Proceedings of 11th International Conference on Software Engineering and Formal Methods, vol. 8137 of LNCS, pp. 259–273 (2013) de Boer, F.S., de Gouw, S., Wong, P.Y.H.: Run-time verification of coboxes. In: Proceedings of 11th International Conference on Software Engineering and Formal Methods, vol. 8137 of LNCS, pp. 259–273 (2013)
11.
Zurück zum Zitat de Gouw, S., Vinju, J., de Boer, F.: Prototyping a tool environment for run-time assertion checking in JML with Communication Histories. In: Proceedings of the 12th Workshop on Formal Techniques for Java-Like Programs, FTFJP ’10, pp. 6:1–6:7. ACM, New York (2010) de Gouw, S., Vinju, J., de Boer, F.: Prototyping a tool environment for run-time assertion checking in JML with Communication Histories. In: Proceedings of the 12th Workshop on Formal Techniques for Java-Like Programs, FTFJP ’10, pp. 6:1–6:7. ACM, New York (2010)
13.
Zurück zum Zitat Feng, L., Lundmark, S., Meinke, K., Niu, F., Sindhu, M.A., Wong, P.Y.H.: Case studies in learning-based testing. In: Proceedings Twenty Fifth IFIP International Conference on Testing Software and Systems (ICTSS 2013), vol. 8254 of LNCS, pp. 164–179. Springer, New York (2013) Feng, L., Lundmark, S., Meinke, K., Niu, F., Sindhu, M.A., Wong, P.Y.H.: Case studies in learning-based testing. In: Proceedings Twenty Fifth IFIP International Conference on Testing Software and Systems (ICTSS 2013), vol. 8254 of LNCS, pp. 164–179. Springer, New York (2013)
14.
Zurück zum Zitat Gómez-Zamalloa, M., Albert, E., Puebla, G.: Test Case Generation for Object-Oriented Imperative Languages in CLP. Theory and Practice of Logic Programming, 26th Int’l. Conference on Logic Programming (ICLP’10) Special Issue, 10 (4–6):659–674, July (2010) Gómez-Zamalloa, M., Albert, E., Puebla, G.: Test Case Generation for Object-Oriented Imperative Languages in CLP. Theory and Practice of Logic Programming, 26th Int’l. Conference on Logic Programming (ICLP’10) Special Issue, 10 (4–6):659–674, July (2010)
15.
Zurück zum Zitat Hähnle, R.: The abstract behavioral specification language: a tutorial introduction. In: Bonsangue, M., de Boer, F., Giachino, E., Hähnle, R. (eds.) International School on Formal Models for Components and Objects: Post Proceedings, vol. 7866 of Lecture Notes in Computer Science, pp. 1–37. Springer-Verlag, Berlin (2013) Hähnle, R.: The abstract behavioral specification language: a tutorial introduction. In: Bonsangue, M., de Boer, F., Giachino, E., Hähnle, R. (eds.) International School on Formal Models for Components and Objects: Post Proceedings, vol. 7866 of Lecture Notes in Computer Science, pp. 1–37. Springer-Verlag, Berlin (2013)
16.
Zurück zum Zitat Hähnle, R., Schaefer, I., Bubel, R.: Reuse in software verification by abstract method calls. In: Bonacina, M.P. (ed.) Proceedings 24th Conference on Automated Deduction (CADE), Lake Placid, USA, vol. 7898 of Lecture Notes in Computer Science, pp. 300–314. Springer-Verlag, Berlin (2013) Hähnle, R., Schaefer, I., Bubel, R.: Reuse in software verification by abstract method calls. In: Bonacina, M.P. (ed.) Proceedings 24th Conference on Automated Deduction (CADE), Lake Placid, USA, vol. 7898 of Lecture Notes in Computer Science, pp. 300–314. Springer-Verlag, Berlin (2013)
17.
Zurück zum Zitat Hamill, P.: Unit Test Frameworks. O’Reilly Media (2004) Hamill, P.: Unit Test Frameworks. O’Reilly Media (2004)
18.
Zurück zum Zitat Johnsen, E.B., Hähnle, R., Schäfer, J., Schlatte, R., Steffen, M.: ABS: a core language for abstract behavioral specification. In: Aichernig, B., de Boer F.S., Bonsangue, M.M. (eds.) Proceedings 9th International Symposium on Formal Methods for Components and Objects (FMCO 2010), vol. 6957 of LNCS, pp. 142–164. Springer-Verlag, Berlin (2011) Johnsen, E.B., Hähnle, R., Schäfer, J., Schlatte, R., Steffen, M.: ABS: a core language for abstract behavioral specification. In: Aichernig, B., de Boer F.S., Bonsangue, M.M. (eds.) Proceedings 9th International Symposium on Formal Methods for Components and Objects (FMCO 2010), vol. 6957 of LNCS, pp. 142–164. Springer-Verlag, Berlin (2011)
19.
Zurück zum Zitat Einar, B.J., Olaf, O.: An asynchronous communication model for distributed concurrent objects. Softw. Syst. Model. 6(1), 35–58 (2007) Einar, B.J., Olaf, O.: An asynchronous communication model for distributed concurrent objects. Softw. Syst. Model. 6(1), 35–58 (2007)
20.
Zurück zum Zitat King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)CrossRefMATH King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)CrossRefMATH
21.
Zurück zum Zitat Klint, P., van der Storm, T., Vinju, J.: RASCAL: a domain specific language for source code analysis and manipulation. In: Proceedings of the 2009 Ninth IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM ’09, pp. 168–177, Washington, DC, USA. IEEE Computer Society (2009) Klint, P., van der Storm, T., Vinju, J.: RASCAL: a domain specific language for source code analysis and manipulation. In: Proceedings of the 2009 Ninth IEEE International Working Conference on Source Code Analysis and Manipulation, SCAM ’09, pp. 168–177, Washington, DC, USA. IEEE Computer Society (2009)
22.
Zurück zum Zitat Martin, M., Livshits, B., Lam, M.S.: Finding application errors and security flaws using PQL: a program query language. In: Proceedings of the 20th annual ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, OOPSLA ’05, pp. 365–383. ACM, New York (2005) Martin, M., Livshits, B., Lam, M.S.: Finding application errors and security flaws using PQL: a program query language. In: Proceedings of the 20th annual ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, OOPSLA ’05, pp. 365–383. ACM, New York (2005)
23.
Zurück zum Zitat Meinke, K., Niu, F., Sindhu, M.: Learning-based software testing: a tutorial. In: Reiner, H., Jens, K., Tiziana, M., Dietmar, S., Bernhard, S. (eds.) Leveraging Applications of Formal Methods, Verification, and Validation, Communications in Computer and Information Science, pp. 200–219. Springer-Verlag, Berlin (2012) Meinke, K., Niu, F., Sindhu, M.: Learning-based software testing: a tutorial. In: Reiner, H., Jens, K., Tiziana, M., Dietmar, S., Bernhard, S. (eds.) Leveraging Applications of Formal Methods, Verification, and Validation, Communications in Computer and Information Science, pp. 200–219. Springer-Verlag, Berlin (2012)
24.
Zurück zum Zitat Meinke, K., Sindhu, M.: Incremental learning-based testing for reactive systems. In: Proceedings Fifth International Conference on Tests and Proofs (TAP2011), number 6706 in Lecture Notes in Computer Science, pp. 134–151. Springer-Verlag, Berlin (2011) Meinke, K., Sindhu, M.: Incremental learning-based testing for reactive systems. In: Proceedings Fifth International Conference on Tests and Proofs (TAP2011), number 6706 in Lecture Notes in Computer Science, pp. 134–151. Springer-Verlag, Berlin (2011)
25.
Zurück zum Zitat Meinke, K., Sindhu, M.A.: LBTest: a learning-based testing tool for reactive systems. In Proc ICST-13, Sixth IEEE International Conference on Software Testing, Verification and Validation, pp. 447–454. IEEE Computer Society (2013) Meinke, K., Sindhu, M.A.: LBTest: a learning-based testing tool for reactive systems. In Proc ICST-13, Sixth IEEE International Conference on Software Testing, Verification and Validation, pp. 447–454. IEEE Computer Society (2013)
26.
Zurück zum Zitat Nobakht, B., Bonsangue, M.M., de Boer, F.S., de Gouw, S.: Monitoring method call sequences using annotations. In: Proceedings of the 7th international conference on Formal Aspects of Component Software, FACS’10, pp. 53–70. Springer-Verlag, Berlin, Heidelberg (2012) Nobakht, B., Bonsangue, M.M., de Boer, F.S., de Gouw, S.: Monitoring method call sequences using annotations. In: Proceedings of the 7th international conference on Formal Aspects of Component Software, FACS’10, pp. 53–70. Springer-Verlag, Berlin, Heidelberg (2012)
27.
Zurück zum Zitat Terrence, P.: The Definitive ANTLR Reference. Pragmatic Bookshelf (2007) Terrence, P.: The Definitive ANTLR Reference. Pragmatic Bookshelf (2007)
28.
Zurück zum Zitat Pohl, Klaus, Böckle, Günter, Van Der Linden, Frank: Software Product Line Engineering: Foundations, Principles, and Techniques. Springer, New York (2005)CrossRef Pohl, Klaus, Böckle, Günter, Van Der Linden, Frank: Software Product Line Engineering: Foundations, Principles, and Techniques. Springer, New York (2005)CrossRef
29.
Zurück zum Zitat Schaefer, I., Bettini, L., Bono, V., Damiani, F., Tanzarella, N.: Delta-oriented programming of software product lines. In: Proceedings of 14th Software Product Line Conference (SPLC 2010), September (2010) Schaefer, I., Bettini, L., Bono, V., Damiani, F., Tanzarella, N.: Delta-oriented programming of software product lines. In: Proceedings of 14th Software Product Line Conference (SPLC 2010), September (2010)
30.
Zurück zum Zitat Schäfer, J., Poetzsch-Heffter, A.: JCoBox: Generalizing active objects to concurrent components. In: European Conference on Object-Oriented Programming (ECOOP’10), vol. 6183 of Lecture Notes in Computer Science, pp. 275–299. Springer-Verlag, June (2010) Schäfer, J., Poetzsch-Heffter, A.: JCoBox: Generalizing active objects to concurrent components. In: European Conference on Object-Oriented Programming (ECOOP’10), vol. 6183 of Lecture Notes in Computer Science, pp. 275–299. Springer-Verlag, June (2010)
31.
Zurück zum Zitat Wong, P.Y.H., Albert, E., Muschevici, R., Proença, J., Schäfer, J., Schlatte, R.: The ABS tool suite: modelling, executing and analysing distributed adaptable object-oriented systems. J. Soft. Tools Technol. Trans. 14(5), 567–588 (2012)CrossRef Wong, P.Y.H., Albert, E., Muschevici, R., Proença, J., Schäfer, J., Schlatte, R.: The ABS tool suite: modelling, executing and analysing distributed adaptable object-oriented systems. J. Soft. Tools Technol. Trans. 14(5), 567–588 (2012)CrossRef
32.
Zurück zum Zitat Wong, P.Y.H., Diakov, N., Schaefer, I.: Modelling Distributed Adaptable Object Oriented Systems using HATS Approach: A Fredhopper Case Study. In: Proceedings of FoVeOOS 2011, vol. 7421 of LNCS (2012) Wong, P.Y.H., Diakov, N., Schaefer, I.: Modelling Distributed Adaptable Object Oriented Systems using HATS Approach: A Fredhopper Case Study. In: Proceedings of FoVeOOS 2011, vol. 7421 of LNCS (2012)
Metadaten
Titel
Testing abstract behavioral specifications
verfasst von
Peter Y. H. Wong
Richard Bubel
Frank S. de Boer
Miguel Gómez-Zamalloa
Stijn de Gouw
Reiner Hähnle
Karl Meinke
Muddassar Azam Sindhu
Publikationsdatum
01.02.2015
Verlag
Springer Berlin Heidelberg
Erschienen in
International Journal on Software Tools for Technology Transfer / Ausgabe 1/2015
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-014-0301-x

Weitere Artikel der Ausgabe 1/2015

International Journal on Software Tools for Technology Transfer 1/2015 Zur Ausgabe