Spatio-temporal features of FocusST
This work provides a domain-specific tool for formal specification in interactive systems, but it appears incremental as it extends an existing framework without new performance metrics.
The authors introduced FocusST, a specification framework for modeling spatio-temporal aspects of systems, building on the existing Focus framework to address spatial and timing features, as demonstrated through a Steam Boiler System example.
In this technical report we summarise the spatio-temporal features and present the core operators of FocusST specification framework. We present the general idea of these operators, using a Steam Boiler System example to illustrate how the specification framework can be applied. FocusST was inspired by Focus, a framework for formal specification and development of interactive systems. In contrast to Focus, FocusST is devoted to specify and to analyse spatial (S) and timing (T) aspects of the systems, which is also reflected in the name of the framework: the extension ST highlights the spatio-temporal nature of the specifications.