| 基于稠密时间的实时系统模型检测的一个应用 |
| |
| 引用本文： | 陆公正,戎玫,张广泉. 基于稠密时间的实时系统模型检测的一个应用[J]. 苏州大学学报(工科版), 2005, 25(2): 1-6 |
| |
| 作者姓名： | 陆公正 戎玫 张广泉 |
| |
| 作者单位： | 1. 苏州大学计算机科学与技术学院,江苏,苏州,215006
2. 暨南大学深圳旅游学院,广东,深圳,518053 |
| |
| 基金项目： | 国家高科技研究发展计划(863)课题(编号2001AA113200)，中国科学院计算机科学国家重点实验室开放课题(编号SYSKF0303)，重庆市科学技术研究项目(编号040803)。 |
| |
| 摘 要： | 模型检测是一种用于并发系统性质验证的算法技术。实际生活中广泛应用的是带有时间约束的并发系统即实时系统，现在模型检测技术越来越被广泛地应用到这类系统的性质验证当中。这类系统通常用时间自动机来表示，而它们的性质则用时序逻辑公式表示。本文简要介绍了时间自动机和时序逻辑TCTL，并着重说明了如何进行基于稠密时间的实时系统的模型检测，最后给出了一个应用实例。
|
| 关 键 词： | 模型检测 实时系统 时间自动机 域自动机 时序逻辑 |
| 文章编号： | 1673-047X(2005)02-0001-06 |
| 修稿时间： | 2004-12-07 |
An Application of Dense Time-based Model-checking of Real-time Systems |
| |
| LU Gong-zheng,RONG Mei,ZHANG Guang-quan. An Application of Dense Time-based Model-checking of Real-time Systems[J]. Journal of Suzhou University(Engineering Science Edition), 2005, 25(2): 1-6 |
| |
| Authors: | LU Gong-zheng RONG Mei ZHANG Guang-quan |
| |
| Affiliation: | LU Gong-zheng~1,RONG Mei~2,ZHANG Guang-quan~1 |
| |
| Abstract: | Model-checking is a technology for the verification of the properties of the concurrent systems.However,concurrent systems with time restriction namely real-time systems are used widely in reallife,and the model-checking techniques are more and more applied to the verification of the properties of the real-time systems.The systems are usually described by the timed automata and the properties are specified by the temporal logic. This paper introduced the timed automata and TCTL in brief,and described how to model check the real-time systems based dense time,then we give an example in the end. |
| |
| Keywords: | model checking real-time systems timed automata region automata temporal logic |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
