AbstractIn this paper, a formal model is introduced for reasoning about resource allocation and scheduling in real-time systems. We extend the concurrent refinement language Circus [Woodcock, J.C.P. and A.L.C. Cavalcanti, The semantics of Circus, in: ZB2002(LNCS 2272) (2002), pp. 184–203] through integrating continuous time and resource information. This model reflects resource issues when modelling the behavior of a system, and allows temporal properties to be accurately determined. We also apply the model to the problem of partitioning in co-design, and show how the partitioned programs preserve the behavior of the specification correctly.