The FME Lucas Award goes to Jeremy Dick and Alain Faivre for their paper
Automating the generation and sequencing of test cases from model-based specifications
published at the First International Symposium of Formal Methods Europe (FME’93).
*Jeremy Dick receives the Lucas Award*
The FME Awards Committee motivated its decision as follows:
Dick and Faivre’s paper is a ground-breaking contribution to automation of testing based on formal specifications, a successful line of research that have added further value to the development of a formal specification. Prior to this paper, automation of testing had been developed for finite state systems and algebraic specifications. This paper presents automated techniques for model-based (sometimes called state-based) specifications, illustrated using VDM. This remarkable piece of work addressed all the aspects of a testing campaign: test-cases identification, test sequencing, generation of test values, and verification of the results against the formal specification. The core idea is the construction of a finite state automaton, using a special DNF partition of the operations domains, and then a partition of the system states. The paper has amassed hundreds of citations, and the approach has been, and is currently, widely used for quite a number of formal notations.
*Jeremy Dick at FM2016*
The paper is available here.