Abstract: Formal specification and verification on complex real-time component system' s interaction behavior have great significance of improving component systems' trustworthy properties such as correctness and reliability. The advantages and disadvantages of using process algebra and automata to model components interaction behavior were analyzed, and timed component interaction automata(TCIA) based modeling methods were presented based on the analysis.The related definition, composition and verification algorithm of I}CIA were given. Models based on I}CIA can clearly specify components' interaction behavior, architecture and real-time information in detail and arc convenient to verify.Finally, an application example was introduced.

Key words: Component, Interaction behavior, Formal specification, Automata