FlexRay通信协议的模型检查

摘要

目前,车载系统主要采用电子控制单元(ECUs)来实现X-by-wire技术。通过X-by-wire技术,使不能机械地被实现的功能或需求变为可能。一般来说,在一个汽车系统中的ECU按照通信协议相互通信,通过一个或多个总线。由于通信协议极大地影响汽车系统的性能,协议能够支持高传输速率和可靠性的要求。最近,FlexRay通信协议被视为实际标准的汽车通信协议。FlexRay通信协议支持高传输速率可达10Mbs,同时仍保持可靠性和容错性。这些特性使FlexRay特别适用于安全关键系统。另一方面,汽车系统的测试过程既费时又复杂的。在工业领域,应准备实现通信协议的设备需测试应用程序在ECUs上执行,连接ECUs和协议控制设备,形成一个测试环境。从以前的测试的数据支持进行测试,专注于特定的节点或数据传输。由于更高的要求,导致复杂的功能,因此需要更多的ECU,并且测试过程中伴随着大量的设备和高财务成本使测试变得更加困难。
　　本文提出了一个框架验证FlexRay车载系统的设计模型。该框架基于UPPAAL,它是一个时间自动机模型检查器为时间相关的行为建模。通过该框架验证设计模型,在设计阶段开发人员用模型检验技术可以更好的机会发现缺陷。这样做可以减少系统的开发的成本,同时提高应用程序的质量。类似于设备为基础的测试,UPPAAL框架由一个FlexRay模型和应用模型组成。前者代表的FlexRay设备,后者代表的ECU执行的应用程序。UPPAAL只提供了应用通道的同步方法,因此FlexRay模型和应用模型必须进行特殊处理。基于FlexRay规格书,对其进行三步抽象最终建立FlexRay模型。FlexRay模型还提供了通信和访问应用模型之间的参数和接口。应用模型只需要按照这些参数和接口,与FlexRay模型合作为车载系统的设计模型。为了评估框架,进行了如下实验:(1)应用模型基本行为的测试是为了检查FlexRay模型的有效性,(2)建立一个简单的应用验证系统的响应时间,通过使用观测器模型进行测试(3)介绍了简化的自适应巡航控制系统,为了显示了可行性通过框架验证实际应用。实验结果分别证明了FlexRay模型的有效性和框架的可行性。特别地检查了时间特性和获得了根据检查结果改善应用模型的经验。

目录

封面

声明

中文摘要

英文摘要

目录

第一章 Introduction

1.1 Motivation

1.2 Objective

1.3 Related Works

1.4 Overview of Proposed Approach

1.5 Structure of the Thesis

第二章 Background

2.1 Automotive System

2.2 FlexRay

2.3 Model Checking

2.4 Timed Automaton

2.5 UPPAAL

第三章 Construction of FlexRay Model

3.1 Overview of FlexRay Communication Protocol Specification

3.2 Abstracted FleRay Model

3.3 FlexRay Model

第四章 Model Checking Applications with FlexRay Model

4.1 Model Checking Applications with FlexRay Model Process

4.2 Interface of FlexRay Model

4.3 An Example of Communication System with FlexRay Model

第五章 Experiments

5.1 A Testing Example

5.2 Response Time Checking with FlexRay Model

5.3 Adaptive Cruise Control Subsystem

第六章 Conclusion

6.1 Summary

6.2 Future Work

参考文献

致谢