形式化分析

作品数：446被引量：1033H指数：13
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：王亚弟文静华韩继红冯登国张玉清更多>>
相关机构：解放军信息工程大学西安电子科技大学贵州大学中国科学院研究生院更多>>
相关期刊：更多>>
相关基金：国家自然科学基金国家高技术研究发展计划国家重点基础研究发展计划国家科技重大专项更多>>
-
在结果中检索

检索结果分析

结果分析中...
选择条件：
  • 基金=国家科技支撑计划x
共 条 记 录，以下是1-8
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
火灾报警系统数据输出协议的形式化分析
《计算机系统应用》2014年第11期218-223,共6页李志刚 
国家"十二五"科技支撑计划(2012BAK21B03)
火灾自动报警系统数据输出通信协议的理解和实现直接影响到通讯双方的兼容性.本文结合协议的应用环境和功能需求,利用形式化分析方法对协议进行剖析,给出协议的Petri网模型,将标准中隐含的、影响兼容性的要求明确化,探讨该协议的网络化...
关键词：消防 火灾自动报警 通信协议 形式化分析 
基于随机Petri网的GSM-R越区切换成功率的形式化分析被引量：1
《华东交通大学学报》2012年第4期73-80,共8页张友兵 刘岭 何祖涛 
科学技术部国家科技支撑计划项目(2009BAG12A08)
首先建立了基于随机Petri网的GSM-R越区切换模型,在模型中综合考虑了信道故障、信道占用和越区切换参数配置不合理等影响越区切换成功率的因素。其次,说明了随机Petri网与马尔可夫链的关系,以及使用马尔可夫链分析"GSM-R越区切换的随机P...
关键词：随机PETRI网 CTCS GSM-R 越区切换 马尔可夫链 
基于有色Petri网的CTCS-3级列控系统RBC切换的建模与形式化分析被引量：18
《铁道学报》2012年第7期49-55,共7页张友兵 唐涛 
国家科技支撑计划(2009BAG12A08)
在CTCS-3级列控系统中,车载设备在执行RBC切换过程中所用时间的长短和切换成功概率的大小,严重影响着列车的运行效率。本文利用有色Petri网对车载设备进行RBC切换的两种方式分别建模,模型中引入GSM-R故障模型和非周期消息模型,模拟在GS...
关键词：CTCS 有色PETRI网 RBC切换 车载设备 
列车运行控制系统中安全通信协议的形式化分析被引量：11
《铁道学报》2012年第7期70-76,共7页陈黎洁 单振宇 唐涛 
国家科技支撑计划(2009BAG14B01);国家自然科学基金(60634010)
安全通信协议是保证基于通信的列车运行控制系统中通信安全的主要因素,其性质和最终实现正确的形式化验证具有重要意义。本文将欧洲列车运行控制系统安全通信协议规范中的一些未强制规定的要求明确化,选择分层赋时有色Petri网(CPN)对修...
关键词：安全通信协议 ETCS EURORADIO 有色PETRI网 形式化分析 
公平交换协议形式逻辑被引量：2
《软件学报》2011年第3期509-521,共13页陈明 吴开贵 吴长泽 徐洁 吴中福 
国家自然科学基金(90818028);国家科技支撑计划(2008BAH37B04)
在深入分析公平交换协议现有研究和各项安全属性的基础上,由于信任逻辑方法难以分析乐观公平交换协议的公平性和时限性,提出一种公平交换协议形式化模型和推理逻辑.新模型将信道错误转化为攻击行为,将参与者分为诚实与不诚实两类,并将...
关键词：异步通信 公平交换 形式化分析 推理逻辑 模型检查 
基于SVO逻辑的云服务安全形式化分析被引量：4
《小型微型计算机系统》2010年第12期2438-2441,共4页陈丹伟 黄秀丽 孙国梓 
科技部国家"十一五"科技支撑计划项目(2007BAK34B06)资助;南京邮电大学攀登计划项目(NY208009)资助
云服务安全方案利用SAML实现SSO功能,使云用户只需要登录网络时进行一次身份认证即可接入各种云服务,从而提高网络认证效率,同时使SAML不需要保存用户的状态,有效提高SAML的性能.SVO逻辑一种基于推理的结构性方法,它具有十分简洁的推理...
关键词：云服务 SAMLSSO 形式化分析 SVO逻辑 
发布/订阅通信模式的实时性能分析与评估被引量：10
《计算机工程》2010年第20期229-231,共3页刘旭军 马跃 于东 
科技部国家科技支撑计划基金资助重点项目(2007BAP20B01);中国科学院知识创新工程重要方向基金资助项目(KGCX2-YW-119)
运用成熟的队列理论知识,通过PRISM模型验证工具,对发布/订阅模式的实时性能进行形式化分析。实验结果表明,发布/订阅模式在消息响应时间及消息传输可靠性两方面比传统的通信模式表现出更良好的性能,该实验模型和实验方法对于优化发布/...
关键词：发布/订阅 队列理论 实时性 形式化分析 
基于实时发布订阅模式的数控总线通信机制研究被引量：2
《小型微型计算机系统》2009年第10期1994-2000,共7页胡毅 于东 岳东峰 刘旭军 黄骏 
国家"高档数控机床与基础制造装备"科技重大专项(2009ZX04009-013)资助;科技部国家科技支撑计划(2007BAP20B01)资助
在研究传统通信机制基础上,针对数控总线特点,本文提出一种新型基于实时发布订阅模式的数控总线通信机制.详细阐述该机制的核心部件消息中间件的设计过程,采用形式化方法对这种机制进行分析,构建出基于概率时间自动机的系统状态转换模型...
关键词：数控总线 RTPS机制 形式化分析 模型验证 
全选清除导出
共1页<1>
检索报告 对象比较 聚类工具 使用帮助 返回顶部