智能汽车CAN总线通信系统的建模与验证

张 芮 王 瑞 楚 敏

(首都师范大学信息工程学院 北京 100048)(首都师范大学轻型工业机器人与安全验证北京市重点实验室 北京 100048)

0 引 言

智能汽车的兴起为普通汽车向无人驾驶汽车转变提供了可能性，但这个过程不是一蹴而就的，需要经历一个漫长的时期[1]。车载通信系统是智能汽车内外交互和信息传输的载体，因此保证智能车辆通信系统的安全是一个非常重要的问题。控制器局域网络总线是一种串行总线，同时支持分布式控制，是应用较为广泛的一种现场总线[2]。它包含了收发器、仲裁器和网关等模块，收发器能够保证报文接收和发送的畅通，仲裁器能够保证报文的格式和优先级的正确，而网关[3]则是针对报文传输速率的差别，对这些报文重新进行打包并且发送。这些通信总线上的关键模块保证了数据在传输过程的正确性。

本文主要对基于CAN总线的智能车辆通信系统进行分析，并对报文的传输过程中各模块建立时间自动机模型，特别加入了对通信过程中网关的建模，保证了报文能够在高速和低速时正常传输，较好地模拟车辆内部通信的过程。其次，将智能汽车在行驶过程中需要满足的属性用计算树逻辑公式进行抽象和形式化描述，运用模型检测工具对这些属性进行验证，确保车辆在遇到突发紧急的交通情况下，通信系统能够及时传递数据，车辆决策正确，辅助驾驶者做出相应操作。

1 系统描述

1.1 基于CAN总线通信的智能车辆系统

通信过程中，数据和命令的传输过程借助于汽车总线系统，汽车总线的种类是多种多样的，例如：CAN总线[4]适用于实时系统，它的优点是线束少、重量轻，可以实现丰富的车身功能；局域互联网络(Local Interconnect Network, LIN)总线可为车载通信系统提供辅助功能，它价格低、性能可靠，主要应用于车灯、外后视镜和门锁等对带宽要求较低的功能中；FlexRay可以对多重安全和舒适功能进行有效管理，适用于电子线控，是一种高速数据传递总线，但是它的成本较高；面向媒体的系统传输总线(Media Oriented System Transport, MOST)运用环形拓扑的结构，一般以光导纤维作为传导媒介，通常应用于多媒体的传输。目前，在车载通信系统中最为常见的仍然是CAN总线[5]。

智能汽车搭载的传感器种类繁多，有检测自身速度、加速度的传感器，如摄像头、红外传感器和激光雷达传感器等，它们共同组成了智能汽车的传感器系统[6]。通信过程中，报文传输的载体是CAN总线系统。它包含了收发器[7]、仲裁器[8]和网关等模块，这些通信总线上的关键模块能够保证传输过程的正确性。图1是智能车辆的通信系统[9]在工作时的过程。

图1 智能车辆的框架

1.2 CAN协议介绍

CAN总线[10]实时性强、可靠性高，同时易于开发和扩展，因此也被广泛应用在汽车[11]、轨道交通、航海船舶和导航等领域。

对CAN协议的验证一般采取传统的办法，如仿真、模拟和测试等。仿真和模拟就是运用软件系统对CAN总线运行环境进行模拟，分析通信过程并得出结论。Lindsey等[12]对CAN总线的IP抗辐射和加固进行研究；Kim等[13]使用了CANoe对重型货车通信系统进行仿真，证实了它基于CAN总线通信的可靠性。CANoe是一个具有编程功能的仿真软件，可以实时分析传递的信号，但是它过分依赖硬件设施，参数的个数也有限，致使实验结果不完备。而测试的方法一般是在设计的收尾阶段才能进行，不仅耗费大量时间，而且可复用度很低，造成很大的成本浪费。

(1) CAN总线结构。CAN总线是成麻花状缠绕的双线制结构，这样就避免了向外辐射和电磁波干扰。与总线连接的每个电子控制单元(ECU)均可传递数据，并能够选择性地读取自身所需数据。当其中一个ECU发生故障之后，不会影响其他电控单元，安全性能较好。CAN总线能够实现不同速率的传输，高速总线被用于驱动系统中，低速总线被用于车身系统中。对于速率不同的总线连接网关，需要进行“翻译”，网关通常是独立控制模块或者借用其他控制模块。CAN总线结构如图2所示。

图2 CAN总线结构

