摘要：高速串行现场总线(controller area network,简称CAN)被广泛部署到机器人通信系统中.而服务机器人任务具有并发性和高实时性的特点,因此,如何根据总线协议规范和应用需求精化设计模型,保证系统设计的正确性和实时性要求,避免设计阶段的漏洞十分必要.针对传统方法的局限性,提出使用形式化方法对基于CAN现场总线型控制系统进行建模分析.首先,对系统进行模型抽象和形式表达;其次进行形式建模和自动验证,在UPPAAL中实现主控制器、关节控制器、收发器、仲裁器和CAN总线的时间自动机模型;最后对机器人通信系统进行正确性验证和实时性分析.实时性分析发现:随着总线上关节节点数的增多,低优先级节点的最坏仲裁时延的增长速率加大.针对这个问题,在形式模型中加入了改进的动态优先级策略.实验结果表明:部署动态优先级策略后不仅减小了低优先级节点的仲裁时延,而且还可以加大CAN总线的节点负载量,为系统设计提供有效的指导和参考.

摘要：机器人操作系统(robot operating system,简称ROS)是一种开源的元操作系统,能够在异种计算簇上提供基于消息机制的结构化通信层.为改善ROS1中存在的数据分发实时性、可靠性问题,ROS2提出了面向数据流的数据分发服务机制.采用概率模型检验的方法,分析、验证ROS2系统数据分发机制的实时性和可靠性.首先,提出一种面向数据流的ROS2数据分发服务的形式化验证框架,并对通信系统模块建立概率时间自动机模型;其次,运用概率模型检测器,通过数据丢失率和系统响应时间等参数分析、验证ROS2面向数据流的数据分发服务的实时性、可靠性;最后,基于重传机制、服务质量(quality of service,简称QoS)策略分析,通过设置和调整服务质量参数,实现不同的数据需求和传输方式的量化性能分析,为ROS2应用的设计人员以及基于数据流的分布式数据分发服务的形式化建模、验证和量化性能分析提供参考.

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

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

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

摘要：针对位于视野两侧的车道线易受光照等影响变得模糊而难以检测的问题,本文利用外形细长的车道线具有较强的空间信息的先验知识,设计了一个基于空间特征编码的端到端多任务网络LDNet-SFE.通过将特征图的每一行视作新的卷积层,把逐层卷积操作的原理应用到逐行卷积中,从而提取丰富空间信息,使网络更好地捕获车道线的空间连续性的特征.我们在公开数据集Cordova1和Washington1下进行实验,LDNet-SFE的F1分数分别达到了0.877和0.866,性能优于现有方法.

摘要：机器人的形式化验证方法通常很复杂,目前还没有一种通用的方法。本文对机器人的形式化设计和验证的概念进行介绍,描述其框架和基本方法。调查多个设计和验证项目,阐述项目的验证目标、方法、优缺点和进展情况。在总结研究现状的基础上,分析和展望机器人形式化设计和验证的发展趋势,从机器人模型设计、验证工具、代码实现等方面给出形式化设计和验证的思路。

摘要：混成系统是实时嵌入式系统的重要子类,其行为中存在连续变化和离散跳转混杂的情况,使得混成系统行为复杂,安全性难以掌握。近年来,混成系统在医疗环境中得到越来越广泛的应用。其中,医疗机器人的穿刺运动控制系统呈现高度复杂的混成性,如果机器人在穿刺过程中失控将导致不可挽回的严重后果。因此穿刺机器人运动行为的安全性设计成为了亟需解决的问题。首先根据穿刺机器人的运动学设计,将机器人的复杂运动分解。然后基于微分动态逻辑理论从混成系统的角度出发对穿刺机器人的运动控制系统进行了形式化建模与分析,并使用证明工具KeYmaera归纳出微分不变式,获得了控制模型的参数约束。最后提出了针对机器人运动到某一靶目标区域这类运动学问题的一般性验证模型。

摘要：目前,大部分机器人通过在线编程的方式来完成预先设定的功能,但是智能化水平相对有限,无法主动学习新的任务和应对新的环境.设计一个基于语音交互和神经网络的机器人自主学习系统,一方面系统根据任务需求,利用Kinect深度传感器采集目标的颜色和深度信息进行目标的检测和特征提取,通过语音识别自动生成神经网络模型的训练样本,用于训练和更新神经网络模型;另一方面基于神经网络模型识别目标,通过自然的语音交互方式控制机器人的运动.通过仿真和真实机器人实验验证了自动训练未知事物模型的机器人学习系统的可行性,其中还对机械臂进行了坐标校正和轨迹规划,这样无论是在笛卡尔空间还是在关节空间内,机械臂都能平滑稳定地运动,保证了路径的平滑和工作的安全性.实验结果表明,基于本文设计的自主学习系统可以快速学习和完成新的任务,具有很好的扩展性,适用于不同的任务需求的应用场景.

摘要：目前,Google和Willow Garage已经为Android系统构建ROS(Robot Operating System)环境提供了基于rosjava的应用功能包集合android_core,便于Android移动终端和ROS进行互联互通。然而,当前的通信机制不能保证Android应用对基于ROS的机器人进行可靠的远程控制。为解决上述问题,从ROS中的应用层和通信机制两方面对ROS进行完善。一是在ROS端TCP/IP协议的应用层设计通信异常检测模块"Check Node Connection"来进行Android移动终端的连接状态检测;二是在Android端设计与ROS中"ROS Action Protocol"相匹配的通信机制"Ros Action On Android"。实验结果表明,设计的通信异常检测模块"Check Node Connection"可以高效地检测Android与ROS间的连接状态。此外,"Ros Action On Android"通信机制可时刻获取ROS机器人在任务执行中的状态反馈信息并支持任务抢占,使得交互控制更加精准可靠。