| With the rapid development of science&technology and automobile industry, more and more research work on automotive electronics have been carried out. In order to achieve rapid and safe transmission of messages between all sorts of complicated electronic equipment within a car, people proposed automotive internal network communication protocol such as CAN, TTCAN, LIN and FlexRay protocol. And AUTOSAR (AUTomotive Open System ARchitecture) is proposed to provide a basis for efficient management of automotive electronics and network system which become more and more complicated.In this paper, TTCAN protocol and AUTOSAR specification are analyzed. Formal methods are used for modeling TTCAN protocol and AUTOSAR-based TTCAN protocol, and then the critical properties of the models are extracted and validated. For TTCAN protocol, This paper not only completes the modeling on the four main modules:system matrix, node message transmission, bus arbitration, and error handling, but also gives a detailed model which describes the communications among these four modules and communications inside these modules. For AUTOSAR-based TTCAN protocol, this paper mainly analyzes the message transmission mode, establishes a three layers’model which contains software component, runtime environment, basic software on the basis of the previous model. Software component provides a sequence of message request for the system. Runtime environment provides virtual function bus for the communication between the upper and lower layers, contains a variety of interfaces for upper module calling the underlying communication service. Basic software includes modules of node message transmission, bus arbitration and error handling which in previous model.Models are established on the basis of Timed CSP, and implemented by tool PAT. At the same time, according to the requirements from TTCAN protocol and AUTOSAR specification, four kinds of properties including deadlock, safety, invariance and fairness are extracted. Properties are described by LTL formulas and assertions, which are verified in the PAT.Modeling and verification of TTCAN protocol and AUTOSAR-based TTCAN protocol by formal methods will improve TTCAN protocol’s safety and correct. Meanwhile, the establishment of AUTOSAR-based TTCAN protocol can enhance the understanding of automotive electronics system architecture, lay the foundation for future analysis on automotive’interior network communication protocols, and model-based development. |