(2) CAN报文格式。 CAN协议将报文划分为数据帧、远程帧、错误帧和过载帧这4种类型，每种类型都有其固定的格式，CAN协议的帧格式分为标准和扩展两种格式，标准格式的标识符是11位，扩展格式的是29位，本文建立模型采用的是标准格式。报文中的数据全部由显性位(0)和隐性位(1)构成，显性位的优先级高，隐性位的优先级低。

(3) CAN的仲裁机制。CAN总线运用的是非破坏仲裁技术。其中，非破坏性指数据和时间都无损，借助逐位仲裁时帧的ID来实现。如果有发送任务时总线空闲，任一数据帧都能占用该总线，接收报文的单元收到数据后会向发送单元传递反馈消息，收到反馈表示任务完成，否则报文将重新发送；当两个或以上不同ID的单元同时传递数据时会产生冲突现象，此时仲裁器需要进行仲裁，也就是逐位比较报文的标识符，优先级高的报文直接发送，优先级低的报文则退回，等待总线空闲时再次发送。因此优先级最高的报文发送时间就没有损失，优先级的高低由数据包的ID决定，ID越小表明优先级越高。

2 形式化建模

形式化验证的方法近年来在众多领域中都发挥了相当的作用[14]，如建筑领域[15]和医疗领域[16]等。它包括模型检测[17]和定理证明[18]，相比之下，模型检测[19]能够对系统进行自动化证明，减少了人工干预。时间自动机理论是模型检测技术的重要基础[20]之一，为实时系统的形式化验证起到了关键的作用，其思想是运用时间自动机的形式建立目标系统的模型，搜索并遍历模型的所有状态，验证系统是否满足属性的要求。

模型检测的过程可以分为三个步骤。首先，对目标系统进行分析，从中描述出需要满足的属性，将其逻辑表达公式表示出来，如CTL公式和LTL公式等。其次，对系统进行合理的抽象并建立模型，建模过程中可以使时间自动机、Kripe结构或者转移结构。最后，用模型检测工具验证属性，若结果正确则说明建立的模型满足需求；若结果错误则会给出反例，应该通过反例检查模型找出问题，如果模型建立没有问题，则需考虑该系统是否有不满足要求的情况。

2.1 符号化模型检测工具UPPAAL

UPPAAL[21]是一个模型检测工具，它提供了对死锁的检测方法，同时运用时钟变量，可以精准地描述模型必须满足的时间方面的条件，更好地分析目标系统的实时性。现在已有的工作中，文献[22]对物理信息系统进行建模与验证，主要是对车辆系统的验证，但是没有考虑到传输速率的差别对系统产生的影响；文献[23]对智能汽车的规划策略问题进行了建模与验证。

UPPAAL[24]是由Uppsala大学和Aalborg大学提出的一个图形化的自动模型检测工具箱，可以用时钟变量来刻画连续的时间变化。本文对智能汽车通信系统中各关键模块分别建立时间自动机模型并组成时间自动机网络，以此来模拟整个通信系统，然后通过穷举搜索所有可能出现的状况，验证其属性的正确性。

UPPAAL由并发进程组成[25]，每个进程都被建立成为对应的时间自动机。每个时间自动机包含一系列节点(location)来表示它的不同状态，还有一系列变迁(transition)来表示改变状态需要的条件和参数的更新。UPPAAL可以运用带有有界整型变量的时间自动机模型网络对存在并发的实时系统展开模拟，每个进程均可通过有参数控制结构、时钟变量和进程间的通道来描述。其中，通道的作用是实现进程间的同步通信。比如，用a来表示一个通道，那么a!表示向其他进程发出了一个同步信号，a?则表示收到了一个来自其他进程的同步信号。在UPPAAL中,也可以通过共享变量实现异步通信。

UPPAAL采用巴科斯范式(BNF)语法描述目标系统的属性，该语法对CTL公式进行了简化，主要包括路径公式和状态公式，路径公式是对模型中路径或轨迹的描述，状态公式是对模型中的状态进行描述。表1给出了几种常用的路径公式。

表1 UPPAAL中的路径公式

建立的属性在模型中体现为对节点和变迁的验证。从初始节点开始，UPPAAL遍历每个节点和变迁形成路径，若能够完整遍历该路径，则路径上的节点可达，变迁上的条件也可以达到。下面以图3为例说明。

图3 UPPAAL建模验证实例

图3为一个模拟灯亮度的时间自动机网络，由User和Lamp两个时间自动机组成。User的作用是发送press!信号，也就是按下开关；Lamp的作用是接收到在不同时间间隔中收到的press?信号，改变灯光的强弱。我们假设灯处于关闭的状态，第一次按下开关时灯处于弱亮度，在5个时间单位内再次按下开关灯则变为强亮度，否则就会执行关灯操作。我们抽取的属性为：

