在离散时段演算中形式化时序图需求
计算机科学中的逻辑
2017-05-15 v1
摘要
若干时序逻辑已被提出，用于形式化硬件与嵌入式控制器上的时序图需求。这些包括LTL、离散时间MTL以及近期的工业标准PSL。然而，时序图的简洁性与视觉结构未被它们的公式充分捕获。区间时序逻辑QDDC是一种用于指定行为模式的高度简洁且视觉化的符号。本文中，我们提出一种实用符号SeCeCntnl，它增强了QDDC的无否定片段，具有名义（nominals）与有限活性（limited liveness）特征。我们展示与时序图相比，时序图可以在SeCeCntnl中被自然（组合式）且简洁地形式化，相较于PSL和MTL。我们给出了从时序图到SeCeCntnl的线性时间翻译。作为第二个主要结果，我们提出了从SeCeCntnl到QDDC的线性时间翻译。这使得QDDC工具如DCVALID和DCSynth可用于检查时序图需求的一致性，以及用于属性监视器与控制器的自动合成。我们给出矿泵控制器与总线仲裁器的示例以说明我们的工具。通过理论分析，我们展示对于提出的SeCeCntnl，可满足性与模型检测具有初等复杂度，而完整逻辑QDDC具有非初等复杂度。
引用
@article{arxiv.1705.04510,
title = {Formalizing Timing Diagram Requirements in Discrete Duration Calulus},
author = {Raj Mohan Matteplackel and Paritosh K. Pandya and Amol Wakankar},
journal= {arXiv preprint arXiv:1705.04510},
year = {2017}
}