nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Formal Specifications and Software Testing, a Fruitful Convergence

verfasst von : Marie-Claude Gaudel

Erschienen in: Formal Methods. FM 2019 International Workshops

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

This paper gives some account of the evolution of ideas and the main advances in the domain of software testing based on formal specifications and reports some personal anecdotes on my activity in this field. Going back to the seventies, being slightly caricatural, software testing was perceived, on the one hand, by its actors as an empirical activity that had nothing to gain from formal methods, on the other hand, by the advocates of these methods as doomed to disappear based on the belief that in the long run programs will be correct by construction. Currently, these two communities haven’t yet reached a complete consensus. But fortunately there have been some significant moves from both sides and various success stories that allow saying that there is a fruitful convergence toward testing methods based on formal specifications.

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!

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

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

Vorheriges Kapitel Specification with Class: A Brief History of Object-Z

Nächstes Kapitel From Manuscripts to Programming Languages: An Archivist Perspective

This note can be seen at https://www.cs.utexas.edu/users/EWD/ where it has no date. But one can bracket it between two dated EWDs: EWD 292, 31 Aug 1970, and EWD 306, 16th March 1971 (thanks to Jeremy Gibbons for the hint).

During my stay there (1981–1983) I interacted with a group of engineers who developed the software of a telephone switching system. I was impressed by their professionalism. They motivated me to pursue this line of research.

A (not so funny) anecdote is that some years later, being back as a professor in a university, I visited the same place with a Ph.D. student, searching for challenging case studies. Mood and people had changed and the head of the group explained that their goal was to be first on the market and their development strategy was “quick an dirty”. To that the Ph.D. student replied that “dirty we can do, but quick I am not sure”. The meeting was unproductive...

This is similar to the issue of lifting computational types and values to the logical level in Hoare’s logic.

IWPTS: 1983–1996; IWTCS: 1997–1999, TESTCOM: 2000–2009, ICTSS: 2010-now.

This series of workshops (Formal Approaches to Testing of Software) took place in 2001–2007.

A notable omission here is the corpus of research on testing based on FSM (Finite State Machines), which has been considerably influential since the sixties both in hardware and in software testing. For an excellent survey with some historical indications see [28].

Barnett, M., Grieskamp, W., Nachmanson, L., Schulte, W., Tillmann, N., Veanes, M.: Towards a tool environment for model-based testing with AsmL. In: Petrenko, A., Ulrich, A. (eds.) FATES 2003. LNCS, vol. 2931, pp. 252–266. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24617-6_18CrossRef

Bernot, G., Gaudel, M.C., Marre, B.: Software testing based on formal specifications: a theory and a tool. Softw. Eng. J. 6(6), 387–405 (1991)CrossRef

Bougé, L.: Modeling the notion of program testing; application to test set generation. Theses, Université Pierre et Marie Curie - Paris VI, October 1982. https://tel.archives-ouvertes.fr/tel-00416558

Bougé, L., Choquet, N., Fribourg, L., Gaudel, M.C.: Application of PROLOG to test sets generation from algebraic specifications. In: Ehrig, H., Floyd, C., Nivat, M., Thatcher, J. (eds.) TAPSOFT 1985. LNCS, vol. 186, pp. 261–275. Springer, Heidelberg (1985). https://doi.org/10.1007/3-540-15199-0_17CrossRef

Brinksma, E.: A theory for the derivation of tests. In: Proceedings of 8th International Conference on Protocol Specification, Testing and Verification, pp. 63–74. North-Holland (1988)

Brucker, A.D., Wolff, B.: On theorem prover-based testing. Formal Asp. Comput. 25(5), 683–721 (2013)MathSciNetCrossRef

Cavalcanti, A., Gaudel, M.-C.: Testing for refinement in CSP. In: Butler, M., Hinchey, M.G., Larrondo-Petrie, M.M. (eds.) ICFEM 2007. LNCS, vol. 4789, pp. 151–170. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-76650-6_10CrossRef

Cavalcanti, A., Gaudel, M.C.: Testing for refinement in Circus. Acta Inf. 48(2), 97–147 (2011)MathSciNetCrossRef

CCITT: Functional specification and description language (SDL), Recommendation Z.100–Z.104 (1984)

10.

Chaudron, M.R.V., Tretmans, J., Wijbrans, K.: Lessons from the application of formal methods to the design of a storm surge barrier control system. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1709, pp. 1511–1526. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48118-4_30

11.

Dauchy, P., Gaudel, M.C., Marre, B.: Using algebraic specifications in software testing: a case study on the software of an automatic subway. J. Syst. Softw. 21(3), 229–244 (1993)CrossRef

12.

DeMillo, R.A.: Software testing. In: Encyclopedia of Computer Science, pp. 1645–1649. John Wiley and Sons Ltd., GBR (2003)

13.

DeMillo, R.A., Upton, R.J., Perlis, A.J.: Social processes and proofs of theorems and programs. Math. Intell. 3(1), 31–40 (1980). https://doi.org/10.1007/BF03023394MathSciNetCrossRefMATH

14.

Dick, J., Faivre, A.: Automating the generation and sequencing of test cases from model-based specifications. In: Woodcock, J.C.P., Larsen, P.G. (eds.) FME 1993. LNCS, vol. 670, pp. 268–284. Springer, Heidelberg (1993). https://doi.org/10.1007/BFb0024651CrossRef

15.

Dijkstra, E.W.: The humble programmer. Commun. ACM 15(10), 859–866 (1972)CrossRef

16.

