Your browser does not support JavaScript!
http://iet.metastore.ingenta.com
1887

Software testing based on formal specifications: a theory and a tool

Software testing based on formal specifications: a theory and a tool

For access to this article, please select a purchase option:

Buy article PDF
£12.50
(plus tax if applicable)
Add to cart
Buy Knowledge Pack
10 articles for £75.00
(plus taxes if applicable)
Add to cart

IET members benefit from discounts to all IET publications and free access to E&T Magazine. If you are an IET member, log in to your account and the discounts will automatically be applied.

Learn more about IET membership 

Recommend Title Publication to library

You must fill out fields marked with: *

Librarian details
Name:*
Email:*
Your details
Name:*
Email:*
Department:*
Why are you recommending this title?
Select reason:
 
 
 
 
 
Software Engineering Journal — Recommend this title to your library

Thank you

Your recommendation has been sent to your librarian.

© The Institution of Electrical Engineers
Published

This paper addresses the problem of constructing test data sets from formal specifications. Starting from a notion of an ideal exhaustive test data set, which is derived from the notion of satisfaction of the formal specification, we show how to select by refinements a practicable test set, i.e. computable, while not rejecting correct programs (unbiased) and accepting only correct programs (valid), when assuming certain hypotheses. The hypotheses play an important role; they formalise common test practices and they express the gap between the success of the test and correctness; the size of the test set depends on the strength of the hypotheses. The paper shows an application of this theory for algebraic specifications and presents the actual procedures used to mechanically product such test sets, using Horn clause logic. These procedures are embedded in an interactive system, which, given some general hypothesis schemes and an algebraic specification, produces a test set and the corresponding hypotheses.

Inspec keywords: formal specification; program testing

Other keywords: test data sets; common test practices; practicable test set; interactive system; Horn clause logic; formal specifications; algebraic specifications

Subjects: Diagnostic, testing, debugging and evaluating systems; Software engineering techniques; Programming and algorithm theory

