constructing unit tests based on tlc models (tla+ specs)

[Alex Tim]

Hi all

I think its not a new idea constructing tests for models...

One deal is proving the correctness of a spec and quite another - checking that a real program (implementation) satisfies it.

Can someone give useful references to relevant publications?

Thanks in advance.

[Leslie Lamport]

I have observed that because unit tests are written by the programmer,

they will test only for problems that the programmer has already

foreseen.  Therefore, they can only test for simple coding errors, not

for whether the unit does what it really needs to do.  

In the real world, the TLA+ spec engineers write mirrors the

implementation that they have in mind.  So, a program unit will

usually correspond to parts of the spec, often directly implementing

an action in the TLA+ spec.  Writing a unit test that checks that the

unit does correctly implement the action should be a great way to

catch errors.  This fits well with the accepted idea that unit tests

should be written before one writes the code, since one should also

understand how the code implements the spec before writing the code.

This idea can be tried by engineers right now when they write their

unit tests to see how well it works.  If it works as well as I think

it should, one can think about writing tools to help.

I have not managed to convince any engineers to try it, and I don't

know of its being done anywhere--except in systems for proving the

correctness of the code, which are still too expensive to use in most

applications.

Leslie

[Ron Pressler]

There are several ways to check the conformance of an implementation to a spec, with varying degrees of soundness and scalability. If you are interested in test generation, this is a 1993 paper I found on the subject (uses VDM specs):

Jeremy Dick, Alain Faivre, Automating the Generation and Sequencing of Test Cases from Model-Based Specifications, FME '93

- Ron