SSP Group Meeting
Wednesday, April 7th, 11am-12pm
Division of Informatics, 80 South Bridge, Room F13
Oracles for Interpreting Test Results
Patricia Machado
Specification-based testing is concerned with deriving testing
information from formal specifications of programs. Several works in
this area have pointed out that testing can be successfully applied in
the formal development of software. However, a great effort is still
needed in order to have testing as a standard activity in formal
frameworks. For instance, the accurate interpretation of testing results
seems to be a crucial a point.
In this talk, we will discuss the oracle problem in the context of
algebraic specifications expressed in first order logic. Oracles are
decision procedures to interpret the results of a testing experiment. A
proposed solution to the oracle problem will also be presented.
Here are the references I mentioned during the talk:
- J. Bicarregui, J. Dick, B Matthews and E. Woods. Making the most of
formal specification through animation, testing and proof. Science of
Computer Programming, 29:53-78, 1997.
- M. Gaudel. Testing can be formal, too. TAPSOFT'95. Lecture Notes in
Computer Science, Springer, 1995.
Gaudel et al. have done some work on testing Prolog programs as well.
All concrete examples of their theory are given in Prolog. If you would
like further references just let me know.
I have a paper where you can find more details (theorems, proofs, examples
and so on) about my talk.
- P. Machado. On Oracles for Interpreting Test Results against Algebraic
Specifications. AMAST'98, Lecture Notes in Computer Science, 1998
But, of course, for the lack of space, this paper does not present many
details and assumes some previous knowledge of Algebraic Specifications.
So, we also have a LFCS technical report with the same title where most of
concepts and results are more carefully presented. Hopefully, this report
will be online in the next couple of weeks.
The paper below just discusses a possible way of applying tests for
verifying refinement steps. No concrete methods, just identifies some
possible barriers.
- P. Machado. Testing in Stepwise Formal Development. WMF'98, Brazil.
1998.