形式化方法

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

检索结果分析

结果分析中...
选择条件：
  • 期刊=小型微型计算机系统x
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
神经网络可信性的形式化验证方法综述被引量：3
《小型微型计算机系统》2022年第9期1830-1837,共8页王莉 李晓娟 关永 王瑞 王佳岳 
国家自然科学基金项目(61977040,61876111)资助;科技创新服务能力建设(20530290073)-首都师范大学交叉研究院项目(19530012005)资助.
随着神经网络技术的不断发展和完善,其应用也随之扩展,如何保证其可信性是在许多应用领域特别是安全攸关应用中部署的关键,目前对神经网络可信性研究主要体现在通过循环优化网络训练等过程和对神经网络进行验证两方面.基于形式化方法可...
关键词：神经网络 可信性属性 模型抽象 形式化方法 
一个基于形式化方法的系统安全性建模分析实例研究被引量：2
《小型微型计算机系统》2020年第2期327-332,共6页石梦烨 胡军 陈朔 唐红英 王立松 
南京航空航天大学研究生创新基地(实验室)开放基金项目(kfjj20181607)资助.
随着安全关键性系统的日益复杂,如何提高安全关键系统的安全性成为急需解决的问题.基于形式化模型的复杂系统设计与分析是一种重要的安全性分析方法.本文工作对AIR6110标准中的机轮刹车实例系统进行了基于形式化方法的安全性分析研究,包...
关键词：机轮刹车系统 AADL SLIM xSAP 故障树 FMEA表 
形式化建模运行在NAND闪存上的DFTL算法被引量：1
《小型微型计算机系统》2018年第1期89-94,共6页张必红 郭宇 李兆鹏 
国家自然科学基金项目(61202052;61103023;61632005;61229201)资助
为了保证一种非常经典的适用大规模存储地NAND闪存上的DFTL算法的正确性,对DFTL算法采用了形式化建模的方法来建立一个高可信的形式化模型.根据DFTL算法提出者的设计,我们以此为依据,对DFTL算法的基本数据结构,读写操作和垃圾回收操作...
关键词：形式化方法 形式化建模 Coq证明 闪存安全 信息安全 闪存转换层算法 
概率模型检测的网络传播干预策略被引量：1
《小型微型计算机系统》2017年第6期1175-1180,共6页李宙洲 魏欧 郭宗豪 余鹏 韩兰胜 
国家"九七三"重点基础研究发展计划项目(2014CB744904)资助;国家自然(61170043;61272033)资助
网络普遍存在于自然界和人类社会中,计算机病毒、传染疾病、森林火灾以及社会流言等在网络中的传播给经济、社会带来巨大挑战.寻找有效的干预策略实现对网络传播的控制是一个重要的研究问题.根据传播过程的内在规律,引入了概率网络传播...
关键词：概率模型检测 网络传播干预策略 近似模型检测方法 形式化方法 
使用模型检验自动化验证路由协议被引量：2
《小型微型计算机系统》2015年第11期2462-2466,共5页马银雪 陈哲 黄志球 黄吴丹 
国家自然科学基金项目(61100034)资助;中国博士后科学基金项目(20110491411;2012T50498)资助;江苏省博士后科研计划项目(1101092C)资助
模型检验可验证路由协议的收敛性,环路问题,包交付失败,由于协议描述的歧义导致的问题,安全性缺陷等.实验一建立关注链路状态数据库同步的OSPF模型,设置攻击者路由器伪造消息,找到攻击成功的反例;实验二建立关注节点加入、失效和相应处...
关键词：模型检验 路由协议验证 形式化方法 SPIN CBMC 
基于扩展SysML活动图的嵌入式系统设计安全性验证方法研究被引量：5
《小型微型计算机系统》2015年第3期408-417,共10页黄传林 黄志球 胡军 徐丙凤 曲长亮 
国家自然科学基金项目(61100034;61170043)资助;中国博士后科学基金项目(20110491411)资助;江苏省普通高校研究生科研创新计划资助项目;中央高校基本科研业务费专项资金(CXZZ11_0218)资助
能源、交通等领域中复杂嵌入式系统设计的安全性分析与验证工作已经成为当前的重要研究热点之一;本文提出一种结合MARTE语义信息的扩展Sys ML活动图模型,用于描述安全关键应用中的嵌入式系统动态行为的设计,并对此扩展模型展开基于模型...
关键词：嵌入式系统安全性分析 SysML活动图 MARTE 模型转换 形式化方法 
GJK算法的一种特殊情形的形式化验证和应用被引量：3
《小型微型计算机系统》2015年第2期365-369,共5页安育龙 施智平 叶世伟 李晓娟 张杰 魏洪兴 
国际科技合作计划项目(2010DFB10930,2011DFG13000)资助;国家自然科学基金项目(60873006,61070049,61170304,61104035,61373034,61303014)资助;北京市自然科学基金暨北京市教委重点项目(4122017,KZ201210028036)资助;北京市优秀人才培养项目资助;北京市属高校青年拔尖人才培育计划资助
计算几何算法经常用于机器人避碰运动规划等安全攸关领域,对这些算法进行正确性证明非常重要.用形式化方法对算法进行验证是一种十分有效的手段,尤其是定理证明的方法用严格的数学公理和定理推理证明逻辑模型的性质,对所验证的性质而言...
关键词：形式化方法 算法验证 机器人规划 定理证明 HOL 
基于模型转换的MARTE顺序图的形式化分析被引量：1
《小型微型计算机系统》2013年第1期100-106,共7页朱梅霞 王捍贫 刘西奎 韩晓琼 
国家自然科学基金项目(60873061)资助;国家"九七三"重点基础研究发展计划项目(2009CB320701;2010CB328103)资助
作为一项新规范,MARTE有许多方面亟待完善.如何对依照MARTE设计的模型开展验证是待解决问题之一.对象管理组织提出用模型转换的方法将依照MARTE设计的模型(记为A)转换成另一种具有完备的验证方法和工具的形式化模型(记为B),然后对B进行...
关键词：实时系统 形式化方法 MARTE 时间变迁系统 验证 
一个支持位运算形式化推理的抽象机
《小型微型计算机系统》2007年第1期88-92,共5页项森 陈意云 林春晓 
国家自然科学基金项目(60473068)资助.
程序推理使用的抽象机器与物理机器的差距降低了推理的精确度,为了缩小这个差距,本文提出了一个带位级别抽象的新抽象机,在这个机器里,二进制整数以纯语法的方式被表示成位矢量而不是非负整数.使用这个抽象机器,可以在其上进行许多带位...
关键词：形式化方法 程序验证 HOARE逻辑 程序设计中的逻辑 
反应式嵌入式系统形式化性能模型的研究
《小型微型计算机系统》2005年第11期2054-2056,共3页张冠华 张连华 白英彩 
基于进程代数EACSR-VP和形式化描述语言CPSL,介绍了如何建立和描述反应式嵌入式系统的形式化性能评价模型.该模型通过抽象去掉了实现了细节,是可执行的,利用其可以对不同的设计方案进行定量的性能验证,得到不同系统的性能指标并进行分...
关键词：嵌入式系统 进程代数 形式化方法 性能 
全选清除导出
共2页<12>
检索报告 对象比较 聚类工具 使用帮助 返回顶部