| QRDChecker:一个QRDC模型检验工具 |
| |
| 作者姓名： | 裴玉 徐启文 李宣东 郑国梁 |
| |
| 作者单位： | 1. 南京大学,计算机科学与技术系,江苏,南京,210093
2. 澳门大学,科技学院,澳门 |
| |
| 基金项目： | Supported by the National Natural Science Foundation of China under Grant No.60233020 (国家自然科学基金); the National Grand Fundamental Research 973 Program of China under Grant No.2002CB312001 (国家重点基础研究发展规划(973) |
| |
| 摘 要： | 反应式系统通常是不终止的,其行为定义为系统状态的无限序列的集合.形式化验证时,检验需求一般使用时序逻辑给出.当使用诸如LTL(linear temporal logic)这样的逻辑时,由于这类逻辑的模型同样是无限序列,系统与需求之间的满足性关系可以简单定义为集合的包含关系.但是,当使用时段时序逻辑(interval temporal logic)作为说明逻辑时,由于逻辑模型的有限性,使得上面的满足关系不再适用.称这类有限序列集合表达的性质为有限性性质.对于不同的有限性性质,它们对应的满足性关系是有区别的.针对两类有限性定义了它们各自的满足性关系,并将这两种关系统一为一个更一般的满足性关系.在此基础上,提出模型检验这两类性质的算法,并将其实现为一个针对时段时序逻辑QRDC(quantified RDC (restricted duration calculus))的检验工具QRDChecker.QRDChecker可以检验QRDC公式在连续时间模型和离散时间模型下的有效性.在离散时间条件下,它还可以将QRDC公式转换成模型检验系统Spin能够接受的自动机的形式,从而可以检查反应式系统是否满足用QRDC公式表达的性质.
|
| 关 键 词： | 模型检验 有限性性质 反应式系统 时段时序逻辑 |
| 文章编号： | 1000-9825/2005/16(03)0355 |
| 收稿时间： | 2003-06-20 |
| 修稿时间： | 2003-06-20 |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载免费的PDF全文 |
|
