论文标题
将TOCK-CSP自动翻译为定时自动机
Automatic Translation of tock-CSP into Timed Automata
论文作者
论文摘要
在支持各种验证工具的支持下，该过程代数TOCK-CSP提供了用于建模离散时间行为的文本符号。同样，实时验证工具箱Uppaal支持定时自动机（TA）的自动验证。 TA和TOCK-CSP在建模和验证方法上都不同。例如，使用TOCK-CSP的构建体很难指定LIVISESSIENS，但在Uppaal中很容易验证。在这项工作中，我们将TOCK-CSP转换为TA以利用Uppaal。我们已经开发了一种翻译技术和工具。我们的工作使用规则将TOCK-CSP转化为小型TA网络，该网络解决了捕获TOCK-CSP的组成性的复杂性。为了进行验证，我们使用基于有限近似值的实验方法进行跟踪集。我们计划使用数学证明来确定涵盖无限痕迹的规则的正确性。
The process algebra tock-CSP provides textual notations for modelling discrete-time behaviours, with the support of various tools for verification. Similarly, automatic verification of Timed Automata (TA) is supported by the real-time verification toolbox UPPAAL. TA and tock-CSP differ in both modelling and verification approaches. For instance, liveness requirements are difficult to specify with the constructs of tock-CSP, but they are easy to verify in UPPAAL. In this work, we translate tock-CSP into TA to take advantage of UPPAAL. We have developed a translation technique and tool; our work uses rules for translating tock-CSP into a network of small TA, which address the complexity of capturing the compositionality of tock-CSP . For validation, we use an experimental approach based on finite approximations to trace sets. We plan to use mathematical proof to establish the correctness of the rules that will cover an infinite set of traces.
