Real-Time Component Composition Using Hierarchical Timed Automata

In component-based software development, it is important to use formal models to describe component composition. However, the existing component composition models generally ignore real-time issues. We present a formal integration model based on Hierarchical Timed Automata (HTA) for real-time software system. We present formal definition of components and different component composition techniques. We then introduce the notions of composable and compatible composition, and use Multiset Labeled Transition Systems to represent the interface actions of HTA to perform compositional verification. This hierarchical and unified framework establishes the foundation for formal analysis of real-time properties of the system.