Formal Verification of Twin Clutch Gear Control

Twin clutch model enables the power-shifts as conventional planetary automatic transmission and eradicates the disadvantages of single clutch transmission. The automatic control of the dual clutches is a synchronization problem. Particularly, to control the clutching component that engages torque when running in one direction of revolution and disengages when running in the other direction, which exchange the torque smoothly during torque phase of the gear-shifts on planetary-type automatic transmissions, seemed for quite a while hard to compensate through clutch control. Another problem is to skip gears during multiple gearshifts. However, the twin clutch gear control described in ["M Goetz, M C Levesley and D A Crolla. Dynamics and control of gearshifts on twin clutch transmissions, Proceedings of the Institution of Mechanical Engineers, Journal of Automobile Engineering 2005"], a significant improvement in twin clutch gear control system is discussed. We formally specify the algorithm for the twin clutch gear control system and verify it using the model-checking. Formal methods have a high potential to measure correctness of communicating protocols. We use UPPAAL for formal specification and verification. Our results show that the twin clutch gear control model partially fulfills its functional requirements