A<> y>=5 imply Lamp.off：对于所有路径来说，两次按开关间隔超过5个时间单位则灯处于关闭状态。所经过的Lamp自动机中的其中一条路径为:

A<> y<5 imply Lamp.bright：对于所有路径来说，两次按开关间隔在5个时间单位则灯处于强亮度状态。所经过的Lamp自动机中的其中一条路径为:

2.2 通信系统模型的建立

智能车辆的通信过程可以描述为以下步骤：传感器系统将收集到的数据传给CAN总线中的收发器，等待仲裁；仲裁器对报文的每一帧数据进行逐位仲裁，判断各个报文的优先级，并根据优先级发送给收发器；网关对发送的报文进行判断是否需要变速传输，速度一致后发送给收发器；收发器接收到反馈消息之后，将报文传输到车辆的主控制器上；主控制器对报文内容分析之后再经由总线系统将命令发送给各个子控制模块；收到报文后每个子控制模块各司其职，执行相应的操作；执行完毕，每个控制单元将会给传感器系统发送反馈信息，至此一轮通信过程结束，可以开始新一轮的传输。

根据智能车辆从数据采集到处理的整个过程，关注车辆的通信过程并且忽略其他无关因素，本文对智能车载通信系统进行合理抽象。如图4所示，抽象模型分为传感器系统、主控制器、子控制器和CAN总线系统，其中CAN总线系统又可划分为总线、收发器、仲裁器和网关四部分。对上述这些部分进行形式化建模和分析，忽略了与通信系统不相关的部分，并且能够进一步明确车辆通信过程关键模块之间的作用关系，保证了模型的精确和可靠。

图4 抽象模型的框架

根据CAN总线的定义，在车辆通信系统中会有多个控制单元接入CAN总线，例如各传感器和子控制器。为了建模的精炼，本文对各个传感器和子控制器均只建立一个模型，必要时再在UPPAAL中根据模板将其实例化为多个模型。因此在传感器模型中集合了多个传感器的特征，将各传感器是否采集数据设置为布尔变量，当传感器发送数据时布尔变量更新为true，反之则为false；子控制器，也就是执行器中集合了多个执行器的特征，将各个执行器是否收到命令设置为布尔变量，当触发该执行器时，布尔变量更新为true；反之则为false。

(1) 传感器模型。传感器系统是通信过程中不可或缺的一部分，它的作用是利用不同传感器对外部事物的数据进行收集，并且对自身属性进行检测，同时传递数据给车辆的主控制器。及时地传递数据为车辆通信系统处理报文内容奠定基础。传感器系统在工作过程中有初始化状态(initial)、空闲状态(idle)、准备发送数据状态(ready_sending)、等待仲裁状态(wait_arb)、发送数据状态(sending)、结束发送数据状态(finish_sending)、准备接收反馈状态(ready_recei-ving)、接收反馈状态(receiving)、结束接收反馈状态(finish)。

首先，系统处于初始状态，每一次传输的开始都将变量begin置为1，一个通信周期开始之后，将begin置0，待到下一个周期开始再将它初始化为1。报文开始传输时，传感器系统准备发送已经接收到的数据，向收发器发出同步信号start_data!后，如果总线系统没有被占用，那么就进入准备发送的状态，此时收发器收到信号之后运用函数writing_data()对各个数据包进行写入，其中数据包包括报文ID、类型、标识符和传输速度等内容。在仲裁成功的情况下，数据包将会迁移到正在发送(sending)的状态。在发送过程中如果摄像头或者各个传感器捕捉到紧急情况，则将相应的变量置1，最后结束一个周期的传输。其次，在收到子控制器处理完成命令的同步信号interruptted?之后开始接受反馈信息，并执行各个子控制模块的工作，将相应的布尔变量更新为true，表示车辆系统对紧急情况作出了相应的反应。传感器的模型如图5所示。

图5 传感器系统的形式化模型

(2) 主控制器模型。主控制器在智能车辆的通信过程中承担了“大脑”的工作，它是连接传感器系统和车辆执行器的中间模块，既要对报文数据进行分析和处理，又要分发命令给各个子控制模块执行相应的操作，是通信系统中不可或缺的一部分。主控制器在工作过程中存在初始状态(idle)、等待仲裁状态(wait_arb)、仲裁状态(arb)、发送命令状态(sending)、结束发送状态(finish_sending)、接收反馈状态(receiving)。

