Spectra: A Specification Language for Reactive SystemsJ1ST
We introduce Spectra, a new specification language for reactive systems, specifically tailored for the context of reactive synthesis. The meaning of Spectra is defined by a translation to a kernel language. 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. We present the language in detail and give an overview of its tool set. Together with the language and its tool set, we present four collections of many, non-trivial, large specifications, written by undergraduate computer science students for the development of autonomous Lego robots and additional example reactive systems. The collected specifications can serve as benchmarks for future studies on reactive synthesis. We present the specifications, with observations and lessons learned about the potential use of reactive synthesis by software engineers.
Wed 13 OctDisplayed time zone: Osaka, Sapporo, Tokyo change
18:00 - 19:00 | Modeling Languages ITechnical Papers at Room 1 Chair(s): Benoit Combemale University of Rennes; Inria; IRISA | ||
18:00 20mTalk | Pragmatic Reuse in DSML DevelopmentJ1ST Technical Papers | ||
18:20 20mTalk | Spectra: A Specification Language for Reactive SystemsJ1ST Technical Papers Link to publication DOI | ||
18:40 20mFull-paper | OSTRICH - A Safe Template Language for Low-code DevelopmentP&I Technical Papers Hugo Lourenço OutSystems SA, Carla Ferreira NOVA School of Science and Technology, João Costa Seco NOVA LINCS -- Universidade Nova de Lisboa |