随着科学技术及汽车工业的快速发展,围绕汽车电子开展的研究越来越多。为了实现汽车上各种复杂的电子设备之间信息的快速、安全传输,人们研究出诸如CAN、TTCAN、LIN、FlexRay等汽车内部网络通讯协议。而汽车开放系统架构AUTOSAR (AUTomotive Open System ARchitecture)的提出则为高效管理愈来愈复杂的汽车电子、网络系统提供一个基础。本文对TTCAN协议及AUTOSAR规范进行分析,并运用形式化方法对TTCAN协议及基于AUTOSAR的TTCAN协议建模,然后根据规范对模型关键性质进行验证。对于TTCAN协议,分别从系统矩阵、节点消息传输、总线仲裁和错误处理四个主要方面进行形式化描述,建立四个模块以及模块之间消息通信的详细模型。对基于AUTOSAR的TTCAN协议则主要在TTCAN协议模型的基础上,根据规范将TTCAN协议模型迁移到AUTOSAR,建立包含软件组件、运行时环境和基础软件三个层次的模型。其中,软件组件实现TTCAN协议模型中系统矩阵的功能,为系统提供消息传输请求的列表；运行时环境为上下层之间的通信提供了虚拟总线的功能,包含了多种接口以供上层模块调用底层通信服务,是对TTCAN协议模型通信通道的抽象；基础软件包含TTCAN协议模型中的节点消息传输、总线仲裁和错误处理模块。模型的建立以Timed CSP为基础,并利用工具PAT实现。同时根据TTCAN协议及AUTOSAR规范的相关需求,提取了包括无死锁性、安全性、不变性及公平性在内的四种类型的性质。提取的性质由LTL公式及断言描述,并在模型验证工具PAT中进行了验证。通过形式化方法对TTCAN协议及基于AUTOSAR的TTCAN协议进行建模与验证,对提高TTCAN协议安全性与实时性有一定的促进作用。同时,建立基于AUTOSAR的TTCAN协议模型可以增强对汽车电子系统架构的理解,为以后分析其它汽车内部网络通讯协议,基于模型开发等研究工作打下基础。