A proof system in PADS

Xinghua Yao; Min Zhang; Yixiang Chen

doi:10.1007/978-3-642-39718-9_23

A proof system in PADS

Xinghua Yao
, Min Zhang^*
, Yixiang Chen

^*Corresponding author for this work

Software Engineering Institute

East China Normal University

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

2 Scopus citations

Abstract

The PADS (Process Algebra for Demand and Supply) framework is an approach to model resource demand and supply for the formal analysis of hierarchical scheduling. Inspired by the demand relation in PADS, we propose a weak demand relation covering several cases which can not be described by a demand relation. And we explore some properties of weak demand relation which are similar to properties of demand relation. Especially, if two tasks are in a weak demand relation then their schedulabilities are closely related. Furthermore, we present a proof system for the weak demand relation in a decomposing-composing way, which helps to compare two tasks' schedulabilities. Finally, we prove that the proof system is sound and complete with respect to the semantic definition of weak demand relation.

Original language	English
Title of host publication	Theoretical Aspects of Computing, ICTAC 2013 - 10th International Colloquium, Proceedings
Publisher	Springer Verlag
Pages	391-408
Number of pages	18
ISBN (Print)	9783642397172
DOIs	https://doi.org/10.1007/978-3-642-39718-9_23
State	Published - 2013
Event	10th International Colloquium on Theoretical Aspects of Computing, ICTAC 2013 - Shanghai, China Duration: 4 Sep 2013 → 6 Sep 2013

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	8049 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	10th International Colloquium on Theoretical Aspects of Computing, ICTAC 2013
Country/Territory	China
City	Shanghai
Period	4/09/13 → 6/09/13

Keywords

demand relation
hierarchical scheduling
real-time process algebra
resource demand and resource supply

Access to Document

10.1007/978-3-642-39718-9_23

Cite this

Yao, X., Zhang, M., & Chen, Y. (2013). A proof system in PADS. In Theoretical Aspects of Computing, ICTAC 2013 - 10th International Colloquium, Proceedings (pp. 391-408). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8049 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-642-39718-9_23

@inproceedings{df995cedad764d97907aacc75b0bd78e,

title = "A proof system in PADS",

abstract = "The PADS (Process Algebra for Demand and Supply) framework is an approach to model resource demand and supply for the formal analysis of hierarchical scheduling. Inspired by the demand relation in PADS, we propose a weak demand relation covering several cases which can not be described by a demand relation. And we explore some properties of weak demand relation which are similar to properties of demand relation. Especially, if two tasks are in a weak demand relation then their schedulabilities are closely related. Furthermore, we present a proof system for the weak demand relation in a decomposing-composing way, which helps to compare two tasks' schedulabilities. Finally, we prove that the proof system is sound and complete with respect to the semantic definition of weak demand relation.",

keywords = "demand relation, hierarchical scheduling, real-time process algebra, resource demand and resource supply",

author = "Xinghua Yao and Min Zhang and Yixiang Chen",

year = "2013",

doi = "10.1007/978-3-642-39718-9\_23",

language = "英语",

isbn = "9783642397172",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "391--408",

booktitle = "Theoretical Aspects of Computing, ICTAC 2013 - 10th International Colloquium, Proceedings",

address = "德国",

note = "10th International Colloquium on Theoretical Aspects of Computing, ICTAC 2013 ; Conference date: 04-09-2013 Through 06-09-2013",

}

Yao, X, Zhang, M & Chen, Y 2013, A proof system in PADS. in Theoretical Aspects of Computing, ICTAC 2013 - 10th International Colloquium, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8049 LNCS, Springer Verlag, pp. 391-408, 10th International Colloquium on Theoretical Aspects of Computing, ICTAC 2013, Shanghai, China, 4/09/13. https://doi.org/10.1007/978-3-642-39718-9_23

A proof system in PADS. / Yao, Xinghua; Zhang, Min; Chen, Yixiang.
Theoretical Aspects of Computing, ICTAC 2013 - 10th International Colloquium, Proceedings. Springer Verlag, 2013. p. 391-408 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8049 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - A proof system in PADS

AU - Yao, Xinghua

AU - Zhang, Min

AU - Chen, Yixiang

PY - 2013

Y1 - 2013

N2 - The PADS (Process Algebra for Demand and Supply) framework is an approach to model resource demand and supply for the formal analysis of hierarchical scheduling. Inspired by the demand relation in PADS, we propose a weak demand relation covering several cases which can not be described by a demand relation. And we explore some properties of weak demand relation which are similar to properties of demand relation. Especially, if two tasks are in a weak demand relation then their schedulabilities are closely related. Furthermore, we present a proof system for the weak demand relation in a decomposing-composing way, which helps to compare two tasks' schedulabilities. Finally, we prove that the proof system is sound and complete with respect to the semantic definition of weak demand relation.

AB - The PADS (Process Algebra for Demand and Supply) framework is an approach to model resource demand and supply for the formal analysis of hierarchical scheduling. Inspired by the demand relation in PADS, we propose a weak demand relation covering several cases which can not be described by a demand relation. And we explore some properties of weak demand relation which are similar to properties of demand relation. Especially, if two tasks are in a weak demand relation then their schedulabilities are closely related. Furthermore, we present a proof system for the weak demand relation in a decomposing-composing way, which helps to compare two tasks' schedulabilities. Finally, we prove that the proof system is sound and complete with respect to the semantic definition of weak demand relation.

KW - demand relation

KW - hierarchical scheduling

KW - real-time process algebra

KW - resource demand and resource supply

UR - https://www.scopus.com/pages/publications/84885005578

U2 - 10.1007/978-3-642-39718-9_23

DO - 10.1007/978-3-642-39718-9_23

M3 - 会议稿件

AN - SCOPUS:84885005578

SN - 9783642397172

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 391

EP - 408

BT - Theoretical Aspects of Computing, ICTAC 2013 - 10th International Colloquium, Proceedings

PB - Springer Verlag

T2 - 10th International Colloquium on Theoretical Aspects of Computing, ICTAC 2013

Y2 - 4 September 2013 through 6 September 2013

ER -

A proof system in PADS

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this