Model checking of in-vehicle networking systems with CAN and FlexRay
Model checking of in-vehicle networking systems with CAN and FlexRay
复制标题
使用 CAN 和 FlexRay 进行车载网络系统的模型检查
DOI：
10.1016/j.jss.2019.110461
复制
发表时间：
2020
影响因子：
3.5
通讯作者：
Lin Hsin-Hung
中科院分区：
文献类型：
--
作者：
Guo Xiaoyun;Aoki Toshiaki;Lin Hsin-Hung
车载网络（IVN）系统由通过总线连接的电子组件组成，并根据需要通过多种协议进行通信。在实践中，智能车辆需要在使用各种协议的子系统之间交换数据，例如控制器局域网（CAN）和FlexRay。此类系统在传输过程中更容易遇到延迟和消息丢失，从而带来严重的安全问题。此外，IVN系统由于节点数量多、通信协议多种、拓扑结构多样而极其复杂。因此，很难直接、准确地检查系统的定时特性。在本文中，我们提出了在设计阶段利用 CAN 和 FlexRay 建模 IVN 系统的适当抽象。使用 UPPAAL 平台分析通信的定时属性。由于IVN系统结构众多，因此开发了一个框架来构建IVN系统设计的模型。该模型是为了验证不同协议之间消息的传输。我们评估了该框架的有效性、适用性和可重用性，并展示了该框架在验证 IVN 系统模型方面的性能。
An in-vehicle networking (IVN) system consists of electronic components that are connected by buses and communicate through multiple protocols according to their requirements. In practice, intelligent vehicles need to exchange data between subsystems that use various protocols, such as the controller area network (CAN) and FlexRay. Such systems are more likely to encounter delays and message loss during transmission, presenting serious safety issues. Moreover, IVN systems are extremely complicated because of their large number of nodes, multiple communication protocols, and diverse topologies. As a result, it is difficult to check the timed properties of the system directly and accurately. In this paper, we present an appropriate abstraction for modeling IVN systems that utilize CAN and FlexRay during the design phase. The timed properties of communication are analyzed using the UPPAAL platform. As there are numerous IVN system structures, a framework is developed to build a model for an IVN system design. The model is to verify the transmission of messages between different protocols. We evaluate the validity, applicability, and reusability of the framework and show the performance of the framework for verifying IVN system models.