形式化方法

作品数：863被引量：2365H指数：18
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：薛锦云肖美华张广泉黄志球胡军更多>>
相关机构：华东师范大学中国科学院软件研究所上海交通大学南京大学更多>>
相关期刊：更多>>
相关基金：国家自然科学基金国家高技术研究发展计划国家重点基础研究发展计划中央高校基本科研业务费专项资金更多>>
-
在结果中检索

检索结果分析

结果分析中...
选择条件：
  • 期刊=计算机工程与科学x
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
图数据压缩技术综述被引量：2
《计算机工程与科学》2020年第1期89-97,共9页李凤英 杨恩乙 董荣胜 
国家自然科学基金(61762024);广西自然科学基金(2017GXNSFDA198050,2016GXNSFAA380054);桂林电子科技大学研究生创新创业项目(2019YCXS053)
应用合适的压缩技术对包含上亿个节点和边的图数据进行紧凑准确的表示和存储是对大规模图数据进行分析和操作的前提。紧凑的图数据表示不仅可以降低图数据的存储空间,而且还可以支持在图数据上的高效操作。从图数据的存储角度出发对图...
关键词：邻接矩阵 邻接表 形式化方法 图压缩 
航空机载嵌入式控制软件需求建模的形式化工程方法被引量：7
《计算机工程与科学》2019年第6期1016-1025,共10页黄怿豪 冯劲草 郑寒月 缪炜恺 蒲戈光 
国防科工局项目(JCKY 2016212B004-2)
嵌入式控制软件是现代航空飞行器的核心部件之一。构建软件需求的形式化规约精确地刻画人们对软件期望的功能和运行场景,是确保此类安全攸关软件质量的根本途径。在工业界,形式化需求建模的大规模应用尽管有成功的案例,但仍面临众多的...
关键词：软件需求建模 需求确认 形式化工程方法 形式化方法 
RFID超轻量级认证协议RCIA形式化分析与改进被引量：6
《计算机工程与科学》2018年第12期2183-2192,共10页钟小妹 肖美华 李伟 谌佳 李娅楠 
国家自然科学基金(61163005;61562026);江西省主要学科学术与技术带头人项目(2017XSDTR0105);江西省自然科学基金(20161BAB202063);江西省教育厅科技项目(GJJ170384)
无线射频识别(RFID)是物联网中的一种非接触式的自动识别技术,被广泛运用于构建物物互联的RFID系统。RCIA是一种超轻量级RFID双向认证协议,提供高安全性并声称能抵御去同步攻击。形式化方法是安全协议分析的有力手段。运用模型检测工具S...
关键词：RFID RCIA协议 形式化方法 模型检测 去同步攻击 
服务组合的代数规约被引量：1
《计算机工程与科学》2018年第6期1075-1083,共9页陈颖 刘冬梅 朱鸿 兰斌 何娟娟 
国家自然科学基金(61502233,61402229);江苏高校”青蓝工程”;中央高校基本科研业务费专项资金(30916011328);欧盟移动云计算FP7项目MONICA(PIRSES-GA-2011-295222)
现有的服务组合描述途径不能有效地验证和测试组合正确性,针对这一问题,提出了一个代数规约方法,引入规约包机制扩展面向服务代数规约语言SOFIA以支持该方法。用代数规约单元描述服务系统中的各种实体,其中基调部分定义实体的语法和结构...
关键词：WEB服务 服务组合 代数规约 形式化方法 
基于事件逻辑的无线Mesh网络认证协议安全性证明被引量：6
《计算机工程与科学》2017年第12期2236-2244,共9页李娅楠 肖美华 李伟 梅映天 钟小妹 
国家自然科学基金(61562026);江西省自然科学基金(20161BAB202063);江西省对外科技合作项目(20151BDH80005);江西省主要学科学术和技术带头人资助计划(2017BCB22015)
无线Mesh网络是一种结合无线局域网和移动自组织网络的新型多跳网络,无线网络的开放性和资源受限性使得无线网络容易遭受重放、伪装等攻击。事件逻辑是一种描述并发与分布式系统中状态迁移和算法的形式化方法,可用于证明网络协议的安全...
关键词：形式化方法 事件逻辑 无线Mesh网络认证协议 中间人攻击 
时钟有限自动机模型及其演化算法
《计算机工程与科学》2017年第2期378-384,共7页范林军 史湘宁 凌云翔 
国家自然科学基金(61272336)
传统分布仿真系统时钟不一致影响因素分析方法,已不能满足当前面向服务分布仿真的时钟状态分析需要。从系统全局时钟演化出发,阐述了时钟状态演化内涵与过程;在此基础上,基于有限自动机理论,提出了用于时钟不一致影响因素量化分析的动...
关键词：计算机应用 分布式系统 时钟一致性演化 因素量化分析 有限自动机 形式化方法 
基于事件逻辑的改进Needham-Schroeder协议安全性证明被引量：4
《计算机工程与科学》2015年第10期1850-1855,共6页刘欣倩 肖美华 程道雷 梅映天 李伟 
国家自然科学基金资助项目(61163005);计算机软件新技术国家重点实验室开放课题资助项目(KFKT2012B18);江西省自然科学基金资助项目(20132BAB201033);江西省高校科技落地计划资助项目(KJLD13038);江西省对外科技合作技术资助项目(20151BDH80005);华东交通大学研究生创新计划资助项目(YC2014-X007)
安全协议是现代网络安全的基础,密码协议的安全性证明是一个挑战性的问题。事件逻辑是一种描述分布式系统中状态迁移的形式化方法,用于刻画安全协议的形式化描述,是定理证明的基础。用事件序语言、事件类和一个表示随机数、密钥、签名...
关键词：事件逻辑 改进的Needham-Schroeder协议 形式化方法 强认证性理论 
一种结合AADL和IMC的系统可靠性建模方法被引量：5
《计算机工程与科学》2015年第8期1517-1524,共8页程亦涵 黄志球 阚双龙 
随着嵌入式软件在安全关键领域广泛应用,系统可靠性随着其规模、复杂度和性能需求的不断提升而愈显重要。结构分析设计语言AADL是应用于嵌入式领域的体系结构建模、分析和验证的重要手段。由于AADL是一种半形式化模型,需要精确描述其语...
关键词：AADL 可靠性模型 IMC模型转换 形式化方法 
复杂串联系统的状态空间生成的形式化分析
《计算机工程与科学》2009年第A01期231-233,共3页郑霄 赖新 王丽 田涛 
国家863计划资助项目(2007AA01Z117);国家973计划资助项目(2007CB310900)
大规模系统的模型状态空间生成过程由于状态空间的规模没有预先估计而不可控,形式化分析有利于解决这一问题。本文针对复杂串联系统的特殊结构,采用形式化方法分析研究了它的状态空间生成规律,从而达到快速预估模型状态空间规模的目的。
关键词：状态空间生成 形式化方法 复杂串联系统 
集成CCS和B语言的形式化方法被引量：2
《计算机工程与科学》2007年第11期102-104,共3页匡春临 潘孝铭 蒋胜利 
华侨大学高层次人才科研启动基金资助项目
本文尝试集成通信系统演算(CCS)和B语言,以扩展CCS在数据和操作定义方面的能力,以及B方法在描述并发系统方面的能力。集成后的形式化模型BCCS可以描述和分析系统的不同方面(结构、控制、数据和功能)和不同类型的系统(顺序、并发和分布式)。
关键词：形式化方法 CCS 集成 
全选清除导出
共2页<12>
检索报告 对象比较 聚类工具 使用帮助 返回顶部