检索结果-内蒙古大学图书馆

软件学报 2023年第8期34卷 3686-3707页

作者：李希萌王国辉张倩颖施智平关永首都师范大学信息工程学院北京100048 电子系统可靠性技术北京市重点实验室(首都师范大学) 北京100048 北京成像理论与技术高精尖创新中心(首都师范大学) 北京100048

各类安全攸关系统的可靠运行离不开软件程序的正确执行.程序的演绎验证技术为程序执行的正确性提供高度保障.程序语言种类繁多,且用途覆盖高可靠性场景的新式语言不断涌现,难以为每种语言设计支撑其程序验证任务的整套逻辑规则,并证明... 详细信息

各类安全攸关系统的可靠运行离不开软件程序的正确执行.程序的演绎验证技术为程序执行的正确性提供高度保障.程序语言种类繁多,且用途覆盖高可靠性场景的新式语言不断涌现,难以为每种语言设计支撑其程序验证任务的整套逻辑规则,并证明其相对于形式语义的可靠性和完备性.语言无关的程序验证技术提供以程序语言的语义为参数的验证过程及其可靠性结果.对每种程序语言,提供其形式语义后可直接获得面向该语言的程序验证过程.提出一种面向大步操作语义的语言无关演绎验证技术,其核心是对不同语言中循环、递归等可导致无界行为的语法结构进行可靠推理的通用方法.特别地,借助大步操作语义的一种函数式形式化提供表达程序中子结构所执行计算的能力,从而允许借助辅助信息对子结构进行推理.证明所提出验证技术的可靠性和相对完备性,通过命令式、函数式语言中的程序验证实例初步评估了该技术的有效性,并在Coq辅助证明工具中形式化了所有理论结果和验证实例,为基于辅助证明工具实现面向大步语义的语言无关程序验证工具提供了基础.

关键词：程序验证大步操作语义定理证明 Coq定理证明器

来源：评论

学校读者我要写书评

暂无评论

以太坊中间语言的可执行语义

引用

软件学报 2021年第6期32卷 1717-1732页

作者：韩宁李希萌张倩颖王国辉施智平关永首都师范大学信息工程学院北京100048 电子系统可靠性技术北京市重点实验室(首都师范大学) 北京100048 北京成像理论与技术高精尖创新中心(首都师范大学) 北京100048

智能合约是实现各类区块链应用的核心软件程序.近期,以太坊区块链平台(Ethereum)上的智能合约暴露出大量错误和安全隐患,在国际上引发了智能合约形式化验证的研究热潮.为提供高可信度的验证结果,智能合约程序语言的形式化必不可少.对以... 详细信息

智能合约是实现各类区块链应用的核心软件程序.近期,以太坊区块链平台(Ethereum)上的智能合约暴露出大量错误和安全隐患,在国际上引发了智能合约形式化验证的研究热潮.为提供高可信度的验证结果,智能合约程序语言的形式化必不可少.对以太坊中间语言Yul进行形式化,首次给出了其类型系统和小步操作语义的形式化定义.该语义为可执行语义(executable semantics),由120个Yul语言程序组成的测试集进行测试.该工作在Isabelle/HOL证明辅助工具中完成,为基于定理证明的智能合约正确性、安全性验证奠定了基础.

关键词：智能合约 Yul语言 Isabelle/HOL 形式化语义以太坊

来源：评论

学校读者我要写书评

暂无评论

机器人碰撞检测方法形式化

引用

软件学报 2022年第6期33卷 2246-2263页

作者：陈善言关永施智平王国辉首都师范大学信息工程学院北京100048 电子系统可靠性与数理交叉学科国家国际科技合作示范型基地(首都师范大学) 北京100048 轻型工业机器人与安全验证北京市重点实验室(首都师范大学) 北京100048 电子系统可靠性技术北京市重点实验室(首都师范大学) 北京100048 高可靠嵌入式系统北京市工程研究中心(首都师范大学) 北京100048

为应对更为复杂的任务需求,现代机器人产业发展愈发迅猛.出于协调工作的灵活性、柔顺性以及智能性等多项考虑因素,多臂/多机器人充分发挥了机器人的强大作用,成为现代机器人产业的重要研究热点.在机器人双臂协调运行当中,机械臂之间以... 详细信息

