🚀 go-pugleaf

In article <1992Nov11.120250.12884@cs.tcd.ie> emcdnnll@cs.tcd.ie (Eoin McDonnell) writes:

   Newsgroups: comp.specification
   Path: daffodil!concert!gatech!destroyer!uunet!mcsun!ieunet!tcdcs!emcdnnll
   From: emcdnnll@cs.tcd.ie (Eoin McDonnell)
   Summary: Ref's req'd for use of formal spec's in software testing
   Keywords: Testing,formal specification
   Organization: Computer Science, Trinity College Dublin
   Date: Wed, 11 Nov 1992 12:02:50 GMT
   Lines: 10


   Hi all,

   I'm interested in finding out how formal specifications can be used to
   help design test programmes for software.   Any references would be
   appreciated.

   Thanks,

   Eoin Mc Donnell.               emcdnnll@cs.tcd.ie



Formal specs can come into play in testing in two ways. 

First, all testing depends upon the existence of an "oracle" to
examine test inputs and program outputs and detect the presence of
failures (incorrect results).  This oracle is most often provided via
human inspection of the input/output data or via textual comparison
against a file of previously recorded expected results.  However, any
scheme for animating/evaluating specifications can also help to serve
as an oracle (at the risk of allowing errors in the specification that
were faithfully copied into the design to go undetected).  Such
automated aids can be of immense use in situations where many
thousands or tens of thousands of tests are being run.  



Second, the spec can be used as the source of information from which
test cases are generated or against which the suitability of tests
sets is measured.  Here's a sampler of several very different
approaches to such specification-based testing:

@article{Bouge/test-gen-logic,
   author = "L. Bouge and N. Choquet and L. Fribourg and M. C. Gaudel",
   journal = "Journal of Systems and Software",
   month = Nov,
   number = "4",
   pages = "343--360",
   title = "Test Sets Generation From Algebraic Specifications Using
		Logic Programming",
   volume = "6",
   year = "1986"
}

@article{Gannon/daists,
   author = "John Gannon and Paul Mc{M}ullin and Richard Hamlet",
   journal = "ACM Transactions on Programming Languages and Systesm",
   month = Jul,
   number = "3",
   pages = "211--223",
   title = "Data-Abstraction Implementation, Specification, and Testing",
   volume = "3",
   year = "1981"
}


@techreport{Luckham/anna-debugging,
   author = "David C. Luckham and Sriram Sankar and Shuzo Takahashi",
   address = "Stanford CA",
   institution = "Stanford University Computer Systems Laboratory",
   month = Apr,
   number = "CSL--TR--89--379",
   title = "Two Dimensional Pinpointing: An Application of Formal
      Specification to Debugging Packages",
   year = "1989
"
}

@article{Wild/refinement-jtvr,
   author = "Christian Wild and Steven Zeil and Ji Chen and Gao Feng",
   journal = "{\rm to appear in} Journal of Software Testing,
   Verification, and Reliability",
   title = "Employing Accumulated Knowledge to Refine Test Cases",
   year = "1992-93"
   note = "also available as Old Dominion University report TR-91-14"
}

(Well, I couldn't resist putting ONE of my own papers in there.)

                                                     Steve Zeil