TY - JOUR
T1 - Integrating Time and Resource into Circus
AU - Pu, Geguang
AU - Qiu, Zongyan
AU - He, Jifeng
PY - 2005/5/12
Y1 - 2005/5/12
N2 - In 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.
AB - In 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.
KW - Denotational semantics
KW - Resource reasoning
KW - Timed Circus
KW - UTP
UR - https://www.scopus.com/pages/publications/18144409504
U2 - 10.1016/j.entcs.2005.03.020
DO - 10.1016/j.entcs.2005.03.020
M3 - 文章
AN - SCOPUS:18144409504
SN - 1571-0661
VL - 130
SP - 401
EP - 418
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
ER -