Compositional Refinement for Real-Time Systems with Priorities

High-level requirements of real-time systems like as time constraints, communications and execution schedulability make the verification of real-time models arduous, where a system is the interaction of a possibly unbounded set of components. Priorities have been introduced to resolve execution conflicts, and by that, prevent the combinatorial explosion of state space. In this paper, we are interested in the composition and refinement of timed systems by considering static and dynamic priorities. Firstly, we propose a revised definition of the product of extended timed transition systems with static and dynamic priorities associated to individual transitions. Afterwards, we study the(compositional) refinement of compound extended timed systems. Without sacrificing compositionality, we instantiate this framework for the case of UPPAAL networks of timed automata with static priority Committed ness, dynamic priority between channels and priority between processes. Moreover, we show how to associate an Extended Timed Transition System (ETTS) to timed automata (TA), where an unique generalized dynamic priority system of ETTS is derived from both dynamic priority orders: priority between channels and priority between processes.