References

    1. 1)
      • E.J. Weyuker . On testing non testable programs. Comput. J. , 4 , 465 - 470
    2. 2)
      • L. Bougé , N. Choquet , L. Fribourg , M.C. Gaudel . Test sets generation from algebraic specifications using logic programming. J. Syst. Softw. , 4 , 343 - 360
    3. 3)
      • J.B. Goodenough , S.L. Gerhart . Towards a theory of test data selection. IEEE Trans. , 2
    4. 4)
      • J. Gannon , P. McMullin , R. Hamlet . Dataabstraction implementation, specification, and testing. ACM Trans. Program. Lang. Syst. , 3 , 211 - 223
    5. 5)
      • S. Kaplan . Conditional rewrite rules. Theoretical Comput. Sci. , 175 - 193
    6. 6)
      • Dauchy, P., Marre, B.: `Test data selection from the algebraic specification of a module of an automatic subway', 638, LRI Report, January 1991.
    7. 7)
      • J. Goguen , J. Thatcher , E. Wagner , R.T. Yeh . (1978) An initial algebra approach to the specification, correctness, and implementation of abstract data types, Current trends in programming methodology.
    8. 8)
      • Bougé, L., Choquet, N., Fribourg, L., Gaudel, M.C.: `Application of PROLOG to test sets generation from algebraic specifications', Proc. Int. Joint Conf. on Theory and Practice of Software Development (TAPSOFT), March 1985, Berlin, Germany, (see also Lect. Notes Comput. Sci., 186, pp. 246–260, Springer-Verlag, and Internal Report LRI 176).
    9. 9)
      • L. Fribourg , K. Fuchi , M. Nivat . (1988) Prolog with simplification, Programming of future generation computers.
    10. 10)
      • M.H. Van Emden , K. Yukawa . Logic programming with equations. Logic Program. , 265 - 268
    11. 11)
      • Gerhart, S.: `Software engineering perspectives on Prolog', TR-85-13, Technical Report, July 1985, Wang Institute of Graduate Studies.
    12. 12)
      • Pesch, H., Schnupp, P., Schaller, H., Spirk, A.P.: `Test case generation using Prolog', Int. Conf. on Software Engineering, 1985, London, UK, p. 252–258, (ICSE).
    13. 13)
      • Geser, A., Hussmann, H.: `Experiences with the RAP system—a specification interpreter combining term rewriting and resolution techniques', Proc. ESOP 86 Conf., 1986, 213, p. 339–350, see also Lect. Notes Comput. Sci..
    14. 14)
      • Choquet, N.: `Test data generation using a PROLOG with constraints', IEEE Catalog Number 86TH0144-6, Workshop on Software Testing, July 1986, Banff, Canada, p. 132–141.
    15. 15)
      • D. Sannella , A. Tarlecki . On observational and algebraic specification. J. Comput. Syst. Sci. , 150 - 178
    16. 16)
      • Naish, L.: `An introduction to MU-PROLOG', 82/2, Technical Report, 1982.
    17. 17)
      • RUBAUX, J.P.: 'Rapport final d'étude du poste de generation de test'. ASA RATP Paris, Direction des Equipements Electriques, TT-SEL/89-183/JPR, France.
    18. 18)
      • S. Kamin . Final data types and their specification. ACM Trans. Program. Lang. Syst. , 5 , 97 - 123
    19. 19)
      • Kowalski, R.: `Logic programming', Proc. IFIP 1983, p. 133–145.
    20. 20)
      • Dincbas, M., Le pape, J.P.: `Metacontrol in logic programs in METALOG', 5th Generation Conf., November 1984, Tokyo, Japan.
    21. 21)
      • Hussmann, H.: `Unificiation in conditional-equational the ories', MIP-8502, Technical Report, January 1985, (see also Proc. EUROCAL 85 Conf., Linz).
    22. 22)
      • Deransart, P.: `An operational algebraic semantics of PROLOG programs', Proc. Programmation en Logique, March 1983, France, Perros-Guirrec, CNET-Lannion.
    23. 23)
      • Marre, B.: `Génération automatique de jeux de tests, une solution: Spécifications algébriques et Programmation logique', Proc. Programmation en Logique, May 1989, Tregastel, CNET-Lannion France, p. 213–236.
    24. 24)
      • SCULLARD, G.T.: 'Test case selection using VDM'. VDM '88, Dublin, Eire, 1988 (see also Lect. Notes Comput. Sci., 1988, 328, pp. 178-186).
    25. 25)
      • Rigal, G.: `Generating acceptance tests from SADT/SPECIF IGL', Technical Report, August 1986.
    26. 26)
      • Schoett, O.: `Data abstraction and the correctness of modular programming', 1986, PhD Thesis, University of Edinburgh, UK.
    27. 27)
      • Wild, C.: `The use of generic constraint logic programming for software testing and analysis', Series 88-02, Technical Report, February 1988, Department of Computer Science, Old Dominion University, Norfolk, Virginia, (see also Proc. 2nd ACM-IEEE Workshop on Software Testing, Verification, and Analysis, Banff, Canada, July 1988).
    28. 28)
      • R. Hennicker . Observational implementation of algebraic specifications. Acta Inform. , 3 , 187 - 230
    29. 29)
      • Gerrard, C.P., Coleman, D., Gallimore, R.: `Formal specification and design time testing', Technical Report, June 1985, Software Science Ltd., 1985 (see also IEEE Trans., 1990, SE-16, (1)).
    30. 30)
      • L. Naish . Negation and control in Prolog. Lect. Notes Comput. Sci.
    31. 31)
      • Bernot, G.: `A formalism for test with oracle based on algebraic specifications', 89-4, LIENS Report, May 1989, LIENS/DMI.
    32. 32)
      • Fribourg, L.: `SLOG: a logic programming language interpreter based on clausal superposition and rewriting', Int. Symp. on Logic Programming, July 1985, Boston, Massachusetts.
    33. 33)
      • Weyuker, E.J.: `The oracle assumption of program testing', Proc. 13th Hawaii Int. Conf. on System Sciences, 1980, Hawaii, 1, p. 44–49.
    34. 34)
      • Gaudel, M.-C., Marre, B.: `Algebraic specifications and software testing: theory and application', 407, LRI Report, February 1988, (see also Proc. IEEE-ACM Workshop on Software Testing, Banff, Canada, July 1988).
http://iet.metastore.ingenta.com/content/journals/10.1049/sej.1991.0040
Loading

Related content

content/journals/10.1049/sej.1991.0040
pub_keyword,iet_inspecKeyword,pub_concept
6
6
Loading
Print this page
This is a required field
Please enter a valid email address