From: Albert Camilleri <ac@com.hp.hpl.hplb>
Message-Id: <9201311111.AA26256@eeyore.hpl.hp.com>
Subject: Re: Query about testing
To: ramu@com.mot.corp.cadsun
Date: Fri, 31 Jan 92 11:11:44 GMT
Cc: info-hol@edu.ucdavis.cs
In-Reply-To: <9201201606.AA17227@cadsun.corp.mot.com>; from "ramu@cadsun.corp.mot.com" at Jan 20, 92 10:06 am

> Ramu@mot.com writes.....

>
> > Given a specification of system, can a theorem prover be used at any
> > stage to perform specification-dependent testing?  Formal testing is
> > mostly like to fault-detection, where one wants to detect undesirable
> > states of a computation.

> > I'd welcome pointers to published papers or technical reports in this
> > area.

I appologise for taking so long to reply to this query, but I have been away.

I'm not sure I understand the terminology `formal testing', but if one
interpretation of it concerns the execution of (formal) specifications, then
some of my earlier work might be of interest.  This concerns the translation
of a certain subset of hardware specifications (written as HOL functions or
relations) to ML functions which can then be executed for facilitating
understanding of the specifications as part of the proof process.

The kind of simulation this would offer, therefore, is based on discrete value
simulation rather than symbolic. The work is of course specific to HOL, mainly
derived from the fact that relations are often used instead of functions, and
that higher order logic specifications cannot in general always be executed.

My PhD dissertation, goes through a reasonable (though maybe by now somewhat
outdated) survey of other approaches, and discusses their facilities for
executing specifications, e.g. this is straighttforward with the Boyer-Moore
prover. The work is described in the following literature. If you'd like me to
send you copies of any of it just email me your snail-mail address and let me
know what you'd like copies of.

Best Regards
Albert

-----------

Camilleri A. J., `Executing Behavioural Definitions in Higher Order Logic',
PhD Dissertation, Technical Report No. 140, University of Cambridge
Computer Laboratory, July 1988.

Camilleri A. J., `Simulation as an aid to Verification using the HOL Theorem
Prover', in "Design Methodologies for VLSI and Computer Architecture",
Edwards D. (ed.), North-Holland, Amsterdam, 1989, pp. 147-168, Proceedings
of the IFIP TC-10 International Working Conference, Pisa, Italy,
19-21 September 1988.

Camilleri A. J., `Simulating Hardware Specifications within a Theorem-Proving
Framework', International Journal of Computer Aided VLSI Design, Vol. 2,
No. 3, pp. 315--337, 1990.