Formal Modelling and Verification of the Clock Synchronization Algorithm of FlexRay

Defence science journal

article

Shimmi Asokan¹  K.H. Kochaleema¹  G. Santhosh Kumar² 

[1] DRDO- Naval Physical and Oceanographic Laboratory;Department of Computer Science, Cochin University of Science & Technology

关键词: Formal verification;    FlexRay;    Model checking;    UPPAAL;    Clock synchronisation;   

DOI  :  10.14429/dsj.73.18449

学科分类：社会科学、人文和艺术（综合）

来源: Defence Scientific Information & Documentation Centre

【 摘 要 】

The hundreds of electronic control devices used in an automotive system can effectively communicate with one another, thanks to an in-vehicle network (IVN) like FlexRay. Even though every node in the network will be running on its local clock, a global notion of time is essential. The clock synchronisation algorithm accomplishes this global time between the nodes in FlexRay. In this era of self-driving cars, the vehicle’s safety is paramount. For the vehicle to operate safely and smoothly, timely communication of information is critical, and the clock synchronisation algorithm plays a vital role in this. It is essential to formally test the clock synchronisation algorithm’s correctness. This paper attempts to model and verify the clock synchronisation algorithm of FlexRay using formal methods, which in turn enhance the reliability of safety-critical automotive systems. The clock synchronisation is modelled as a network of six timed automata in the UPPAAL model checker. Three system models were developed, a model for an ideal clock, another for a drifting clock, and a third model considering propagation delay. The precision of the clocks is verified to be within the prescribed limits. Simulation studies are also conducted on the model to ensure that the clock’s drift is always within the precision.

【 授权许可】

All Rights reserved