[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Re: constructing unit tests based on tlc models (tla+ specs)

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

On Monday, April 6, 2020 at 4:32:33 PM UTC+1, Alex Tim wrote:
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.

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/16f9f5d5-7817-47fd-aa22-ba20b9aeecd5%40googlegroups.com.