UM  > 科技學院  > 電腦及資訊科學系
QRDChecker:一个 QRDC 模型检验工具
裴玉1; 徐启文2; 李宣东1; 郑国梁1
2005
Source Publication软件学报
ISSN1000-9825
Volume16Issue:03Pages:355-364
Abstract

反应式系统通常是不终止的,其行为定义为系统状态的无限序列的集合.形式化验证时,检验需求一般 使用时序逻辑给出.当使用诸如 LTL(linear temporal logic)这样的逻辑时,由于这类逻辑的模型同样是无限序列, 系统与需求之间的满足性关系可以简单定义为集合的包含关系.但是,当使用时段时序逻辑(interval temporallogic)作为说明逻辑时,由于逻辑模型的有限性,使得上面的满足关系不再适用.称这类有限序列集合表达的性质 为有限性性质.对于不同的有限性性质,它们对应的满足性关系是有区别的.针对两类有限性定义了它们各自的 满足性关系,并将这两种关系统一为一个更一般的满足性关系.在此基础上,提出模型检验这两类性质的算法,并 将其实现为一个针对时段时序逻辑 QRDC(quantified RDC (restricted duration calculus)) 的 检验工具 QRDChecker.QRDChecker 可以检验 QRDC 公式在连续时间模型和离散时间模型下的有效性.在离散时间条件 下,它还可以将 QRDC 公式转换成模型检验系统 Spin 能够接受的自动机的形式,从而可以检查反应式系统是否 满足用 QRDC 公式表达的性质.

Keyword模型检验 有限性性质 反应式系统 时段时序逻辑
DOI10.1360/jos160355
Language中文
Fulltext Access
Citation statistics
Document TypeJournal article
CollectionDEPARTMENT OF COMPUTER AND INFORMATION SCIENCE
Corresponding Author裴玉
Affiliation1.南京大学 计算机科学与技术系,江苏 南京 210093
2.澳门大学 科技学院,澳门
Recommended Citation
GB/T 7714
裴玉,徐启文,李宣东,等. QRDChecker:一个 QRDC 模型检验工具[J]. 软件学报,2005,16(03):355-364.
APA 裴玉,徐启文,李宣东,&郑国梁.(2005).QRDChecker:一个 QRDC 模型检验工具.软件学报,16(03),355-364.
MLA 裴玉,et al."QRDChecker:一个 QRDC 模型检验工具".软件学报 16.03(2005):355-364.
Related Services
Recommend this item
Bookmark
Usage statistics
Export to Endnote
Google Scholar
Similar articles in Google Scholar
[裴玉]'s Articles
[徐启文]'s Articles
[李宣东]'s Articles
Baidu academic
Similar articles in Baidu academic
[裴玉]'s Articles
[徐启文]'s Articles
[李宣东]'s Articles
Bing Scholar
Similar articles in Bing Scholar
[裴玉]'s Articles
[徐启文]'s Articles
[李宣东]'s Articles
Terms of Use
No data!
Social Bookmark/Share
All comments (0)
No comment.
 

Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.