为应对更为复杂的任务需求,现代机器人产业发展愈发迅猛.出于协调工作的灵活性、柔顺性以及智能性等多项考虑因素,多臂/多机器人充分发挥了机器人的强大作用,成为现代机器人产业的重要研究热点.在机器人双臂协调运行当中,机械臂之间以及机械臂与外部障碍物之间容易发生碰撞,可能会造成财产损失甚至人员伤亡.对机器人碰撞检测方法进行形式化验证,以球体和胶囊体形式化模型为基础,构建基本几何体单元之间最短距离和机器人碰撞的高阶逻辑模型,证明其相关属性及碰撞条件,建立机器人碰撞检测方法基础定理库,为多机系统碰撞检测算法可靠性与稳定性的验证提供技术支撑和验证框架.

关键词：机器人碰撞检测形式化方法定理证明 HOL-Light

来源：评论

学校读者我要写书评

暂无评论

软硬件协同设计的SEU故障注入技术研究

引用

电子学报 2018年第10期46卷 2534-2538页

作者：王晶荣金叶周继芹于航申娇张伟功首都师范大学信息工程学院北京100048 北京微电子技术研究所北京100076 首都师范大学电子系统可靠性技术北京市重点实验室北京100048

针对现有容错计算机故障注入方法缺乏对空间环境中频发的单粒子故障模型的支持,本文提出了一种利用背板技术的软硬件协同仿真与故障注入技术,分别针对寄存器部件和存储器部件的特性,设计了多位错误的单粒子故障模型,在寄存器传输级实现... 详细信息

针对现有容错计算机故障注入方法缺乏对空间环境中频发的单粒子故障模型的支持,本文提出了一种利用背板技术的软硬件协同仿真与故障注入技术,分别针对寄存器部件和存储器部件的特性,设计了多位错误的单粒子故障模型,在寄存器传输级实现了通过软件生成故障并注入到硬件设计中的软硬件协同故障注入方案,避免了在硬件设计中修改代码生成故障破坏系统完整性的问题.基于Leon2内核的故障注入实验表明,本文设计的平台为处理器容错设计提供了一个自动化、非侵入、低开销的故障注入和可靠性评估方案.

关键词：容错故障注入软硬件协同单粒子翻转微处理器寄存器传输级

来源：评论

学校读者我要写书评

暂无评论

基于精化的可信执行环境内存隔离机制验证

引用

软件学报 2022年第6期33卷 2189-2207页

作者：靳翠珍张倩颖马雨薇李希萌王国辉施智平关永首都师范大学信息工程学院北京100048 高可靠嵌入式系统北京市工程研究中心(首都师范大学) 北京100048 计算机体系结构国家重点实验室(中国科学院计算技术研究所) 北京100190 电子系统可靠性技术北京市重点实验室(首都师范大学) 北京100048 电子系统可靠性与数理交叉学科国家国际科技合作示范型基地(首都师范大学) 北京100048

可信执行环境(trusted execution environment,TEE)基于硬件隔离机制,为安全敏感应用提供隔离的执行环境,保护敏感数据的安全性.内存隔离机制是TEE的关键机制之一,用于对安全内存和非安全内存进行隔离,并对安全内存实施访问控制,如果其... 详细信息

可信执行环境(trusted execution environment,TEE)基于硬件隔离机制,为安全敏感应用提供隔离的执行环境,保护敏感数据的安全性.内存隔离机制是TEE的关键机制之一,用于对安全内存和非安全内存进行隔离,并对安全内存实施访问控制,如果其安全性不能保证,可能造成存储在安全内存中的敏感数据泄露.为验证TEE内存隔离机制的安全性,针对基于ARM TrustZone技术构建的TEE,提出一种基于精化的可信执行环境内存隔离机制安全性验证方法.建立抽象模型和具体模型,并定义两种模型之间的精化关系,在证明精化关系成立和抽象模型满足信息流安全性的前提下,验证具体模型的信息流安全性.具体模型建模了TEE内存隔离机制的关键硬件和软件,包括TrustZone地址空间控制器、MMU和TrustZone monitor等,在定理证明器Isabelle/HOL中,验证了该模型满足无干扰、无泄露、无影响等信息流安全属性.

