QRDChecker:一个QRDC模型检验工具

作者：裴玉; 徐启文; 李宣东; 郑国梁

来源：软件学报, 2005, (03): 355-364.

• 模型检验
• 有限性性质
• 反应式系统
• 时段时序逻辑 model checking
• finitary property
• reactive system
• interval temporal logic

反应式系统通常是不终止的,其行为定义为系统状态的无限序列的集合.形式化验证时,检验需求一般使用时序逻辑给出.当使用诸如 LTL(linear temporal logic)这样的逻辑时,由于这类逻辑的模型同样是无限序列,系统与需求之间的满足性关系可以简单定义为集合的包含关系.但是,当使用时段时序逻辑(interval temporallogic)作为说明逻辑时,由于逻辑模型的有限性,使得上面的满足关系不再适用.称这类有限序列集合表达的性质为有限性性质.对于不同的有限性性质,它们对应的满足性关系是有区别的.针对两类有限性定义了它们各自的满足性关系,并将这两种关系统一为一个更一般的满足性关系.在此...

• 单位
  南京大学; 澳门大学