A Method on Specification and Verification of Component Interaction in Real-Time Reactive Systems

We present timed component-interaction automata with cost (TCIAC) to specify and verify component interaction behavior, timing cost and timing constraint information in component-based real-time reactive systems. TCIAC extends the description ability of component interaction automata by binding each action with a time interval and a timing cost value. The timing cost values of sequence and parallel actions can be worked out using a timing cost computing semiring we presented in this paper. TCIAC models of real-time components can be composed together based on the TCIAC composition definition. We discuss the application of TCIAC through a simple railroad crossing control system. We model the system using TCIAC for specifying and verifying the timeliness and other trustworthiness properties of component interaction.