云南高校图书馆联盟文献共享服务平台- 有界模型检测

有界模型检测: 作品数：21被引量：38H指数：4; 导出分析报告; 相关领域：自动化与计算机技术更多>>; 相关作者：杨晋吉苏开乐骆翔宇肖茵茵侯刚更多>>; 相关机构：中山大学桂林电子科技大学中国科学院软件研究所北京大学更多>>; 相关期刊：《通信学报》《计算机应用与软件》《计算机应用研究》《小型微型计算机系统》更多>>; 相关基金：国家自然科学基金广东省自然科学基金国家重点基础研究发展计划国家杰出青年科学基金更多>>

航天嵌入式软件整数溢出的形式化验证方法被引量：2: 《软件学报》2021年第10期2977-2992,共16页高猛滕俊元王政; 国家自然科学基金(61802017);装备预研领域基金(61400020407)。; 整数溢出引起的软件系统安全性问题屡见不鲜,已有的模型检测技术由于存在状态空间爆炸、不能有效支持中断驱动型程序检测等缺点而少有工程应用.结合真实案例,对航天嵌入式软件整数溢出问题的分布和特征进行了系统性的分析.在有界模型检...; 关键词：航天嵌入式软件整数溢出有界模型检测中断驱动型程序顺序化

基于有界模型检测的门级软件自测试方法: 《同济大学学报（自然科学版）》2018年第11期1575-1581,共7页张颖张嘉琦王真江建慧; 国家自然科学基金(61432017;61404092); 提出了基于有界模型检测的门级软件自测试方法.将处理器中的模块简化成约束模块,缓解状态爆炸问题.将难测故障的触发条件逐个转化成性质并且采用有界模型检测技术,搜索触发这些性质的违例.最后,将违例映射成测试指令序列,并为测试指令...; 关键词：基于软件的自测试(SBST) 模型检测抽象

基于程序局部性引导的有界模型检测优化方法: 《通信学报》2018年第3期181-190,共10页王舜杜晔韩臻刘吉强; 北京高校青年英才计划基金资助项目(No.YETP0548);国家自然科学基金资助项目(No.61672092)~~; 基于多种模型检测方法组合的复合检测方式是当前软件模型检测领域开展研究的热点之一。在当前的研究中,提高检测的规模和检测的对象复杂程度的关键在于如何有效处理抽象的扩张和收缩。证明通过对程序模式或验证信息的利用可以加快状态...; 关键词：模型检测 BMC 软件检测局部性优化

基于半张量积的完备性阈值求解方法: 《计算机应用研究》2016年第9期2641-2644,共4页许海洋庄毅刘振斌; 国家自然基金面上资助项目(61572253);国家自然科学基金青年科学基金资助项目(61403223); 为了精确地计算Kripke模型的完备性阈值,将半张量积引入到有界模型检测的完备性阈值的计算中,采用离散时间进化系统来研究Kripke模型的状态进化拓扑结构,提出了基于半张量积的有界模型检测完备性阈值的求解算法。通过实例说明了该方法...; 关键词：有界模型检测完备性阈值半张量积离散时间系统

基于有界模型检测的C/C++程序内存泄露检测被引量：1: 《电脑迷》2016年第7期173-,共1页蔡程; 前言:C/C++是一种应用十分之广泛的程序设计语言,在动态内存管理机制中应用具有显著的优势,但是程序编程人员在实际应用中所出现的错误,容易造成动态内存管理机制出现内存泄露问题,严重影响程序应用性能,甚至可能直接造成程序的瘫痪。...; 关键词：内存泄露检测方案程序 C/C 有界模型检测

基于有界模型检测的C/C++程序内存泄露检测被引量：2: 《计算机应用研究》2016年第6期1762-1766,共5页黄蔚洪玫杨秋辉郭鑫宇代声馨徐保平高婉玲赵鹤; 四川省应用基础研究项目(2014JY0112); C/C++语言中的动态内存管理机制自由且灵活,但动态内存的使用容易引入内存泄露,导致系统性能降低甚至系统崩溃。为了更加有效地检测内存泄露,提出了一个基于有界模型检测技术的C/C++程序内存泄露检测方案MLD-CBMC。该方案以C/C++程序文...; 关键词：C/C++程序内存泄露有界模型检测可满足性模理论

基于CBMC有界模型检测的无线抄表路由协议验证: 《计算机应用与软件》2016年第4期138-142,共5页胡世超杨红丽秦胜潮王非刘渊; 针对工业界实现的无线抄表路由协议WM2RP(Wireless Meter Reading Routing Protocol),提出将CBMC有界模型检测工具运用到该协议实现的验证方法。WM2RP协议实现是嵌入式C程序,CBMC工具主要针对嵌入式软件的验证,运用CBMC对WM2RP进行验证...; 关键词：模型检测 WM2RP路由协议 CBMC

ROS中XML-RPC协议实现的形式化验证被引量：3: 《小型微型计算机系统》2015年第12期2629-2633,共5页贾娟娟施智平关永李勇坚魏洪兴; 国际科技合作计划项目(2010DFB10930,2011DFG13000)资助;国家自然科学基金项目(61070049,61170304,61104035,61373034,61303014,61472468)资助;北京市教委科研基地建设项目(TJSHG201310028014)资助;北京市属高等学校创新团队建设与教师职业发展计划项目(IDHT20150507)资助;北京市优秀人才培养资助项目资助;北京市属高校青年拔尖人才培育计划项目资助; XML-RPC协议是ROS节点通讯的核心调用机制,其实现的正确性关乎整个系统的顺利运行.使用模型检测和定理证明结合的方法对ROS系统中的XML-RPC协议进行验证.首先使用CBMC模型检测工具逐个验证协议源代码的函数,然后对模型检测不能全面验证...; 关键词：ROS系统 XML-RPC协议有界模型检测定理证明 CBMC

使用事件自动机规约的C语言有界模型检测被引量：4: 《软件学报》2014年第11期2452-2472,共21页阚双龙黄志球陈哲徐丙凤; 国家自然科学基金(61272083;61100034); 提出使用事件自动机对C程序的安全属性进行规约,并给出了基于有界模型检测的形式化验证方法.事件自动机可以规约程序中基于事件的安全属性,且可以描述无限状态的安全属性.事件自动机将属性规约与C程序本身隔离,不会改变程序的结构.在事...; 关键词：事件自动机可满足性模理论有界模型检测自动机可达树安全关键软件

基于时间Petri网的嵌入式系统中断建模与验证: 《计算机科学》2014年第9期205-209,219,共6页周宽久常军旺侯刚任龙涛王小龙; 国家自然科学基金:航天多核嵌入式软件可信性验证与系统原型(61272174)资助; 嵌入式系统为中断驱动系统,但中断触发的随机性和不确定性导致中断缺陷很难被追踪发现,并且一旦发生中断故障,往往会使整个嵌入式系统陷入崩溃。因此必须保证中断系统软件的可信性,但是目前缺乏有效的中断系统资源冲突检测方法。针对上...; 关键词：中断建模有界模型检测时间自动机可满足性模理论时间PETRI网

有界模型检测