Integrating Time and Resource into Circus

Geguang Pu; Zongyan Qiu; Jifeng He

doi:10.1016/j.entcs.2005.03.020

Integrating Time and Resource into Circus

Geguang Pu^*
, Zongyan Qiu
, Jifeng He

^*Corresponding author for this work

Research output: Contribution to journal › Article › peer-review

Abstract

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.

Original language	English
Pages (from-to)	401-418
Number of pages	18
Journal	Electronic Notes in Theoretical Computer Science
Volume	130
DOIs	https://doi.org/10.1016/j.entcs.2005.03.020
State	Published - 12 May 2005
Externally published	Yes

Keywords

Denotational semantics
Resource reasoning
Timed Circus
UTP

Access to Document

10.1016/j.entcs.2005.03.020

Cite this

@article{a209f4ee70f1460f8647c75673b8665a,

title = "Integrating Time and Resource into Circus",

abstract = "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.",

keywords = "Denotational semantics, Resource reasoning, Timed Circus, UTP",

author = "Geguang Pu and Zongyan Qiu and Jifeng He",

year = "2005",

month = may,

day = "12",

doi = "10.1016/j.entcs.2005.03.020",

language = "英语",

volume = "130",

pages = "401--418",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier B.V.",

}

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 -

Integrating Time and Resource into Circus

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this