关键词: 实时构件，时间行为协议，形式化描述，一致性验证

Abstract: The formal specification and consistency verification of complex real-time component systems' behavior can efficiently improve the systems' reusability, correctness and reliability. This paper analyzed the timed behavior protocol and the other mainstream formal specification methods of real-time behavior used in academia and industry. Based on the analysis we gave the substitution theory and the consistency verification algorithm based on timed behavior protocol,which can support complex real-time component based systems' development.

Key words: Realtime component, Timed behavior protocol, Formal specification, Consistency verification