Formal specification and verification of components´ real-time behavior

Formal specification and verification of complex realtime component systems´ behavior can efficiently improve the systems´ correctness and reliability. This paper analyzed the formal specification and verification languages of components´ timed behavior. Based on the analysis we extended behavior protocol (BP) used in SOFA component model by incorporating timing constraint information and new operations into it. Besides simple and convenient to apply, extended behavior protocol is more power than BP and can specify sophisticated behavior in component based real-time systems. An example and discussion on applications of extended behavior protocol were given and verification of extended behavior protocol was discussed finally.