Generalised Test Tables: A Practical Specification Language for Reactive Systems

2017 ◽  
pp. 129-144 ◽  
Author(s):  
Bernhard Beckert ◽  
Suhyun Cha ◽  
Mattias Ulbrich ◽  
Birgit Vogel-Heuser ◽  
Alexander Weigl
Keyword(s):  
Reactive Systems ◽  
Specification Language

scholarly journals Spectra: a specification language for reactive systems

2021 ◽  
Author(s):  
Shahar Maoz ◽  
Jan Oliver Ringert
Keyword(s):  
Reactive Systems ◽  
Specification Language ◽  
Lessons Learned ◽  
Science Students ◽  
Future Studies ◽  
Reactive Synthesis ◽  
Quality Specifications ◽  
Software Engineers ◽  
Tool Set ◽  
Potential Use

AbstractWe 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.

scholarly journals Generalized test tables: A powerful and intuitive specification language for reactive systems

2017 ◽  
Author(s):  
Alexander Weigl ◽  
Franziska Wiebe ◽  
Mattias Ulbrich ◽  
Sebastian Ulewicz ◽  
Suhyun Cha ◽  
...  
Keyword(s):  
Reactive Systems ◽  
Specification Language

scholarly journals A spatio-temporal specification language and its completeness & decidability

2020 ◽  
Vol 9 (1) ◽  
Author(s):  
Tengfei Li ◽  
Jing Liu ◽  
Haiying Sun ◽  
Xiang Chen ◽  
Lipeng Zhang ◽  
...  
Keyword(s):  
Intelligent Transportation System ◽  
Cyber Physical Systems ◽  
Specification Language ◽  
Finite Model ◽  
Critical Systems ◽  
Physical Systems ◽  
Spatial Objects ◽  
Temporal Properties ◽  
Spatio Temporal ◽  
Temporal Specification

AbstractIn the past few years, significant progress has been made on spatio-temporal cyber-physical systems in achieving spatio-temporal properties on several long-standing tasks. With the broader specification of spatio-temporal properties on various applications, the concerns over their spatio-temporal logics have been raised in public, especially after the widely reported safety-critical systems involving self-driving cars, intelligent transportation system, image processing. In this paper, we present a spatio-temporal specification language, STSL PC, by combining Signal Temporal Logic (STL) with a spatial logic S4 u, to characterize spatio-temporal dynamic behaviors of cyber-physical systems. This language is highly expressive: it allows the description of quantitative signals, by expressing spatio-temporal traces over real valued signals in dense time, and Boolean signals, by constraining values of spatial objects across threshold predicates. STSL PC combines the power of temporal modalities and spatial operators, and enjoys important properties such as finite model property. We provide a Hilbert-style axiomatization for the proposed STSL PC and prove the soundness and completeness by the spatio-temporal extension of maximal consistent set and canonical model. Further, we demonstrate the decidability of STSL PC and analyze the complexity of STSL PC. Besides, we generalize STSL to the evolution of spatial objects over time, called STSL OC, and provide the proof of its axiomatization system and decidability.

Sign in / Sign up

Export Citation Format

Share Document