定时并发约束程序的自动验证
计算机科学中的逻辑
2007-05-23 v1
摘要
定时并发约束语言（tccp）是并发约束编程（cc）范式在时间维度上的扩展，它允许我们指定时序至关重要的并发系统，例如反应式系统。可以用tccp指定具有无限状态数的系统。模型检测是一种能够自动验证具有大量状态的有限状态系统的技术。近年来，多项研究探讨了如何将模型检测技术扩展到具有无限状态数的系统。本文提出了一种利用tccp计算模型的方法。基于约束的计算使我们能够定义一种将模型检测算法应用于（一类）无限状态系统的方法论。我们将用于LTL的经典模型检测算法扩展到一种专门为tccp验证而定义的逻辑，以及本文中为建模程序行为而定义的tccp结构。我们定义了时间的一个限制以获得有限模型，并开发了一些说明性示例。据我们所知，这是首个为tccp定义模型检测方法论的方法。
引用
@article{arxiv.cs/0505026,
title = {Automatic Verification of Timed Concurrent Constraint Programs},
author = {Moreno Falaschi and Alicia Villanueva},
journal= {arXiv preprint arXiv:cs/0505026},
year = {2007}
}