Automatic synthesis of a voting machine design

摘要: Synthesis from specification has long been considered the “holy grail” of the design process. Instead of implementing a design by hand, we prefer to provide a high-level description of the design, and have the implementation automatically generated. Synthesis also eliminates the need for verification, since the synthesized design is correct-byconstruction. We apply two methods of synthesis to the design of an accurate and reliable voting machine. In the first approach, we use an automata-theoretic approach to perform synthesis from a linear temporal logic specification. In the second approach, we use a modified version of the L* algorithm to perform synthesis from scenarios. We compare the two approaches in terms of effort required and results produced, and suggest a third alternative combining aspects of each.