形式化

作品数：5172被引量：11555H指数：35
导出分析报告
相关领域：自动化与计算机技术文化科学更多>>
相关作者：关永施智平薛锦云张广泉段振华更多>>
相关机构：华东师范大学国防科学技术大学西安电子科技大学清华大学更多>>
相关期刊：更多>>
相关基金：国家自然科学基金国家高技术研究发展计划国家重点基础研究发展计划国家社会科学基金更多>>
-
在结果中检索

检索结果分析

结果分析中...
选择条件：
  • 期刊=计算机工程与应用x
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
面向适航标准的机载软件测试验证工具综述被引量：1
《计算机工程与应用》2021年第11期1-10,共10页刘友林 郑巍 谭莉娟 樊鑫 杨丰玉 
国家自然科学基金(61867004);江西省教育厅自然科学基金(GJJ180523)。
机载软件的测试与验证是保障机载软件正确性和可靠性的重要方法。软件的测试与验证离不开工具的支持,使用工具能够提高效率、降低成本,对机载软件的测试验证工具研究是对其进行充分测试验证的保障。对机载软件及适航标准进行了简介;按...
关键词：机载软件测试验证工具 适航标准 DO-178C 基于模型 形式化方法 
指挥控制协同能力需求体系形式化框架被引量：1
《计算机工程与应用》2020年第5期49-56,共8页柴磊 王智学 何明 
国家自然科学基金（No.61273210）
指挥控制协同性是实现信息化条件下联合作战指挥的关键。针对当前对指挥控制协同能力需求缺乏形式化描述和分析方法等问题,提出一种指挥控制协同能力需求形式化描述框架,运用进程代数方法对能力之间的关系以及操作进行形式化定义,消除...
关键词：指挥控制协同 能力需求 形式化 进程代数 
轻量级移动支付协议公平性分析被引量：4
《计算机工程与应用》2018年第19期82-87,共6页李茜 王峥 马建芬 李娜 
山西省重点研发计划国际合作项目(No.201603D421013)
为保证移动支付安全、顺利进行,必须采用安全的移动支付协议。针对计算和存储能力有限的移动设备和不可靠的移动环境,选择采用对称加密的轻量级移动支付协议PCMS,使用串空间理论对其建模,进行形式化分析。通过图的方式直观描述协议的执...
关键词：移动支付协议 形式化分析 串空间 公平性 模型检测 
穿刺机器人运动安全性的形式化分析与建模
《计算机工程与应用》2018年第18期263-270,共8页孙浩然 施智平 关永 王瑞 
国际科技合作计划(No.2010DFB10930,No.2011DFG13000);国家自然科学基金(No.61170304,No.61104035,No.61373034,No.61303014,No.61472468,No.61572331);北京市科委项目(No.Z141100002014001);北京市教委科研基地建设项目(No.TJSHG201310028014);北京市属高等学校创新团队建设与教师职业发展计划项目(No.NoIDsHT20150507)。
混成系统是实时嵌入式系统的重要子类,其行为中存在连续变化和离散跳转混杂的情况,使得混成系统行为复杂,安全性难以掌握。近年来,混成系统在医疗环境中得到越来越广泛的应用。其中,医疗机器人的穿刺运动控制系统呈现高度复杂的混成性,...
关键词：混成系统 医疗机器人 微分动态逻辑 微分不变式 形式化验证 
一种改进的满足后向安全的RFID双向认证协议被引量：8
《计算机工程与应用》2017年第9期136-140,共5页马远佳 刘道微 
广东省云机器人(石油化工)工程技术研究中心开放基金资助课题(No.201507B05);广东省石化装备故障诊断重点实验室开放基金(No.772715);广东省科研创强重点项目(No.2012B01040);广东省科技计划项目(No.2014A020208139)
针对在物联网应用中,现有的RFID双向认证协议存在认证效率低和安全隐患等问题,提出了一种满足后向安全的RFID双向认证协议,采用随机数使标签保持信息的新鲜性,从而实现标签与阅读器之间的双向认证;通过Rabin加密算法的运算单向性,来解...
关键词：物联网 射频识别 Rabin算法 BAN形式化分析 双向认证 
模型检测在完整性形式化验证中的应用研究被引量：1
《计算机工程与应用》2017年第4期59-63,134,共6页严亚伟 周雁舟 惠文涛 
对于信息系统而言,数据信息的安全性是十分重要的,数据的完整性是数据安全最重要的表现形式。为了确保系统中数据信息的安全性,提高系统可靠性,需要对数据的完整性进行分析和验证。针对数据完整性的定量评估问题,提出使用概率计算树逻...
关键词：完整性 形式化 概率分析 概率计算树逻辑 模型测试 
基于SPIN的远程证明协议的形式化分析及改进被引量：4
《计算机工程与应用》2017年第1期34-38,72,共6页秦嫚蔓 王峥 王莉 
国家高技术研究发展计划(863)项目(No.2014AA015204)
远程证明是解决移动支付安全问题的有效手段之一。通过对可信计算远程证明协议进行分析,发现用户平台配置信息的隐私性、用户的认证性和远程验证者的认证性存在脆弱点,使用SPIN模型检测工具,应用模型检测方法对协议进行了形式化分析,检...
关键词：移动支付 远程证明协议 用户属性 形式化分析 SPIN模型检测 
一种约束求解的Web应用测试数据生成与筛选方法被引量：2
《计算机工程与应用》2016年第18期214-221,共8页邓志丹 杨海燕 吴际 
传统基于随机算法、约束求解以及面向白盒测试的测试数据生成方法往往忽略了测试数据与数据库系统之间的依赖关系,同时并不适用于数据复用、Web应用测试。提出一种面向业务流程数据约束的测试数据生成与筛选方法,通过在Web业务流程模型...
关键词：WEB应用测试 测试数据 业务流程 半形式化描述 约束 数据复用 
车站联锁进路控制逻辑的形式化方法被引量：8
《计算机工程与应用》2016年第17期229-234,270,共7页胡晓辉 韩佳芮 
国家自然科学基金(No.61163009);甘肃省硕导项目(No.1104-05)
基于计算机联锁系统是一个对列车行驶系统提供安全条件的系统,车站联锁系统是保证车站行车安全和提高运输效率的典型安全苛求性系统。以形式化方法 Event-B为基础,引入角色Agent对联锁系统进行规范定义,通过智能体与Event-B的建模和验证...
关键词：联锁 进路控制 Event-B方法 多智能体系统(MAS) 
非确定性环境中移动机器人避障策略的验证——基于形式化建模和概率分析被引量：2
《计算机工程与应用》2016年第10期31-38,70,共9页王铭 王瑞 李晓娟 关永 张杰 魏洪兴 
国家自然科学基金(No.61373034;No.61303014);国际科技合作计划(No.2011DFG13000);北京市教委科研基地建设项目(No.TJSHG201310028014)
针对存在制动机误差和传感器噪声等因素的移动机器人,提出采用概率模型检测的方法对非确定性环境中移动机器人的避障策略进行验证和定量分析。首先将移动机器人的避障运动和动态障碍物的不确定性运动建模为马尔可夫决策过程。然后运用...
关键词：非确定性环境 移动机器人 避障 概率模型检测 马尔可夫决策过程 
全选清除导出
共12页<12345678910>
检索报告 对象比较 聚类工具 使用帮助 返回顶部