基于模拟关系的精化检测方法

发布时间：2017-10-06 22:25

  本文关键词：基于模拟关系的精化检测方法

  更多相关文章： 精化检测 模拟 failures divergence 时间自动机

【摘要】：精化检测是一种重要的形式化验证方法,将系统实现和性质规约用相同的形式化语言进行建模,如能证明两者间存在某种精化关系,且该关系能够维持性质,可得出系统实现满足性质规约.为验证不同类型的系统性质,traces,stable failures和failures-divergence精化检测方法已被提出.精化检测算法依赖于子集构造,因而其面临状态空间爆炸问题.近年来,已有学者针对NFA语言包含问题提出了基于模拟关系的状态空间消减方法,极大地提高了算法的性能,且该方法能够直接用于traces精化检测.在此基础上,提出了基于模拟关系的stable failures和failuresdivergence精化检测方法.此外,还将精化检测扩展到了时间系统的验证中,提出了基于模拟关系的时间自动机traces精化检测方法.实验结果表明,基于模拟关系的算法效率有很大提高.
【作者单位】： 浙江工业大学计算机科学与技术学院;School
【关键词】： 精化检测 模拟 failures divergence 时间自动机
【基金】：国家自然科学基金(61103044,U1509214) 浙江省自然科学基金(LQ15E050006,LY16F020035)~~
【分类号】：TP301.1
【正文快照】： 精化(refinement)方法已在理论研究和工程实践中被广泛应用,一般过程是通过对抽象模型的逐步求精得到具体的系统实现,系统实现和抽象模型间即存在精化关系.两者均能满足某种性质,使得系统实现在代替抽象模型时能够保持一致性和正确性.在形式化验证方面,利用精化关系的验证(以

【相似文献】

中国期刊全文数据库 前6条

1 祁方民;;Petri网结点精化及其应用[J];计算机与现代化;2014年07期

2 王云峰 ,庞军 ,查鸣 ,杨朝晖 ,郑国梁;精化演算支撑工具的分析[J];计算机应用与软件;2002年02期

3 刘瑜,张世琨,邬伦,叶燕林;地理信息系统中的设计模式——以过滤和精化为例[J];北京大学学报(自然科学版);2001年06期

4 熊建;陈晓克;;基于Wiki技术可持续精化精品课教学平台[J];福建电脑;2010年12期

5 杨朝晖;王云峰;郑国梁;;精化演算支撑工具PRT的研究[J];计算机科学;2000年03期

6 ;[J];;年期

中国重要会议论文全文数据库 前5条

1 周鑫;;面对新形势、树立新观念、迎接新挑战——谈企业职工面对“精化分立、分业经营”新形势的感想[A];陕西省体制改革研究会2006-2007优秀论文集[C];2007年

2 高阳;王敏中;;拉伸矩形梁的精化理论[A];北京力学会第11届学术年会论文摘要集[C];2005年

3 高阳;王敏中;;横观各项同性压电矩形直梁的精化理论[A];中国力学学会学术大会'2005论文摘要集（下）[C];2005年

4 赵红丽;范景辉;郭小方;刘广;陈建平;;CR辅助的基线参数精化方法研究[A];第十七届中国遥感大会摘要集[C];2010年

5 江东;王庆宾;王凯;;重力场精化的空间插值方法研究[A];中国测绘学会2010年学术年会论文集[C];2010年

中国重要报纸全文数据库 前10条

1 罗平华;彩虹精化气雾漆龙头今日挂牌[N];证券时报;2008年

2 证券时报记者 罗平华;彩虹精化出口收入逆势增长三成[N];证券时报;2009年

3 证券时报记者 向南;彩虹精化 涉足室内环保业务[N];证券时报;2010年

4 记者 翟敏;彩虹精化上半年业绩平平 管理层就“巨额订单”事件致歉[N];上海证券报;2011年

5 记者 王健杰;彩虹精化营收内降外增[N];北京商报;2009年

6 中国空空导弹研究院 综合管理处;精化军品能力 优化民品结构[N];中国航空报;2004年

7 本报通讯员 周善良 记者 李雨农;精化分立 一所多制[N];中国航空报;2002年

8 武连寅邋蔡军;淮化精化再次入选国家高新企业[N];中国化工报;2007年

9 记者 孙燕飚　刘琼;万润精化再上会 日德企业“锁喉”难改观[N];第一财经日报;2011年

10 记者 况玉清;彩虹精化虚假陈述案下月开庭[N];北京商报;2012年

中国博士学位论文全文数据库 前4条

1 陈桂芝;解大规模非对称矩阵特征问题的一些精化算法[D];大连理工大学;2000年

2 梁红瑾;并发程序精化验证及其应用[D];中国科学技术大学;2014年

3 牛大田;计算大规模矩阵部分奇异值分解的精化Lanczos型算法[D];大连理工大学;2003年

4 梁坤;高灵敏度GPS接收技术中几个关键问题的研究[D];中国科学院研究生院（国家天文台）;2008年

中国硕士学位论文全文数据库 前5条

1 钱洁;轨旁系统的形式化建模精化与验证[D];华东师范大学;2015年

2 刘婷婷;双层梁的精化理论[D];辽宁科技大学;2015年

3 刘稳;隐式重启和精化的全局Lanczos方法与块Lanczos方法[D];南京航空航天大学;2014年

4 付亚军;面向多主体的基于政策的运行机制研究[D];湖南大学;2009年

5 吴钢;解大规模非对称矩阵特征问题Lanczos方法的两种精化版本[D];大连理工大学;2001年

，

本文编号：985370