形式化描述

作品数:545被引量:1759H指数:18
导出分析报告
相关领域:自动化与计算机技术更多>>
相关作者:张广泉史建琦赵保华屈玉贵顾翔更多>>
相关机构:国防科学技术大学清华大学武汉大学中国科学技术大学更多>>
相关期刊:更多>>
相关基金:国家自然科学基金国家高技术研究发展计划国家教育部博士点基金国家重点基础研究发展计划更多>>
-

检索结果分析

结果分析中...
选择条件:
  • 期刊=计算机科学x
条 记 录,以下是1-10
视图:
排序:
面向DO-178C的襟缝翼控制系统需求的形式化描述
《计算机科学》2018年第4期196-202,共7页战芸娇 魏欧 胡军 
国家自然科学基金项目(61170043);国家重点基础研究发展计划(973)项目(2014CB744904);航空科学基金项目(20155552047)资助
DO-178C是对机载软件适航认证标准DO-178B的改进和补充,用于对民用飞机机载系统和设备软件质量控制提供指导。SCR(Software Cost Reduction)方法作为一种形式化方法,基于四变量模型,可以对复杂和大型的嵌入式系统进行需求描述。文中基于...
关键词:DO-178C SCR方法 四变量模型 机载软件 T-VEC 
软件漏洞静态检测模型及检测框架被引量:4
《计算机科学》2016年第5期80-86,116,共8页王涛 韩兰胜 付才 邹德清 刘铭 
基于任务的木马关联行为识别研究(61272033);移动网络行为的多态聚类及其演化研究(61272405);云计算安全基础理论与方法研究(2014CB340600)资助
软件漏洞静态分析是信息安全领域的重点研究方向,如何描述漏洞及判别漏洞是漏洞静态分析的核心问题。提出了一种用于描述和判别漏洞的漏洞静态检测模型。首先对软件漏洞的属性特征进行形式化定义,并对多种软件漏洞和其判定规则进行形式...
关键词:静态分析 漏洞检测 形式化描述 状态空间爆炸 中间表示 
树突细胞算法及其理论研究被引量:2
《计算机科学》2015年第2期131-133,156,共4页方贤进 王丽 康佳 刘佳 
国家自然科学基金(61240023)资助
树突细胞算法(DCA)是受先天性免疫系统中树突细胞(DCs)功能的启发而开发的算法,它已被成功运用于许多计算机安全相关领域。但是对DCA理论方面的分析工作很少,对算法大多数理论方面的研究也较少出现。而其它的人工免疫算法如负选择算法...
关键词:树突细胞算法 形式化描述 运行时间复杂度 
DTL-Real-Time Object-Z形式化规格说明语言及其责任授权模型描述被引量:2
《计算机科学》2014年第4期184-189,共6页马莉 钟勇 霍颖瑜 
广东省自然科学基金(10152800001000016);佛山市科技发展专项资金(2011AA100061);佛山市产学研专项资金(2012HC10027)资助
Object-Z语言缺乏完整的时态描述能力,如无法表达操作在特定时间之后执行或按某种周期执行等,也不具有操作补偿等概念。针对这些问题,在Object-Z中集成实时概念和分布式时态逻辑,提出DTL-Real-Time Object-Z规格语言,该语言能有效地描...
关键词:形式化描述语言 责任授权模型 OBJECT-Z 分布式时态逻辑 
SIMD指令集设计空间的形式化描述被引量:1
《计算机科学》2013年第6期32-36,共5页李春江 徐颖 黄娟娟 杨灿群 
国家自然科学基金项目(61170046,61170045)资助
SIMD(Single-Instruction-Multiple-Data)并行体系结构在现代处理器体系结构中扮演非常重要的角色。SIMD指令集已经成为处理器指令集中重要的子集。SIMD结构和指令集实现了短向量并行处理能力,SIMD指令集实现了对多种数据类型、多种操...
关键词:SIMD 指令集 设计空间 形式化描述 
微内核架构多线程机制的形式化设计研究被引量:5
《计算机科学》2013年第4期136-141,163,共7页钱振江 卢亮 黄皓 
国家高技术研究发展计划(863)(2011AA01A202);江苏省"六大人才高峰"高层次人才项目(2011-DZXX-035);江苏省高校自然科学研究项目(12KJB520001)资助
微内核架构因其有效的模块隔离性而成为操作系统方面研究的热点,多线程机制是微内核架构需要解决的关键性能问题。有不少的工作对微内核架构多线程机制进行了研究,但存在频繁的系统地址空间切换和实现复杂度高的问题。采用形式化的方式...
关键词:微内核 多线程 操作系统 形式化描述 形式化设计 
基于协议的实时构件行为一致性验证被引量:2
《计算机科学》2012年第6期125-128,142,共5页张振领 贾仰理 谢圣献 李舟军 
国家自然科学基金项目(90718017);山东省自然科学基金项目(ZR2011FL023);山东省软科学项目(2010RKE16007);山东省高校智能信息处理与网络安全重点实验室(聊城大学)资助
对复杂实时构件系统行为进行形式化描述和一致性验证,可以提高实时构件的可复用性和系统的正确性、可靠性。分析了时间行为协议TBP(Timed Behavior Protocol)及其它学术界和工业界常用的时序行为形式化描述方法,对实时构件替换理论进行...
关键词:实时构件 时间行为协议 形式化描述 一致性验证 
基于XYZ/ADL的网络中心化仿真运行支撑平台体系结构形式化描述被引量:2
《计算机科学》2012年第B06期365-369,共5页孙黎阳 毛少杰 林剑柠 刘中 
网络中心化仿真运行支撑平台体系结构是为了满足动态构建仿真任务共同体而提出的相应支撑环境。采用基于XYZ/ADL的双重软件体系结构描述框架,分别从图形语言和形式语言对仿真运行支撑平台体系结构进行了描述并对仿真任务共同体构建中仿...
关键词:网络中心化仿真 任务共同体 运行支撑平台体系结构 体系结构描述语言 XYZ/ADL 
软件体系结构层切点指示器的形式化描述方法被引量:2
《计算机科学》2012年第1期124-129,共6页倪友聪 叶鹏 杜欣 肖如良 张琳琳 
福建省自然科学基金项目(2011J05146);福建省教育厅项目(JB11029);湖北省教育厅科学技术研究项目(B20111607);新疆维吾尔自治区高校科研计划青年教师科研培育基金(XJEDU2009S15);新疆大学博士毕业生科研启动基金项目(BS090142)资助
软件体系结构层切点指示器是在软件体系结构层次上实现量化机制和描述方面编织的基础。一些面向方面软件体系结构的描述语言虽然引入了切点指示器(Pointcut Designator)的语法成分,但仍未给出其语义的形式化描述,因而难以精确刻画软件...
关键词:面向方面软件体系结构 面向方面软件体系结构描述语言 方面编织 切点指示器 
一种适用于电子病历系统的使用控制模型被引量:1
《计算机科学》2010年第11期190-193,共4页王莹 陈伟鹤 鞠时光 
国家自然科学基金(60603041;60773049);江苏省教育厅自然科学基金(09KJB520003);江苏大学高级人才启动基金(07JDG031)资助
通过分析采用传统访问控制的电子病历系统存在的不足,提出了一种使用新一代访问控制模型——使用控制模型(UCON,usage control)思想的电子病历系统,并给出了具体的访问控制策略及其形式化描述。
关键词:电子病历 使用控制 形式化描述 
检索报告 对象比较 聚类工具 使用帮助 返回顶部