tock-CSP 到时间自动机的自动翻译
计算机科学中的逻辑
2021-04-30 v2 形式语言与自动机理论
摘要
进程代数 tock-CSP 提供了用于建模离散时间行为的文本记号，并支持多种验证工具。类似地，实时验证工具箱 UPPAAL 支持时间自动机（TA）的自动验证。TA 与 tock-CSP 在建模与验证方法上均有所不同。例如，活性需求难以用 tock-CSP 的构造来规约，但在 UPPAAL 中易于验证。在本工作中，我们将 tock-CSP 翻译为 TA 以利用 UPPAAL 的优势。我们开发了一种翻译技术与工具；我们的工作使用将 tock-CSP 翻译为小型 TA 网络的一组规则，以应对刻画 tock-CSP 组合性所带来的复杂性。为进行验证，我们采用了一种基于迹集有限逼近的实验方法。我们计划使用数学证明来确立这些规则的正确性，从而覆盖无限的迹集。
引用
@article{arxiv.2008.06935,
title = {Automatic Translation of tock-CSP into Timed Automata},
author = {Abdulrazaq Abba and Ana Cavalcanti and Jeremy Jacob},
journal= {arXiv preprint arXiv:2008.06935},
year = {2021}
}
备注
An updated version of this paper is available in this link arXiv:2104.13434