收到传感器系统串的同步信号start_data?和报文之后，主控制器开始处理并发送命令给各个子控制模块，经由收发器写入命令包和仲裁器进行仲裁，接着进行数据传输，最后结束整个工作周期。主控制器的模型如图6所示。

图6 主控制器的形式化模型

(3) 子控制器模型。子控制器在通信系统中承担执行器的任务，智能车辆中各模块承担着不同的任务，上文已经分析过。收到主控制器分发的命令后，由各模块分别执行相应的操作，结束操作之后，通过CAN总线系统为传感器系统提供反馈，并且开始新一轮任务。子控制器在模型中定义了以下状态：初始状态(idle)、等待仲裁状态(waiting_arb)、等待总线空闲状态(wait_ack)、执行状态(execute)、发送反馈状态(sending)、结束发送反馈状态(finish_ack)、接收反馈状态(receiving)。其中，每个模板均可实例化为多个时间自动机模型。

子控制器在接收报文之后开始执行命令，过程中要求执行的时间不超过3个时间单位。执行过程中，要求通信系统在处理紧急情况时发出声音、灯光、视觉和视频等方面的提示，辅助驾驶员做出正确的反应。执行完毕之后向传感器系统发送反馈信息，表示可以开始下一轮传输，并且将总线的状态由忙碌变为空闲。子控制器的模型如图7所示。

图7 子控制器的形式化模型

(4) 收发器模型。收到传感器发送的数据之后，收发器首先判断CAN总线的状态，若总线处于忙碌状态，也就是data_active为0，那么报文进入等待的状态；若总线是空闲状态，也就是data_active为1，那么报文进入仲裁器进行优先级判断。如果该报文仲裁成功，则开始发送数据；如果仲裁失败，则重复上述步骤。收发器的模型如图8所示。

图8 收发器的形式化模型

(5) 仲裁器模型。数据收发器发送的同步信号readyData_arb?被仲裁器收以到后，开始进行仲裁工作，对报文的内容逐位计算，也就是比较当前数据位的值与求得的总线的值是否匹配，若不匹配就表明报文传输失败，退出仲裁，该自动机迁移到请求失败的状态；若二者匹配，但是标识符还未比较完，那么将对下一位进行仲裁；如果二者匹配且标识符都已比较完毕，则报文传输成功，仲裁工作随之完成。仲裁器的模型如图9所示。

图9 仲裁器的形式化模型

(6) 网关模型。结束仲裁之后，报文进入网关，在数据包中声明了该报文发送的速度，如果它的速度与下一个报文相同，则不需要变速；如果不同，则需要将该报文的速度进行改变，并且要求整个变速的过程不超过1个时间单位。网关的工作原理如图10所示。

图10 网关的工作过程

网关的模型如图11所示。

图11 网关的形式化模型

(7) 总线模型。CAN总线在模型中存在两个状态：空闲状态和忙碌状态，当传递报文时，需要的总线数量data_account大于0， data_active将置为1，成为忙碌状态，当发送报文之后，data_active恢复为0，总线也恢复为空闲状态。CAN总线模型如图12所示。

图12 总线的形式化模型

3 属性的形式化描述和验证

通过对智能车辆通信系工作流程和特性的分析，要求它满足的属性可分为两大类：安全性属性和功能类属性。

3.1 系统的安全性

在验证其他属性之前，首先要确保整个通信过程没有死锁的发生。

A[] not deadlock

3.2 通信系统的正确性

在报文发出之后总会收到反馈的消息，说明在这期间报文传输成功并且子控制器执行了相应的操作。

A<> (Sensor.sending imply Sensor.finish)

3.3 仲裁时间

由于Uppaal是以时间单位计时的，因此考虑到系统的实时性，要求仲裁时间不超过1个时间单位。

A<> t_darb<=1

3.4 网关判断时间

考虑到系统的实时性，要求网关变速时间不超过1个时间单位。

A<> dgw_t<=1

3.5 防抱死系统(ABS_system)

紧急刹车时车辆会触发ABS系统，此时车辆可以对制动力的大小进行控制，这样轮胎就不会被抱死，而是边滚边滑。轮胎上装有的感应速度或加速度传感器在速度值骤减或加速度绝对值为很大的负值时，即可将数据传输给主控制器，主控制器经过判断之后向ABS系统和警报系统发出命令，汽车自动触发ABS，并且提示司机当前警告。

A<> Speed_transmitter==1 imply (ABS_system==1 and sound_warning==1 and ABS_reflect==true and Sub_controller.t_execute<=3)

