First FME Lucas Award to Dick and Faivre

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.

Author: Einar Broch Johnsen