通过将 tock-CSP 自动翻译为时序自动机进行时态推理
形式语言与自动机理论
2021-04-29 v1 软件工程
摘要
在这项工作中,我们考虑将 tock-CSP 翻译为用于 UPPAAL 的时序自动机(Timed Automata),以便于在 UPPAAL 中推理 tock-CSP 模型的时态规约。进程代数 tock-CSP 提供了用于建模离散时间行为的文本记号,并配有自动验证工具的支持。类似地,具有图形记号的时序自动机(TA)的自动验证由 UPPAAL 实时验证工具箱 \uppaal 支持。这两种建模方法,TA 和 tock-CSP,在建模和验证方法、时态逻辑和精化以及它们提供的自动验证设施方面均有所不同。例如,活性需求难以用 tock-CSP 的构造来指定,但在 UPPAAL 中易于指定和验证。为了利用时态逻辑的优势,我们将 tock-CSP 翻译为用于 \uppaal 的 TA;我们已开发了一种翻译技术及其支持工具。我们提供了将 tock-CSP 翻译为小型 TA 网络以捕获 TA 中不具备的 tock-CSP 组合结构的规则。为验证,我们首先基于有限逼近迹集的实验方法。然后,我们探索数学证明以建立覆盖无限迹的规则的正确性。
引用
@article{arxiv.2104.13434,
title = {Temporal Reasoning Through Automatic Translation of tock-CSP into Timed Automata},
author = {Abdulrazaq Abba and Ana Cavalcanti and Jeremy Jacob},
journal= {arXiv preprint arXiv:2104.13434},
year = {2021}
}
备注
arXiv admin note: substantial text overlap with arXiv:2008.06935