基于稠密时间的实时系统模型检测的一个应用

被引：12

作者：

陆公正

戎玫

张广泉

机构：

[1] 苏州大学计算机科学与技术学院

[2] 暨南大学深圳旅游学院

[3] 苏州大学计算机科学与技术学院江苏苏州

[4] 广东深圳

[5] 江苏苏州

来源：

苏州大学学报(工科版) | 2005年 / 02期

关键词：

模型检测; 实时系统; 时间自动机; 域自动机; 时序逻辑;

D O I：

暂无

中图分类号：

TP273 [自动控制、自动控制系统];

学科分类号：

080802 [电力系统及其自动化];

摘要：

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

引用

页码：1 / 6

页数：6