Beyond the Verification Approach: The Synthesis Approach
This work has been partially supported by the Natural Sciences and Engineering Research Council of Canada and the Fonds pour la formation de chercheurs et l'aide à la recherche (FCAR).
Synthesis approaches involve deriving a program from a high-level specification. This can be accomplished by using synthesis algorithms that are well adapted to a particular application domain. Efficiency of synthesis algorithms may be demonstrated by experiments done in different settings. Such experiments help to bridge the gap between empirical practices and formal methods. We present an academic experiment that constitutes a first step toward the performance study of synthesis algorithms that allow verification of properties while generating controllers for discrete-event systems. The goal of this experiment is to show the limitations of synthesis algorithms and compare algorithms between them.
