Reactive Synthesis with Spectra: A Tutorial

Abstract

Spectra is a formal specification language specifically tailored for use in the context of reactive synthesis, an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. Spectra comes with the Spectra Tools, a set of analyses, including a synthesizer to obtain a correct-by-construction implementation, several means for executing the resulting controller, and additional analyses aimed at helping engineers write higher-quality specifications.

This hands-on tutorial will introduce participants to the language and the tool set, using examples and exercises, covering an end-to-end process from specification writing to synthesis to execution. The tutorial may be of interest to software engineers and researchers who are interested in the potential applications of formal methods to software engineering.

ICSE'21 Tutorial Spectra Installation

To appear in May 2021! Until then, see instructions here.

ICSE'21 Tutorial Modules

  • (L1) Write your first specification: using basic language constructs: variable declarations, type definitions, basic assumptions and guarantees
  • (E2) Execute your first reactive system: using the synthesized controller in your Java application
  • (A2) Unrealizability: unrealizablity core, counter-strategies, and repair
  • (L3) Advanced language constructs: using patterns
  • (E4) Advanced execution features: efficiency and reliability
  • ...

To be available in May 2021!