Dubois, C., Giorgetti, A.: Tests and proofs for custom data generators. Formal Aspects Comput. 30(6), 659–684 (2018). https://doi.org/10.1007/s00165-018-0459-1MathSciNetCrossRefMATH

17.

Feliachi, A., Gaudel, M.-C., Wenzel, M., Wolff, B.: The Circus testing theory revisited in Isabelle/HOL. In: Groves, L., Sun, J. (eds.) ICFEM 2013. LNCS, vol. 8144, pp. 131–147. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-41202-8_10CrossRef

18.

Fraser, G., Wotawa, F., Ammann, P.: Issues in using model checkers for test case generation. J. Syst. Softw. 82(9), 1403–1418 (2009)CrossRef

19.

Gannon, J.D., McMullin, P.R., Hamlet, R.G.: Data-abstraction implementation, specification, and testing. ACM Trans. Program. Lang. Syst. 3(3), 211–223 (1981)CrossRef

20.

Gaudel, M.-C., Le Gall, P.: Testing data types implementations from algebraic specifications. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) Formal Methods and Testing. LNCS, vol. 4949, pp. 209–239. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78917-8_7CrossRef

21.

Gaudel, M.C., James, P.R.: Testing algebraic data types and processes: a unifying theory. Formal Asp. Comput. 10(5–6), 436–451 (1998)CrossRef

22.

Hierons, R.M., et al.: Using formal specifications to support testing. ACM Comput. Surv. 41(2), 9:1–9:76 (2009)

23.

Hoare, C.A.R.: How did software get so reliable without proof? In: Gaudel, M.-C., Woodcock, J. (eds.) FME 1996. LNCS, vol. 1051, pp. 1–17. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-60973-3_77CrossRef

24.

Houssais, B.: Verification of an Algol 68 implementation. ACM SIGPLAN Not. 12(6), 117–128 (1977)CrossRef

25.

ISO: Conformance testing methodology and framework. International Standard IS-9646 (1991)

26.

Jalote, P.: Specification and testing of abstract data types. In: IEEE International Computer Software and Applications Conference COMSAC, pp. 508–511 (1983)

27.

Jard, C., Jéron, T.: TGV: theory, principles and algorithms. Int. J. Softw. Tools Technol. Transf. 7(4), 297–315 (2005)CrossRef

28.

Lee, D., Yannakakis, M.: Principles and methods of testing finite state machines-a survey. Proc. IEEE 84(8), 1090–1123 (1996)CrossRef

29.

Legeard, B., Peureux, F.: Generation of functional test sequences from B formal specifications-presentation and industrial case study. In: 16th IEEE International Conference on Automated Software Engineering (ASE 2001), Coronado Island, San Diego, CA, USA, 26–29 November 2001, pp. 377–381. IEEE Computer Society (2001)

30.

Marre, B., Blanc, B.: Test selection strategies for Lustre descriptions in GATeL. Electr. Notes Theor. Comput. Sci. 111, 93–111 (2005)CrossRef

31.

Petiot, G., Kosmatov, N., Botella, B., Giorgetti, A., Julliand, J.: How testing helps to diagnose proof failures. Formal Aspects Comput. 30(6), 629–657 (2018). https://doi.org/10.1007/s00165-018-0456-4MathSciNetCrossRefMATH

32.

Pitt, D.H., Freestone, D.: The derivation of conformance tests from LOTOS specifications. IEEE Trans. Software Eng. 16(12), 1337–1343 (1990)CrossRef

33.

Sarikaya, B., von Bochmann, G.: Some experience with test sequence generation for protocols. In: Protocol Specification, Testing and Verification, Proceedings of the IFIP WG6.1 Second International Workshop on Protocol Specification, Testing and Verification, Idyllwild, CA, USA, 17–20 May 1982, pp. 555–567. North-Holland (1982)

34.

Satpathy, M., Butler, M., Leuschel, M., Ramesh, S.: Automatic testing from formal specifications. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol. 4454, pp. 95–113. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73770-4_6CrossRef

35.

Stocks, P., Carrington, D.A.: Test templates: a specification-based testing framework. In: Proceedings of the 15th International Conference on Software Engineering, Baltimore, Maryland, USA, 17–21 May 1993, pp. 405–414. IEEE Computer Society/ACM Press (1993)

36.

Tretmans, J.: Test generation with inputs, outputs and repetitive quiescence. Softw. Concepts Tools 17(3), 103–120 (1996)MATH

37.

Tretmans, J., van de Laar, P.: Model-based testing with TorXakis. In: Proceedings of 30th CECIIS, the Central European Conference on Information and Intelligent Systems, Varaždin, Croatia, 2–4 October 2019, pp. 247–258 (1987)

38.

Ural, H.: A test derivation method for protocol conformance testing. In: Protocol Specification, Testing and Verification VII, Proceedings of the IFIP WG6.1 Seventh International Conference on Protocol Specification, Testing and Verification, Zurich, Switzerland, 5–8 May 1987, pp. 347–358. North-Holland (1987)

39.

Veanes, M., Campbell, C., Grieskamp, W., Schulte, W., Tillmann, N., Nachmanson, L.: Model-based testing of object-oriented reactive systems with Spec Explorer. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) Formal Methods and Testing. LNCS, vol. 4949, pp. 39–76. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78917-8_2CrossRefMATH

Titel: Formal Specifications and Software Testing, a Fruitful Convergence
verfasst von: Marie-Claude Gaudel
Verlag: Springer International Publishing
Buch: Formal Methods. FM 2019 International Workshops
Print ISBN: 978-3-030-54996-1

Electronic ISBN: 978-3-030-54997-8

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-54997-8_5

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+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"