TY - JOUR
T1 - Spectra: a specification language for reactive systems
AU - Maoz, Shahar
AU - Ringert, Jan Oliver
N1 - Funding Information:
We thank the 67 undergraduate students who participated in our four project classes. We thank Elizabeth Firman, Aviv Kuvent, Or Pistiner, Rafi Shalom, Ilia Shevrin, Keren Solodkin, and Yoni Wolbe for their contribution to the implementation of Spectra Tools. This project has received funding from the European Research Council (ERC) under the European Union?s Horizon 2020 research and innovation program (grant agreement No 638049, SYNTECH).
Funding Information:
TLA [] (Temporal Logic of Actions) is a versatile specification language for software systems. TLA includes language constructs for the structural definition of closed and open (reactive) systems. Behavior in TLA can be specified using temporal operators. Analyses of TLA specifications are supported by the TLC model-checker []. The TLA language is too expressive for model-checking to be fully automated and only subsets of the language are supported. TLA has been successfully applied in industrial settings []. We believe that in the future, Spectra could benefit from composition mechanisms for specifications, similar to the ones provided by TLA.
Publisher Copyright:
© 2021, The Author(s).
Copyright:
Copyright 2021 Elsevier B.V., All rights reserved.
PY - 2021/10
Y1 - 2021/10
N2 - 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.
AB - 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.
KW - Reactive synthesis
KW - GR(1)
KW - Specification language
UR - http://www.scopus.com/inward/record.url?scp=85102825828&partnerID=8YFLogxK
U2 - 10.1007/s10270-021-00868-z
DO - 10.1007/s10270-021-00868-z
M3 - Article
SN - 1619-1366
VL - 20
SP - 1553
EP - 1586
JO - Software and Systems Modeling
JF - Software and Systems Modeling
IS - 5
ER -