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 (updated in 10/2022)

  • Download and install Eclipse for Java and DSL Developers (Windows 64Bit or Linux or Mac)
    • Note: When you run the Eclipse installer, remember to choose "Eclipse IDE for Java and DSL Developers"
  • Use "Eclipse/Help/Install new software..." to install Spectra Tools from our update site: http://smlab.cs.tau.ac.il/syntech/spectra/tools/update/
    • Note: Mac users, starting July 2023, Spectra IDE should be compatible with M1. If you use M2, use "Eclipse/Window/Preferences/Spectra" to change the BDD engine to "JTLV package".
  • Download the tutorial zip and import the projects into your workspace

Installation instructions video is available here.

ICSE'21 Tutorial Modules

Three module types: [L] - Language; [A] - Analyses; [E] - Execution

  • [L1] Write your first specification: variable declarations, assumptions and guarantees
  • [L2] Advanced language constructs: type definitions, defines, predicates, arrays
  • [L3] Advanced language constructs: patterns and past operators
  • [A1] Synthesize your first controller
  • [A2] Unrealizability: checking realizability, unrealizability core, counter-strategies
  • [A3] Non-well-separation
  • [E1] Basic step-by-step simulation
  • [E2] Execute your reactive system: using the synthesized controller in your Java application
  • [E3] Advanced step-by-step simulation: using breakpoints and reachability
A playlist with all the tutorial modules is available on YouTube here.