主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2019年第10期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
裴玉,徐启文,李宣东,郑国梁.QRDChecker:一个QRDC模型检验工具.软件学报,2005,16(3):355-364
QRDChecker:一个QRDC模型检验工具
QRDChecker: A Model Checking Tool for QRDC
投稿时间:2003-06-20  修订日期:2004-03-29
DOI:
中文关键词:  模型检验  有限性性质  反应式系统  时段时序逻辑
英文关键词:model checking  finitary property  reactive system  interval temporal logic
基金项目: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)
作者单位
裴玉 南京大学,计算机科学与技术系,江苏,南京,210093 
徐启文 澳门大学,科技学院,澳门 
李宣东 南京大学,计算机科学与技术系,江苏,南京,210093 
郑国梁 南京大学,计算机科学与技术系,江苏,南京,210093 
摘要点击次数: 2998
全文下载次数: 3372
中文摘要:
      反应式系统通常是不终止的,其行为定义为系统状态的无限序列的集合.形式化验证时,检验需求一般使用时序逻辑给出.当使用诸如LTL(linear temporal logic)这样的逻辑时,由于这类逻辑的模型同样是无限序列,系统与需求之间的满足性关系可以简单定义为集合的包含关系.但是,当使用时段时序逻辑(interval temporal logic)作为说明逻辑时,由于逻辑模型的有限性,使得上面的满足关系不再适用.称这类有限序列集合表达的性质为有限性性质.对于不同的有限性性质,它们对应的满足性关系是有区别的.针对两类有限性定义了它们各自的满足性关系,并将这两种关系统一为一个更一般的满足性关系.在此基础上,提出模型检验这两类性质的算法,并将其实现为一个针对时段时序逻辑QRDC(quantified RDC (restricted duration calculus))的检验工具QRDChecker.QRDChecker可以检验QRDC公式在连续时间模型和离散时间模型下的有效性.在离散时间条件下,它还可以将QRDC公式转换成模型检验系统Spin能够接受的自动机的形式,从而可以检查反应式系统是否满足用QRDC公式表达的性质.
英文摘要:
      A reactive system does not terminate and its behaviors are typically defined as a set of infinite sequences of states. In formal verification, a requirement is usually expressed in a logic, and when the models of the logic are also defined as infinite sequences, such as the case for LTL (linear temporal logic), the satisfaction relation is simply defined by the set containment. However, this satisfaction relation does not work for interval temporal logics, where the models are finite sequences. In fact, for different interval based properties, different satisfaction relations are sensible. Two classes of finitary properties are identified, and then two satisfaction relations are defined for them, which are unified by a general relation. A model checking algorithm is proposed and implemented in a verification tool for QRDC (quantified RDC (restricted duration calculus)), which is an interval temporal logic. The tool QRDChecker can check the validity of QRDC formulae under both continuous and discrete interpretations. Moreover, for discrete QRDC, it can also translate the formulae into an automaton in the form accepted by the Spin model checking system, which can be subsequently used to verify a reactive system against properties expressed in the logic.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会 京ICP备05046678号-4
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利