Models based on Timed Automata often adapt a simple structure, e.g., a network of Timed Automata with no hierarchy. The benefit is that efficient model checking is made feasible. Nonetheless, designing and verifying real-time systems are becoming an increasingly difficult task due to the widespread applications and increasing complexity of such systems. High-level requirements for real-time systems are often stated in terms like deadline, timeout, and waituntil. In industrial case studies of real-time system verification, system requirements are often structured into phases, which are then composed sequentially. Unlike Statechart (with clocks) or timed process algebras, Timed Automata lacks of high-level compositional patterns (besides parallel composition of a network of Timed Automata) for hierarchical design. As a result, users often need to manually cast those terms into a set of clock variables with carefully calculated clock constraints. The process is tedious and error-prone.

This module supports real-time systems which are specified compositional timed processes. Timed processes running in parallel may communicate through either a shared memory or channel communications. Instead of explicitly manipulating clock variables, a number of timed behavioral patterns are used to capture quantitative timing requirements, e.g., delay, timeout, deadline, waituntil, timed interrupt, etc. For such systems, a model checking algorithm can be used to explore on-the-fly all system behaviors by dynamically creating (only if necessary) and pruning clock variables (as early as possible), and maintaining/solving a constraint on the active clocks.