#	Pagina
attuale pagina	/open-h2020/projects/193554/results.html

Report

Teaser, summary, work performed and final results

Periodic Reporting for period 2 - SYNTECH (Synthesis Technologies for Reactive Systems Software Engineers)

Teaser

Summary

Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from a given specification. Examples of these systems include the software controllers of robotic systems. Despite recent advancements on the theory and algorithms of reactive synthesis, e.g., efficient synthesis for the GR(1) fragment of linear temporal logic, many challenges remain in bringing reactive synthesis technologies to the hands of software engineers.

The SYNTECH project is about bridging this gap. It addresses challenges that relate to the change from writing code to writing specifications, and the development of tools to support a specification-centric rather than a code-centric development process.

Work performed

So far, we have performed work along four objectives. The design and implementation of a new specification language for reactive systems, where we incorporated ideas from programming language design. The design and implementation of analysis methods, beyond the synthesis algorithm itself, including, for example, means to deal with unrealizable specifications. The implementation of an end-to-end synthesis-based development environment and its application to autonomous robots implemented as Lego robots in our lab. And finally, early experience and evaluation with the new language and tools, with 3rd year computer science undergraduate students, to learn about the challenges of the project moving forward and create a collection of specifications that can be used in the future as a benchmark.

Final results

Our work advanced the state of the art in reactive synthesis on several fronts. On the new language development front, we have defined the Spectra language, a first of its kind specification language for reactive systems synthesis. The language has novel features targeting ease of use by software engineers for the context of temporal declarative specifications for reactive synthesis. On the new methods front, in addition to a major effort in implementation of our own GR(1) synthesizer, we have made major progress in analysis tools that assist engineers in writing higher quality specifications. On the application domains and evaluation fronts, we have so far mostly invested in the autonomous robots domain, and implemented an environment for application on Lego robots.