关键词: 实时构件系统，时序行为，形式化方法，建模，相容性验证工具

Abstract: It can efficiently improve the system's correctness and reliability for specification and verifying of timing behavior in complex real-time components. This paper presented the timed behavior protocol based formal modeling methods of timing behavior and the verification method for component based systems. The architecture of the specification and verification tool named TC;I3V was given. An application example was introduced and the experimental results show that the timed behavior protocol based specification and verification methods can accurately model and conveniently verify errors of timing behavior in complex real-time component systems. Finally, TCBV and other related tools were compared and the differences between them were analyzed.

Key words: Real-time component system, Timing behavior,Formal methods,Specification,Compatibility verification tool