一种模型检测精确加速的判断方法

摘要：

在实时系统中具有不同的时间度量,在用时间自动机进行建模及验证时会引起片段问题,通常的解决办法是向时间自动机添加一个附加环,但是在片段数量较少或片段不满足一定条件时,添加附加环的加速效果并不明显,甚至会降低验证速度.对此,本文提出一种模型检测精确加速的判断方法,通过分析加速过程中的主要参数,推导出了精确加速是否有效的判断条件.实验结果表明,利用这个判定条件可以准确地判断模型是否需要加速.

关键词： 实时系统 模型检测 时间自动机 附加环加速技术 判断标准

作者: 勾利杰 李真 王从银 庄雷

作者单位: 郑州大学 信息工程学院,郑州 450001 郑州大学 信息工程学院,郑州 450001;吉首大学 数学与计算机科学学院,湖南 吉首 416000

会议类型: 国内会议

会议名称: 2014年河南省计算机学会学术年会暨河南省计算机大会

会议地点: 河南安阳

会议语种:中文

页码: 37-41

在线出版日期: 2014-08-18（万方平台首次上网日期，不代表论文的发表时间）