Reactive Synthesis with Spectra: A Tutorial
Reactive Synthesis with Spectra: A Tutorial
复制标题
光谱反应合成：教程
DOI：
--
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Jan Oliver Ringert
中科院分区：
文献类型：
--
作者：
S. Maoz;Jan Oliver Ringert
SPECTRUM是一种专门用于反应合成的形式描述语言，反应合成是从其时间逻辑规范中获得按构造正确的反应系统的自动化过程。Spectra随附了Spectra工具、一组分析，包括一个合成器以获得按构造进行的正确实现、几种用于执行最终控制器的方法，以及旨在帮助工程师编写更高质量规范的附加分析。本实践教程将使用示例和练习向参与者介绍该语言和工具集，涵盖从编写规范到合成再到执行的端到端过程。对软件工程中形式方法的潜在应用感兴趣的软件工程师和研究人员可能会对本教程感兴趣。
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.