3.6 防碰撞预警系统(AWS_system)

危险碰撞发生之前，及时发出警报信号提醒驾驶者。在车前装有超声波等传感器，在司机精神分散或者疲劳时与前车没有保持安全距离，传感器将数据传给主控制器，再由它触发警报系统对驾驶人员进行声音和其他形式的预警。

A<> Range_sensor==1 imply (AWS_system==1 and light_warning==1 and view_warning==1 and AWS_reflect==true and Sub_controller.t_execute<=3)

3.7 夜视辅助系统(NVA_system)

车灯上装有红外摄像机，在夜晚光线情况不好的情况下帮助驾驶人员提前看到灯光照不到的地方。红外摄像机可感受前方道路的热量情况，对驾驶者进行辅助，在车内以视频的形式帮助驾驶人员对外界的情况进行观察。

A<> Infrared_camera==1 imply (NVA_system==1 and video_assist==1 and NVA_reflect==true and sub_controller.t_execute<=3)

3.8 变道辅助系统(LCA_system)

前后车门之间的车身被称为C柱，驾驶人员在驾驶位上存在C柱盲区。C柱边缘装24 GHz雷达传感器，在变道时自动监测左后方或者右后方是否有车辆靠近，若有则主控制器向子控制器发送消息，对驾驶人员发出警报提醒。

A<> Infrared_camera==1 imply (NVA_system==1 and video_assist==1 and NVA_reflect==true and sub_controller.t_execute<=3)

3.9 主动防追尾系统(ARE_system)

车尾装有超声波传感器，一旦后车没有保持安全距离，则车后灯发出警报，主动警示后车驾驶人员注意保持安全距离。

A<> Radar_sensor==1 imply (LCA_system==1 and sound_warning==1 and view_warning==1 and LCA_reflect==true and Sub_controller.t_execute<=3)

4 验证结果

4.1 验证实例

现以通信系统的正确性为例，对验证过程进行阐述：A<>(Sensor.sending imply Sensor.finish)。其含义是：对于所有的路径来说，如果到达Sensor.sending数据发送状态，那么一定会到达Sensor.finish完成处理状态。也就是说，对于每一个传输的数据都可以发送并且处理成功。运用UPPAAL中的模拟轨迹功能对模型进行随机路径的模拟。图13是在模拟轨迹中截取的初始状态、发送状态和完成状态。

图13 模型路径随机模拟过程

该属性的验证经过Sensor模型的以下路径，路径的形式化验证描述如图14所示。

图14 模型路径的形式化描述

UPPAAL可以完整地遍历该路径的每个节点和变迁，那么属性验证成功。

路径的随机模拟只是偌大模型中的其中一条路径，因此为避免状态爆炸问题，本文使用验证器对该属性进行验证，UPPAAL的验证器会枚举所有可能的状态路径进行验证，图15所示为验证结果。

图15 验证实例结果

4.2 结果分析

本文中UPPAAL软件运行的计算机环境为：3.60 GHz的八核CPU，内存环境为8.00 GB。表2为以上属性在该环境中的验证结果。其中验证总用时较短，均在秒级以下；常驻内存和虚拟内存的使用峰值也在可以接受的合理范围内。验证结果表明，基于CAN总线的智能汽车通信系统可以顺利地传输数据，对外界情况作出及时的反应，满足实时性的要求。

表2 验证结果

5 结 语

本文研究了基于CAN总线的智能汽车通信系统的形式化验证，通过对此类车辆的通信系统进行剖析和抽象，建立模型并且进行实验验证，结果表明：采用本文提供的模型检测方法能够有效地验证智能车辆通信系统的逻辑正确性和实时性。通过UPPAAL软件的验证，能够确保在车辆遇到突发状况时通信系统及时发送数据，车辆及时作出正确反应，辅助驾驶员做出相应的判断。

本文的贡献之一是对基于CAN总线的智能汽车通信系统进行安全性和实时性的验证，为现代汽车通信系统的安全验证提供了一种方法，为智能汽车过渡到无人驾驶汽车提供了硬件基础的保证；其二是对通信总线中网关进行了建模，确保差异速率下报文传输的正确性。实验结果也表明了本文模型的设计逻辑可行，验证属性的方法正确，其能够对智能汽车通信功能的正确性和实时性进行很好地验证。

本研究也存在一定的不足，比如只能通过提前定义输入的形式来定义报文内容，而不能动态地输入数据。下一步工作可能对解决动态输入传输内容的问题进行研究，同时也可以将模型检测的方法应用到其他的系统和领域中去。