论文部分内容阅读
模型检测是一种用于并发系统性质验证的算法技术.实际生活中广泛应用的是带有时间约束的并发系统即实时系统,现在模型检测技术越来越被广泛地应用到这类系统的性质验证当中.这类系统通常用时间自动机来表示,而它们的性质则用时序逻辑公式表示.本文简要介绍了时间自动机和时序逻辑TCTL,并着重说明了如何进行基于稠密时间的实时系统的模型检测,最后给出了一个应用实例.