TY - GEN
T1 - A process algebraic framework for modeling resource demand and supply
AU - Philippou, Anna
AU - Lee, Insup
AU - Sokolsky, Oleg
AU - Choi, Jin Young
N1 - Funding Information:
This research was supported in part by NSF grants CNS-0834524 and CNS-0720703.
PY - 2010
Y1 - 2010
N2 - As real-time embedded systems become more complex, resource partitioning is increasingly used to guarantee real-time performance. Recently, several compositional frameworks of resource partitioning have been proposed using real-time scheduling theory with various notions of real-time tasks running under restricted resource supply environments. However, these real-time scheduling-based approaches are limited in their expressiveness in that, although capable of describing resource-demand tasks, they are unable to model resource supply. This paper describes a process algebraic framework for reasoning about resource demand and supply inspired by the timed process algebra ACSR. In ACSR, real-time tasks are specified by enunciating their consumption needs for resources. To also accommodate resource-supply processes we define PADS where, given a resource CPU, the complimented resource denotes for availability of CPU for the corresponding demand process. Using PADS, we define a supply-demand relation where a pair (S, T) belongs to the relation if the demand process T can be scheduled under supply S. We develop a theory of compositional schedulability analysis as well as a technique for synthesizing an optimal supply process for a set of tasks. We illustrate our technique via a number of examples.
AB - As real-time embedded systems become more complex, resource partitioning is increasingly used to guarantee real-time performance. Recently, several compositional frameworks of resource partitioning have been proposed using real-time scheduling theory with various notions of real-time tasks running under restricted resource supply environments. However, these real-time scheduling-based approaches are limited in their expressiveness in that, although capable of describing resource-demand tasks, they are unable to model resource supply. This paper describes a process algebraic framework for reasoning about resource demand and supply inspired by the timed process algebra ACSR. In ACSR, real-time tasks are specified by enunciating their consumption needs for resources. To also accommodate resource-supply processes we define PADS where, given a resource CPU, the complimented resource denotes for availability of CPU for the corresponding demand process. Using PADS, we define a supply-demand relation where a pair (S, T) belongs to the relation if the demand process T can be scheduled under supply S. We develop a theory of compositional schedulability analysis as well as a technique for synthesizing an optimal supply process for a set of tasks. We illustrate our technique via a number of examples.
UR - http://www.scopus.com/inward/record.url?scp=78049411023&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-15297-9_15
DO - 10.1007/978-3-642-15297-9_15
M3 - Conference contribution
AN - SCOPUS:78049411023
SN - 3642152961
SN - 9783642152962
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 183
EP - 197
BT - Formal Modeling and Analysis of Timed Systems - 8th International Conference, FORMATS 2010, Proceedings
T2 - 8th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2010
Y2 - 8 September 2010 through 10 September 2010
ER -