关键词： TEE 内存隔离机制形式化验证精化关系信息流安全性

来源：评论

学校读者我要写书评

暂无评论

实时嵌入式双操作系统架构研究综述

引用

电子学报 2018年第11期46卷 2787-2796页

作者：张美玉张倩颖孟子琪施智平关永首都师范大学信息工程学院北京100048 成像技术北京市高精尖创新中心北京100048 轻型工业机器人与安全验证北京市重点实验室北京100048 电子系统可靠性技术北京市重点实验室北京100048

随着全球工业4. 0战略的提出,工业控制及航空航天等领域对嵌入式系统的要求越来越高,对实时性具有严格要求同时还需要应用功能丰富的通用操作系统的支持.针对该需求现状,学术界和产业界提出双操作系统的解决思路,即同时运行实时操作系... 详细信息

随着全球工业4. 0战略的提出,工业控制及航空航天等领域对嵌入式系统的要求越来越高,对实时性具有严格要求同时还需要应用功能丰富的通用操作系统的支持.针对该需求现状,学术界和产业界提出双操作系统的解决思路,即同时运行实时操作系统和通用操作系统.本文归纳总结国内外嵌入式双操作系统的研究现状,对各种实现技术进行深入探讨和分析,列举嵌入式双操作系统典型应用和主要应用领域,最后对该类技术的研究趋势进行总结.

关键词：双操作系统嵌入式操作系统实时性虚拟化双核

来源：评论

学校读者我要写书评

暂无评论

微内核操作系统互斥量模块功能正确性的形式化验证

引用

软件学报 2024年第9期35卷 4179-4192页

作者：张林雁李希萌施智平关永曹钦翔张倩颖首都师范大学信息工程学院北京100048 电子系统可靠性技术北京市重点实验室(首都师范大学) 北京100048 北京成像理论与技术高精尖创新中心(首都师范大学) 北京100048 上海交通大学约翰霍普克罗夫特计算机科学中心上海200030

操作系统在许多安全攸关领域为软件系统提供关键性底层支撑,操作系统中一个微小的错误或漏洞都可能引起整个软件系统的重大故障,造成巨大经济损失或危及人身安全.为了减少此类安全事故的发生,对操作系统正确性进行验证十分必要.传统测... 详细信息

操作系统在许多安全攸关领域为软件系统提供关键性底层支撑,操作系统中一个微小的错误或漏洞都可能引起整个软件系统的重大故障,造成巨大经济损失或危及人身安全.为了减少此类安全事故的发生,对操作系统正确性进行验证十分必要.传统测试手段无法穷尽系统中的所有潜在错误,因而操作系统验证有必要使用具有严格数学理论基础的形式化方法.在操作系统中,互斥量可协调多任务对资源的访问,是一种常用的任务同步方式,其功能正确性对于保障多任务应用的正确性十分关键.基于定理证明方法,在交互式定理证明器Coq中对某抢占式微内核操作系统的互斥量模块进行代码级形式化建模,给出其接口函数的形式化规范,并实现这些接口函数的功能正确性验证.

关键词：互斥量功能正确性形式化验证定理证明 Coq定理证明器

来源：评论

学校读者我要写书评

暂无评论

基于周期粒度的级间寄存器备份机制

引用

电子学报 2018年第10期46卷 2486-2494页

作者：王晶申娇丁利华杨星邱柯妮张伟功首都师范大学信息工程学院北京100048 中国科学院计算技术研究所计算机体系结构国家重点实验室北京100190 首都师范大学电子系统可靠性技术北京市重点实验室北京100048

单粒子翻转是空间环境下微处理器发生异常的重要诱因之一,随着集成电路特征尺寸的缩小,单粒子翻转不仅会引发单位错误,还会引发大量的多位错误,如何有效解决处理器所面临的多位故障是容错处理器设计面临的新挑战.本文提出了一种基于周... 详细信息

