Reactive Synthesis in Action

Introduction

Bugs in software systems pose a huge and growing cost on society, not only in economic terms but also in direct risk to human lives. Reactive synthesis is a new technology to automatically generate correct-by-construction software. Unlike testing and formal verification, which require advance investment in an implementation, reactive synthesis generates a correct implementation directly from its formal specification.

Current State of Reactive Synthesis

Despite its potential to reduce software development costs and at the same time increase the confidence one may have in the correctness of software, to date, no application of reactive synthesis has been examined outside academic labs.

Objectives of the SYNTACT PoC

The SYNTACT PoC will put reactive synthesis technologies to test in industrial beta-sites and will thus:

1. Generate and disseminate know-how on the use of reactive synthesis in practice.
2. Identify and address product and process obstacles.
3. Build a community of parties that are interested in the promotion and transfer of reactive synthesis technologies from academia to industry.
4. Lay a foundation to guide future research, standardization, collaboration, and industry investment in reactive synthesis technologies.

Expected Outcomes

We expect the SYNTACT PoC to advance the state-of-the-practice in reactive synthesis and thus start paving the way for its adoption in industry. Its expected outcomes include:

• Several industrial systems that were developed using synthesis.
• Case-study reports describing the beta-sites projects.
• Training materials.
• A new set of real benchmark specifications.
• Estimations of the potential return on investment in deploying reactive synthesis.
• Draft standardization documents.

Conclusion

As more and more aspects of modern life depend on the correctness of software, the SYNTACT PoC will directly introduce the reactive synthesis correct-by-construction new perspective and tools to the industrial settings, as a timely step towards its broad future adoption.