关键词：形式化方法;;模型检验;;Timed CSP;;TTCAN;;AUTOSAR
摘 要：随着科学技术及汽车工业的快速发展,围绕汽车电子开展的研究越来越多。为了实现汽车上各种复杂的电子设备之间信息的快速、安全传输,人们研究出诸如CAN、TTCAN、LIN、FlexRay等汽车内部网络通讯协议。而汽车开放系统架构AUTOSAR (AUTomotive Open System ARchitecture)的提出则为高效管理愈来愈复杂的汽车电子、网络系统提供一个基础。本文对TTCAN协议及AUTOSAR规范进行分析,并运用形式化方法对TTCAN协议及基于AUTOSAR的TTCAN协议建模,然后根据规范对模型关键性质进行验证。对于TTCAN协议,分别从系统矩阵、节点消息传输、总线仲裁和错误处...