单粒子翻转是空间环境下微处理器发生异常的重要诱因之一,随着集成电路特征尺寸的缩小,单粒子翻转不仅会引发单位错误,还会引发大量的多位错误,如何有效解决处理器所面临的多位故障是容错处理器设计面临的新挑战.本文提出了一种基于周期粒度的级间寄存器备份机制的容错方法,采用双流水线冗余结构,通过比较器对比两条流水线的级间寄存器以检测单粒子故障;以周期粒度对级间寄存器的内容进行备份,当检测到单粒子故障时,使用2个周期对流水线进行恢复;为避免脏数据流出流水线,在数据缓存和寄存器堆的入口设置写缓冲,通过延迟写入保证信息可靠性.本文基于实际的SPARC V8结构处理器,对提出的方法进行了具体实现,在实验平台上进行了仿真,仿真结果显示,本文提出的容错方法能够以一定的面积开销实现对SEU、SET、和MBU故障容错,加固处理器的主频最高可以提升70%.

关键词：单粒子翻转多位故障容错备份写缓冲流水线加固

来源：评论

学校读者我要写书评

暂无评论

面向ROS的差分模糊测试方法

引用

软件学报 2021年第6期32卷 1867-1881页

作者：王颖王冰青关永李晓娟王瑞首都师范大学信息工程学院北京100048 轻型工业机器人与安全验证北京市重点实验室(首都师范大学) 北京100048 电子系统可靠性与数理交叉学科国家国际科技合作示范型基地(首都师范大学) 北京100048

机器人操作系统(robot operating system,简称ROS)是一种广泛应用于机器人开发的开源系统,它可以为开发者提供硬件抽象、设备驱动、库函数、可视化、消息传递和软件包管理等诸多功能,应用前景广阔.ROS集成了可以实现不同功能的功能包,... 详细信息

机器人操作系统(robot operating system,简称ROS)是一种广泛应用于机器人开发的开源系统,它可以为开发者提供硬件抽象、设备驱动、库函数、可视化、消息传递和软件包管理等诸多功能,应用前景广阔.ROS集成了可以实现不同功能的功能包,例如定位绘图、行动规划、感知、模拟等等,但其中可能存在一些漏洞,破坏整个机器人系统的安全性和可靠性.提出了一种差分模糊测试方法对ROS不同版本的功能包进行测试,找出其中的漏洞.该方法包括测试用例生成和差分模糊测试执行两个模块:首先,对于输入文件进行加载、处理,并基于策略生成的方法生成测试用例文件;其次,节点间使用话题通信机制实现通信,使用上一模块生成的测试用例文件作为统一的模糊输入,对ROS不同版本的功能包进行差分模糊测试;接着,对测试结果中的不一致输出进行差异计算并评估,符合评估指标的种子将被保留并反馈给用例生成模块循环生成测试用例,有效提高了种子质量及代码覆盖率;最后分析不一致输出原因,找出漏洞.将该方法应用在机器人坐标转换的实验中,实现对不同参考系下坐标转换的功能包TF和TF2的测试.最终的实验结果表明:与TF2相比,TF在功能实现上更加准确.TF2实现坐标旋转变换的函数存在漏洞.

关键词：差分模糊测试机器人操作系统功能包漏洞检测可靠性

来源：评论

学校读者我要写书评

暂无评论

自适应双路间隔调控跟踪算法

引用

计算机应用与软件 2023年第1期40卷 173-183页

作者：蒋秋萍付小雁首都师范大学信息工程学院北京100048 电子系统可靠性技术北京市重点实验室北京100048

卷积特征可有效解决复杂场景下的跟踪漂移问题,但特征提取耗时较长;传统手工算法跟踪速度快,然而精度有待提高。基于此,提出自适应双路间隔调控算法。针对目标尺度变化问题,使用多尺度特征训练跟踪器并依据质量评估自适应融合结果,为减... 详细信息

卷积特征可有效解决复杂场景下的跟踪漂移问题,但特征提取耗时较长;传统手工算法跟踪速度快,然而精度有待提高。基于此,提出自适应双路间隔调控算法。针对目标尺度变化问题,使用多尺度特征训练跟踪器并依据质量评估自适应融合结果,为减少计算开销采用主成分分析降维;算法实时评估目标运动状态,在手工主线算法基础上间隔性地调用深度算法,在保证跟踪精度的同时尽可能地减少时间消耗。实验表明该算法实现了特征优势互补,精度可达0.91,GPU速度17.5 FPS。

关键词：相关滤波多尺度质量评估深度卷积特征双路间隔调控策略

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：