%0 Journal Article
%T qrdchecker:一个qrdc模型检验工具
%A 裴玉？
%A 徐启文？
%A 李宣东？
%A 郑国梁？
%J 软件学报
%P 355-364
%D 2005
%X 反应式系统通常是不终止的,其行为定义为系统状态的无限序列的集合.形式化验证时,检验需求一般使用时序逻辑给出.当使用诸如ltl(lineartemporallogic)这样的逻辑时,由于这类逻辑的模型同样是无限序列,系统与需求之间的满足性关系可以简单定义为集合的包含关系.但是,当使用时段时序逻辑(intervaltemporallogic)作为说明逻辑时,由于逻辑模型的有限性,使得上面的满足关系不再适用.称这类有限序列集合表达的性质为有限性性质.对于不同的有限性性质,它们对应的满足性关系是有区别的.针对两类有限性定义了它们各自的满足性关系,并将这两种关系统一为一个更一般的满足性关系.在此基础上,提出模型检验这两类性质的算法,并将其实现为一个针对时段时序逻辑qrdc(quantifiedrdc(restricteddurationcalculus))的检验工具qrdchecker.qrdchecker可以检验qrdc公式在连续时间模型和离散时间模型下的有效性.在离散时间条件下,它还可以将qrdc公式转换成模型检验系统spin能够接受的自动机的形式,从而可以检查反应式系统是否满足用qrdc公式表达的性质.
%K 模型检验
%K 有限性性质
%K 反应式系统
%K 时段时序逻辑
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=20050304&flag=1