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
- 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"
- Download the tutorial zip and import the projects into your workspace
- Use "Eclipse/Help/Install new software..." to install Spectra Tools from our update site:
Note: Mac users should use "Eclipse/Window/Preferences/Spectra" to change the BDD engine to "JTLV package"
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