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

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

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

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

基于注意力机制的多分支LSTM心理负荷评估模型

充分获取脑电信号的有效特征已成为心理负荷评估亟待解决的问题.提出一种多分支LSTM和注意力机制相结合的多分类网络框架.首先,此网络在对脑电信号做切片处理后,采用多分支LSTM网络提取切片中的时间特征;然后,利用注意力机制对所提取的时间特征进行权重参数优化;最后,通过softmax层输出心理负荷评估结果.通过消融实验和对比实验对模型进行验证.结果 表明,此网络无论在二分类任务还是多分类任务中的表现均优于现有先进网络.     

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

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

摄动开普勒问题形式化建模与验证

摄动开普勒问题广泛应用于卫星轨道摄动分析,然而卫星轨道摄动分析数学模型的错误将导致灾难性后果.传统的建模与分析方法涉及到矢量代数、旋量代数、复数、四元数等多种不同的代数系统,在各个代数系统相互转换过程中极易引入错误.几何代数方法将多种代数系统统一到相同代数结构中,弥补了传统分析方法的不足.但是基于几何代数的摄动开普勒问题数学模型的正确性并没有通过严格的形式化验证.本文采用高阶逻辑来描述该问题的属性和规范,以公认的逻辑公理和推理规则为基础构建其形式化模型并进行验证,从而最大程度确保数学模型的正确性和分析方法的可靠性.     

具有多层次优化能力的EEG生成模型

基于生成对抗网络(generative adversarial networks, GAN)的脑电信号(electroencephalogram, EEG)生成技术存在生成样本特征单一、幅值差异过大以及拟合速度慢等问题, 其质量难以满足深度学习模型训练和优化的要求. 因此, 本文通过对WGAN-GP的优化, 使其更适应脑电信号生成, 从而解决以上问题. 具体而言: (1)在WGAN-GP网络的框架的基础上, 通过将长短期记忆网络(long short-term memory, LSTM)代替卷积神经网络(convolutional neural networks, CNN), 以保证时间相关特征的完整性, 从而解决脑电生成特征单一的问题; (2)将标准化处理后的真实脑电信号输入至判别器, 以解决幅值差异过大问题; (3)将脑电噪声部分作为先验知识输入至网络生成器, 以提高生成模型的拟合速度. 本文分别通过sliced Wasserstein distance (SWD)、mode score (MS) 以及EEGNet对生成模型做多层次定量评估. 与目前已有生成网络WGAN-GP相比较, 基于本模型的生成数据更为接近真实数据.     

面向实时数据的CPS一体化建模方法

信息物理系统（cyber-physical system，简称CPS）是一个在环境感知的基础上整合了物理和计算元素的系统，它可以智能地响应真实世界的动态变化，具有重要而广阔的应用前景.然而，CPS工作在复杂的物理环境中，周围的物理变化会对CPS的行为产生影响.因此，确保CPS在复杂环境中的安全性和可靠性至关重要.提出了一种面向实时数据的一体化建模方法，通过定义一系列的规则，将领域环境模型组合到运行时验证过程中去，从而保证CPS在不确定环境中的安全性和可靠性.该方法首先为环境建立数学模型.然后，设计合并规则将相同系统参数下仅有一个环境影响因子的数学模型合并为相同系统参数下有一个或多个环境影响因子的数学模型.之后，定义转换规则，将数学模型转换为伪代码表示的环境模型.最后，根据组合规则将环境模型组合到运行时监视模型中执行验证.该方法使得监视模型更加完整、准确，当环境发生变化时，通过动态调整参数范围使得CPS中的安全属性在复杂的物理环境中仍然得以满足.将该方法应用到移动机器人避障实验中，对影响电池容量的温度和湿度进行数学建模，然后将环境模型组合到监视模型中去，最终实现在执行任务前可以根据不同的物理环境准确地给出续航时间安全提醒.     

具有多传感器的CPS系统的攻击检测

信息物理系统（cyber-physical systems，简称CPS）是基于环境感知实现计算、通信与物理元素紧密结合的下一代智能系统，广泛应用于安全攸关的系统和工业控制等领域.信息技术与物理世界的相互作用使得CPS容易受到各种恶意攻击，从而破坏其安全性.主要研究存在瞬态故障的CPS中传感器的攻击检测问题.考虑具有多个传感器测量相同物理变量的系统，其中一些传感器可能受到恶意攻击并提供错误的测量.此外，使用抽象传感器模型，每个传感器为控制器提供一个真实值的可能间隔.已有的用于检测传感器被恶意攻击的方法是保守的.当专业攻击者在一段时间内轻微地或不频繁地操纵传感器的输出时，现有方法很难捕获到攻击，如隐身攻击.为了解决这个问题，设计了一种基于融合间隔和历史测量的传感器攻击检测方法.该方法首先为不同的传感器构建不同的故障模型，使用系统动力学方程把历史测量融入到攻击检测方法中，从不同的方面分析传感器的测量.另外，利用历史测量和融合间隔解决了两个传感器的测量相交时是否存在故障的问题.该方法的核心思想是利用传感器之间的成对不一致关系检测和识别攻击.从EV3地面车辆上获得真实的测量数据来验证算法的性能.实验结果表明，所提出的方法优于现有方法，对各种攻击类型都有较好的检测和识别性能，特别是对于隐身攻击，检测率和识别率大约提高了90%以上.