离散持续时间计算中时序图要求的形式化
Formalizing Timing Diagram Requirements in Discrete Duration Calulus
摘要：
已经提出了几种时序逻辑来正式化硬件和嵌入式控制器的时序图要求。这些包括LTL、离散时间MTL和最近的行业标准PSL。然而，时序图的简洁性和视觉结构并没有被他们的公式充分捕捉。区间时序逻辑QDDC是一种高度简洁和可视化的表示法，用于指定行为模式。在本文中，我们提出了一个实际有用的符号称为SeCeCntnl，增强了否定自由片段的QDDC与功能的名词和有限的活性。我们表明，时序图可以自然（成分）和successly正式在SeCeCntnl相比，PSL和MTL。我们给出了一个线性时间翻译时序图SeCeCntnl。作为我们的第二个主要结果，我们提出了SeCeCntnl到QDDC的线性时间翻译。这使得QDDC工具，如DCVALID和DCSynth，可用于检查时序图要求的一致性，以及自动合成属性监视器和控制器。我们给出了一个矿泵控制器和总线仲裁器的例子来说明我们的工具。给出了理论分析，我们表明，所提出的SeCeCntnl，可满足性和模型检验具有初等复杂性相比，非初等复杂性的全逻辑QDDC。
英文摘要：
Several temporal logics have been proposed to formalise timing diagram requirements over hardware and embedded controllers. These include LTL, discrete time MTL and the recent industry standard PSL. However, succintness and visual structure of a timing diagram are not adequately captured by their formulae. Interval temporal logic QDDC is a highly succint and visual notation for specifying patterns of behaviours. In this paper, we propose a practically useful notation called SeCeCntnl which enhances negation free fragment of QDDC with features of nominals and limited liveness. We show that timing diagrams can be naturally (compositionally) and succintly formalized in SeCeCntnl as compared with PSL and MTL. We give a linear time translation from timing diagrams to SeCeCntnl. As our second main result, we propose a linear time translation of SeCeCntnl into QDDC. This allows QDDC tools such as DCVALID and DCSynth to be used for checking consistency of timing diagram requirements as well as for automatic synthesis of property monitors and controllers. We give examples of a minepump controller and a bus arbiter to illustrate our tools. Giving a theoretical analysis, we show that for the proposed SeCeCntnl, the satisfiability and model checking have elementary complexity as compared to the non-elementary complexity for the full logic QDDC.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
