基于深度残差学习的自动驾驶道路场景理解

随着道路场景理解技术的快速发展，自主驾驶领域取得了长足的进步。在相关任务中，包括道路分割、分类和车辆检测的实时性和准确性是安全性的一个关键问题。为此，提出了一个具有编/解码器网络结构的基于深度残差学习的方法。一方面，编码器网络结构使用不同层次的残差网络来提取高维中的抽象特征，这些特征在接下来的三个任务中共享使用；另一方面，解码器网络结构采用一种子任务的并行计算机制，即道路分割、车辆检测和道路分类任务同时执行。此外，全卷积神经网络用于对提取的图像特征进行上采样以解决道路分割问题。最终，实验结果表明在保证高精度的前提下处理帧率可达到15 fps以上。     

用LTL模型检验的方法验证SpaceWire检错机制

SpaceWire是应用于航空航天领域的高速通信总线协议,对SpaceWire设计正确性与可靠性要求极高,由于传统的验证方法,存在不完备性等缺陷,对SpaceWire的严格验证一直是备受关注的问题之一。模型检验以其验证的完备性得到设计人员的重视。提出用线性时态逻辑（LTL）模型检验的方法验证SpaceWire系统的检错机制。在检错模块中,该方法与用分支时态逻辑（CTL）验证方法相比,BDD分配数和状态数明显减少,提高了验证效率,还验证了错误优先级;对检错模块处理的五种错误的发生进行验证,验证结果均为正确。该方法实现了对检错机制的完备性验证。     

基于语义学习的图像多模态检索

针对语义鸿沟问题,在语义学习的基础上设计图像的多模态检索系统。该系统结合3种查询方式进行图像检索。基于视觉特征的查询通过特征提取与相似度匹配进行排位。基于标签的查询建立在图像自动标注的基础上,但在语义空间之外的泛化能力较差。基于语义图例的查询能够在很大程度上克服这个缺陷,通过在显式或隐式的语义空间上进行查询,使检索结果更符合人类感知。实验结果表明,与基于纹理特征的图像检索相比,基于语义图例的检索具有更高的精度及召回率。     

城市应急联动系统GEIS

GEIS（Grid Based Emergency Inter-Act System）是一个基于主体网格的城市应急联动与社会综合服务系统，通过主体网格和通信系统将治安、消防、卫生急救、交通、公共设施，自然灾害等突发事件的应急联动与综合服务，调度集成在一个管理平台中，通过共享指挥平台和基础信息，实现统一接处警，统一指挥，联合行动，快速反应，为市民提供更加便捷的紧急救援及相关服务，为政府科学决策和处置各种紧急与灾害事件提供技术支持为城市公共安全提供技术保障。GEIS的一个突出优势是将范例推理（Case Base Reasoning,CBR）与规则推理（Rule Base Reasoning,RBR）两种人工智能技术相结合，实现了快速预案支持，为科学决策打下良好基础，目前，GEIS已经应用到抗洪抢险和交通事故处理中，效果表明它具有跨平台性好，稳定性强，响应速度快，易操作的独特优势。     

基于小波变换和ICA的运动目标分割

提出一种时空融合的运动目标分割方法.在时域方面,采用时间轴一维小波变换提取运动对象,然后用独立成分分析法提取独立的运动对象,并基于灰度直方图进一步提取视频对象;在空域方面,提出对轮廓提取后的图像进行分水岭变换的改进方法.与COST211 AM算法比较表明,文中方法能更完整、准确地提取出运动对象.     

基于内容图像检索中的优化鉴别特征

为了提高基于内容图像检索系统的检索速度和准确率,提出一种融合两类线性鉴别分析的方法来提取低维的优化鉴别特征.首先把多类问题转换为多个两类问题,对每个两类问题进行线性鉴别分析,得到鉴别向量;所有的鉴别向量组成鉴别变换矩阵,对图像特征进行投影变换得到鉴别特征;最后用变换后的鉴别特征进行图像检索或分类,得到准确率更高的结果.该方法中鉴别特征空间的维数与类别数相等.与多种特征优化方法进行比较的实验结果表明,采用文中方法可以显著地提高图像检索和图像分类的性能.     

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

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

可信执行环境软件侧信道攻击研究综述

为保护计算设备中安全敏感程序运行环境的安全,研究人员提出了可信执行环境(TEE)技术,通过对硬件和软件进行隔离为安全敏感程序提供一个与通用计算环境隔离的安全运行环境.侧信道攻击从传统的需要昂贵设备发展到现在仅基于微体系结构状态就能通过软件方式获取机密信息的访问模式,从而进一步推测出机密信息.TEE架构仅提供隔离机制,无法抵抗这类新出现的软件侧信道攻击.深入调研了ARM TrustZone、Intel SGX和AMD SEV这3种TEE架构的软件侧信道攻击及相应防御措施,并探讨其攻击和防御机制的发展趋势.首先,介绍了ARM TrustZone、Intel SGX和AMD SEV的基本原理,并详细阐述了软件侧信道攻击的定义以及缓存侧信道攻击的分类、方法和步骤;之后从处理器指令执行的角度,提出一种TEE攻击面分类方法,利用该方法对TEE软件侧信道攻击进行分类,并阐述了软件侧信道攻击与其他攻击相结合的组合攻击;然后详细讨论TEE软件侧信道攻击的威胁模型;最后全面总结业界对TEE软件侧信道攻击的防御措施,并从攻击和防御两方面探讨TEE软件侧信道攻击未来的研究趋势.     

Ptolemy离散事件模型形式化验证方法

Ptolemy是一个广泛应用于信息物理融合系统的建模和仿真工具包,主要通过仿真的方式保证所建模型的正确性.形式化方法是保证系统正确性的重要方法之一.本文提出了一种基于形式模型转换的方法来验证离散事件模型的正确性.离散事件模型根据不同事件的时间戳触发组件,时间自动机模型能够表达这个特征,因此选用Uppaal作为验证工具.首先定义了离散事件模型的形式语义,其次设计了一组从离散事件模型到时间自动机的映射规则.然后在Ptolemy环境中实现了一个插件,可以自动将离散事件模型转换为时间自动机模型,并通过调用Uppaal验证内核完成验证.最后以一个交通信号灯控制系统为例进行了成功的转换和验证,实验结果证实了该方法能够验证Ptolemy离散事件模型的正确性.     

GJK算法的一种特殊情形的形式化验证和应用

计算几何算法经常用于机器人避碰运动规划等安全攸关领域,对这些算法进行正确性证明非常重要.用形式化方法对算法进行验证是一种十分有效的手段,尤其是定理证明的方法用严格的数学公理和定理推理证明逻辑模型的性质,对所验证的性质而言是完备的.基于GJK算法设计了计算空间两条线段间距离的算法,用定理证明器HOL4对其相关的定义和定理进行形式化定义和证明,进而基于霍尔逻辑完成形式化表示和证明,对该算法的正确性实现了形式化验证.最后,给出了这一经过验证的算法在双臂机器人无碰撞运动规划中的应用.