FocusST的时空特征

摘要：

在这份技术报告中，我们总结了时空特征，并提出了FocusST规范框架的核心运算符。我们提出了这些运营商的总体思路，使用蒸汽锅炉系统的例子来说明如何规范框架可以应用。FocusST的灵感来自于Focus，一个用于交互式系统的正式规范和开发的框架。与Focus相比，FocusST致力于指定和分析系统的空间（S）和时间（T）方面，这也反映在框架的名称中：扩展ST突出了规范的时空性质。

英文摘要：

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.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。