模型检测工具

作品数：11被引量：81H指数：3
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：段振华徐雨波吴尽昭张轶冯庆奎更多>>
相关机构：中国科学院软件研究所西安电子科技大学中国科学院大学中国科学院成都计算机应用研究所更多>>
相关期刊：《计算机工程与设计》《计算机应用与软件》《计算机应用研究》《信息安全研究》更多>>
相关基金：国家自然科学基金国家重点基础研究发展计划国家高技术研究发展计划国家教育部博士点基金更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
基于约束依赖图的并发程序模型检测工具
《软件学报》2023年第7期3064-3079,共16页苏杰 杨祖超 田聪 段振华 
国家自然科学基金(62192730,62192734,61732013,62172322);科技创新2030——“新一代人工智能”重大项目(2018AAA0103202)。
模型检测是一种基于状态空间搜索的自动化验证方法,可以有效地提升程序的质量.然而,由于并发程序中线程调度的不确定性以及数据同步的复杂性,对该类程序验证时存在更为严重的状态空间爆炸问题.目前,大多采用基于独立性分析的偏序约简技...
关键词：约束依赖图 偏序约简 并发程序 模型检测 工具 
无人机无线通信协议的形式化认证分析与验证被引量：2
《计算机测量与控制》2021年第4期244-250,共7页刘栋 连晓峰 王宇龙 谭励 赵宇琦 李林 
装备发展部项目(170341402020)。
针对无人机组与地面控制站之间进行无线通信时的身份认证问题,首先分析无线通信协议的工作流程及其形式化表示,然后对网络系统中的诚实主体和攻击者进行形式化建模,其中推导了协议安全属性的LTL公式,通过建立密钥机制,实现控制站与无人...
关键词：无人机无线通信协议 形式化表示与建模 模型检测工具SPIN 攻击者知识项获取 
基于SMV模型检测工具的分布式动漫渲染系统软件建模与分析被引量：1
《黑龙江大学自然科学学报》2020年第3期362-366,共5页洪志国 王永滨 石民勇 于水源 
国家科技支撑计划课题资助项目(2013BAH54F03);中国传媒大学优秀中青年教师培养工程资助项目(YXJS201508);中国传媒大学理工科规划项目(3132015XNG1504)。
利用网络资源搭建分布式动漫渲染系统是提升渲染速度、克服动漫制作效率瓶颈的有效方式。分布式动漫渲染系统软件的健壮性和可用性是渲染系统稳定高效运行的重要保障。因此,从模型检测角度对软件开发进行建模与分析将有效地预防和消除...
关键词：模型检测 动漫渲染 SMV 状态机 
智能合约的形式化验证方法被引量：65
《信息安全研究》2016年第12期1080-1089,共10页胡凯 白晓敏 高灵超 董爱强 
国家自然科学基金项目(91538202)
智能合约是一种代码合约和算法合同,将成为未来数字社会的基础技术,它利用协议和用户接口,完成合约过程的所有步骤.总结了智能合约主要技术特点和现存的可信、安全等问题,提出将形式化方法应用于智能合约的建模、模型检测和模型验证过程...
关键词：智能合约 形式化方法 建模 验证 SPIN模型检测工具 
RGPS过程层元模型正确性验证被引量：1
《计算机工程》2012年第15期39-42,共4页袁开银 郭瑞 陆翔升 吴尽昭 
国家"863"计划基金资助项目"基于代数符号计算的新型软件形式化验证技术和支持工具"(2007AA01Z143)
利用Web服务本体描述语言对RGPS过程层元模型进行描述,建立Promela模型。基于线性时序逻辑,以及Spin检测工具的偏序规约和on-the-fly等优化技术对Promela模型进行正确性验证,设计并实现RGPS过程层元模型正确性验证平台。通过城市交通系...
关键词：RGPS框架 Promela建模 Spin模型检测工具 过程层元模型 线性时序逻辑 
基于一阶迁移系统的限界模型检测工具实现
《计算机工程与设计》2010年第1期118-121,136,共5页冯庆奎 
为了简化在限界模型检测过程中模型的建立过程,给出了一种采用基于一阶迁移系统语言的模型建立方法,并在此一阶迁移系统语言中加入了通道的功能,增强了描述能力。然后在此基础上完成了一个以基于插值和k步归纳的限界验证算法为核心的模...
关键词：限界模型检测 一阶迁移系统 通道 验证算法 协议分析 
基于Groebner基的模型检测技术及其工具实现
《计算机应用》2009年第10期2841-2843,共3页廖紫骅 谭红艳 吴尽昭 
国家863计划项目(2007AA01Z143);国家973计划项目(2007CB310803)
为了减少运算复杂度和运算时间,优化检测的性能,使得计算过程更加快速高效,在符号化模型检测的过程中,利用G roebner基进行多项式约化,设计出新的模型检测算法。并且基于该算法开发出新的符号模型检测工具。该工具能更快速地验证各软件...
关键词：符号模型检测 GROEBNER基 多项式环 不动点 模型检测工具 
着色Petri网模型检测工具的扩展及其在Web服务组合中的应用被引量：8
《计算机研究与发展》2009年第8期1294-1303,共10页门鹏 段振华 
国家自然科学基金项目(60433010;60873018);教育部高等学校博士学科点基金项目(200807010012)~~
Web服务组合的形式化描述和验证是一个重要的研究问题.为了更好地完成验证工作,提出了扩展着色Petri网的模型检测方法.首先,在着色Petri网原有的基于CTL的局部模型检测算法基础上,给出了获取模型检测证据/反例的算法,并在着色Petri网模...
关键词：着色PETRI网 WEB服务组合 形式化验证 模型检测 时序逻辑 
模型检测在软件需求分析及设计中的应用被引量：3
《计算机应用与软件》2009年第4期128-130,共3页贺亚博 郝克刚 葛玮 
模型检测技术因其完全自动化并且验证速度快的优点在硬件及协议的验证中广泛应用,近年来在软件领域的应用研究也不断涌现。总结了模型检测在软件需求分析及设计中已有的应用技术,包括利用模型检测工具对RSML,SCR和UML图形的检测,以及直...
关键词：模型检测 模型检测工具 直接检测 
一种基于有限精度时间自动机的模型检测工具被引量：1
《计算机应用研究》2006年第5期121-125,共5页徐雨波 晏荣杰 
国家自然科学基金资助项目(60273025);国家"973"计划资助项目(2002CB312200)
基于有限精度时间自动机模型,实现了一种新的数据结构———SDS,用SDS符号化表示状态空间的实时系统模型检测工具,并进行了初步的实验分析,取得了良好的效果。
关键词：模型检测工具 实时系统 数据结构 有限精度 时间自动机 
全选清除导出
共2页<12>
检索报告 对象比较 聚类工具 使用帮助 返回顶部