软件模型检测

作品数：15被引量：37H指数：4
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：张德运肖健宇化志章薛锦云张健沛更多>>
相关机构：北京轩宇信息技术有限公司大连理工大学清华大学西安交通大学更多>>
相关期刊：《电子学报》《西安交通大学学报》《桂林电子科技大学学报》《小型微型计算机系统》更多>>
相关基金：国家自然科学基金国家教育部博士点基金国家重点基础研究发展计划教育部“新世纪优秀人才支持计划”更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
基于模块化Abstract-Refine算法框架的软件模型检测方法被引量：1
《电子学报》2020年第5期997-1002,共6页王舜 杜晔 韩臻 
国家自然科学基金(No.61672092)。
Abstract-Refine(抽象—精炼)方法是软件模型检测领域中较为有效的设计思想,具有较高的通用性和效率优势,但目前并没有一个框架可以对其精确进行描述及实现有效的模块化使用和替换.本文提出了一种模块化的Abstract-Refine算法框架,分析...
关键词：软件模型检测 模块化方法 抽象—精炼(Abstract-Refine) 通用算法 抽象程序 
软件模型检测中状态爆炸问题的解决方法被引量：2
《现代计算机（中旬刊）》2017年第1期35-38,共4页屈媛媛 杜伊 
在软件模型检测中,系统所对应的状态数会随着系统大小成指数级增长,即状态空间爆炸问题。为了研究近年来该问题的解决方法,按照系统综述的方法,归类整理近年来对近年来解决状态空间爆炸的方法,并对每类方法的应用、限制以及该领域的未...
关键词：状态空间爆炸 模型检测 文献综述 
软件模型检测中的抽象模型研究综述被引量：12
《计算机研究与发展》2015年第7期1580-1603,共24页魏欧 石玉峰 徐丙凤 黄志球 陈哲 
国家自然科学基金项目(61170043;61100034;61272083);国家"九七三"重点基础研究发展计划基金项目(2014CB744904)
抽象是解决模型检测中状态爆炸问题的一个基本方法.对近年来软件模型检测研究中所提出的一系列抽象模型进行综述.首先以抽象解释为理论框架阐述了抽象软件模型检测的各组成部分.然后根据模型的结构和功能特征,将抽象模型分为3类:1)传统...
关键词：抽象模型 自上逼近 自下逼近 模型检测 多值模型 
传播最大和最新接受前驱的On-the-Fly并行空性检测被引量：1
《小型微型计算机系统》2015年第6期1203-1208,共6页赵璐 张健沛 杨静 
国家自然科学基金项目(61370083;61073043;61073041)资助;高等学校博士学科点专项科研基金项目(20112304110011;20122304110012)资助;哈尔滨市科技创新人才研究专项资金项目(2011RFXXG015)资助
针对一种结合最大接受前驱的on-the-fly并行空性检测方法,在接受环最大接受前驱处于环外的情境,无法通过传播接受前驱以on-the-fly方式识别接受环的问题,提出一种传播最大和最新接受前驱的on-the-fly并行空性检测方法.在首次遍历积自动...
关键词：软件模型检测 并行空性检测 Biichi自动机 on—the-fly方法 
收缩候选回溯集的有状态动态偏序归约方法被引量：1
《计算机工程》2015年第5期70-76,共7页赵璐 张健沛 杨静 
国家自然科学基金资助项目(61370083;61073043;61073041);教育部高等学校博士学科点专项科研基金资助项目(20112304110011;20122304110012);哈尔滨市科技创新人才研究专项基金资助项目(2011RFXXG015)
在验证多线程并发程序时,将基于无状态或有状态搜索的软件模型检测与动态偏序归约方法相结合,能大幅缩减待验证程序的状态空间,而动态偏序归约需不断利用当前候选回溯集更新相应回溯集,导致更新回溯集的计算成本过高。为此,形式化定义...
关键词：软件模型检测 动态偏序归约 有状态搜索 回溯集 收缩候选集 
基于ZING的Web服务建模与验证
《桂林电子科技大学学报》2011年第3期202-207,共6页陆晶晶 骆翔宇 
国家自然科学基金(60763004)
为了验证Web服务的正确性和可靠性等性质以及提高Web服务流程验证的自动化程度,提出了一种适合构造BPEL4WS(Web服务的业务流程执行语言)结构模型的输入输出标记迁移系统(I/OLTS)作为中间形式化模型,将BPEL转化为中间形式模型I/OLTS,然...
关键词：WEB服务 BPEL4WS I/OLTS 软件模型检测 
面向源代码的软件模型检测及其实现被引量：6
《计算机科学》2009年第1期267-272,共6页何恺铎 顾明 宋晓宇 李力 李江 
国家自然科学基金(No.60553002;No.90718039)支持
模型检测应用于检测软件可靠性具有重要意义。介绍了一种基于谓词抽象和反例引导抽象求精技术对源程序进行建模和验证的模型检测方法,并结合自行研发的Jchecker工具详细介绍了该软件模型检测技术的运作过程和关键算法。
关键词：软件模型检测 源程序验证 谓词抽象 抽象求精 面向源代码 
并行软件模型检测被引量：3
《计算机工程》2008年第19期23-25,29,共4页邝宏斌 罗贵明 
国家自然科学基金资助项目(60474026,60672110);清华大学研究基金资助项目;清华大学信息学院基金资助项目
并行化是提高模型检测效率的重要手段。该文研究了基于标号迁移系统的C程序模型检测,提出一种软件模型检测并行化的方法。该方法利用软件模型检测工具模块化验证(MAGIC)的模块化特性对C程序进行组件分解,将各组件均衡地分发到若干计算节...
关键词：并行模型检测 软件模型检测 标号迁移系统 模块化验证 
程序重构预处理在提高软件模型检测效率中的应用
《计算机研究与发展》2008年第8期1417-1422,共6页黄卫平 
湖南省科技厅科技计划基金项目(2007JT2006);湖南省教育厅科技资助项目(06b011)~~
针对软件模型检测目前很难处理大型程序的问题,提出用程序重构技术对待检的源代码进行预处理,以提高模型检测算法的效率.程序重构将大型程序分解成语义一致的小型过程的集合,由于模型检测算法中过程总结边可单独计算,而且在程序中对某...
关键词：软件模型检测 谓词抽象 程序重构 状态爆炸 过程总结 
基于层次单元划分的软件模型检测技术被引量：1
《计算机应用》2008年第8期2109-2112,共4页陈晨 陈永生 
通过对近年来软件模型检测领域流行的几种技术进行综述,提出了一种基于层次单元划分,使用引导式搜索方式的软件模型检测方案。本方案分为预处理、单元划分、状态空间搜索三个阶段,其中使用on-the-fly技术提高了搜索性能。实验证明,该方...
关键词：软件模型检测 层次单元划分 引导式搜索 
全选清除导出
共2页<12>
检索报告 对象比较 聚类工具 使用帮助 返回顶部