Abstract
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 \(\overline{CPU}\) 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.
This research was supported in part by NSF grants CNS-0834524 and CNS-0720703.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Altisen, K., Gößler, G., Pnueli, A., Sifakis, J., Yovine, Y.: A framework for scheduler synthesis. In: Proceedings of RTSS’99, pp. 154–163. IEEE Computer Society, Los Alamitos (1999)
Altisen, K., Gößler, G., Sifakis, J.: Scheduler modeling based on the controller synthesis paradigm. Real-Time Systems 23(1-2), 55–84 (2002)
Ben-Abdallah, H., Choi, J.-Y., Clarke, D., Kim, Y.S., Lee, I., Xie, H.-L.: A Process Algebraic Approach to the Schedulability Analysis of Real-Time Systems. Real-Time Systems 15, 189–219 (1998)
Bucci, G., Fedeli, A., Sassoli, L., Vicario, E.: Modeling flexible real time systems with preemptive time Petri nets. In: Proceedings of ECRTS’03, pp. 279–286. IEEE Computer Society, Los Alamitos (2003)
Deng, Z., Liu, J.W.-S.: Scheduling real-time applications in an open environment. In: Proceedings of RTSS’97, pp. 308–319. IEEE Computer Society Press, Los Alamitos (1997)
Easwaran, A., Anand, M., Lee, I.: Compositional analysis framework using edp resource models. In: Proceedings of RTSS’07, pp. 129–138. IEEE Computer Society, Los Alamitos (2007)
Easwaran, A., Lee, I., Sokolsky, O.: Interface algebra for analysis of hierarchical real-time systems. In: Proceedings of FIT (2008)
Feng, X., Mok, A.: A model of hierarchical real-time virtual resources. In: Proceedings of RTSS’02, pp. 26–35. IEEE Computer Society, Los Alamitos (2002)
Fersman, E., Krcál, P., Pettersson, P., Yi, W.: Task automata: Schedulability, decidability and undecidability. Information and Computation 205(8), 1149–1172 (2007)
Fersman, E., Pettersson, P., Yi, W.: Timed automata with asynchronous processes: Schedulability and decidability. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 67–82. Springer, Heidelberg (2002)
GmbH, R.-T.S.: Real-Time Hybervisor (2010), http://www.real-time-systems.com
Henzinger, T.A., Matic, S.: An interface algebra for real-time components. In: Proceedings of RTAS’06, pp. 253–263. IEEE Computer Society, Los Alamitos (2006)
Lee, I., Brémond-Grégoire, P., Gerber, R.: A Process Algebraic Approach to the Specification and Analysis of Resource-Bound Real-Time Systems. Proceedings of the IEEE, 158–171 (1994)
Lee, I., Philippou, A., Sokolsky, O.: Resources in process algebra. Journal of Logic and Algebraic Programming 72, 98–122 (2007)
Linuxworks. LynxSecure Embedded Hypervisor and Separation Kernel (2010), http://www.lynuxworks.com/virtualization/hypervisor.php
Lipari, G., Bini, E.: Resource partitioning among real-time applications. In: Proceedings of ECRTS’03, pp. 151–160. IEEE Computer Society, Los Alamitos (2003)
Liu, J.: Real-time systems. Prentice Hall, Englewood Cliffs (2000)
Mousavi, M., Reniers, M., Basten, T., Chaudron, M.: PARS: a process algebra with resources and schedulers. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 134–150. Springer, Heidelberg (2004)
Nunez, M., Rodriguez, I.: PAMR: A process algebra for the management of resources in concurrent systems. In: Proceedings of FORTE’01, pp. 169–184 (2001)
Saewong, S., Rajkumar, R., Lehoczky, J., Klein, M.: Analysis of hierarchical fixed-priority scheduling. In: Proceedings of ECRTS’02, pp. 173–181. IEEE Computer Society, Los Alamitos (2002)
Shin, I., Lee, I.: Periodic resource model for compositional real-time guarantees. In: Proceedings of RTSS’03, pp. 2–13. IEEE Computer Society, Los Alamitos (2003)
Shin, I., Lee, I.: Compositional real-time scheduling framework. In: Proceedings of RTSS’04, pp. 57–67. IEEE Computer Society, Los Alamitos (2004)
Thiele, L., Wandeler, E., Stoimenov, N.: Real-time interfaces for composing real-time systems. In: Proceedings of EMSOFT’06. ACM, New York (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Philippou, A., Lee, I., Sokolsky, O., Choi, JY. (2010). A Process Algebraic Framework for Modeling Resource Demand and Supply. In: Chatterjee, K., Henzinger, T.A. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2010. Lecture Notes in Computer Science, vol 6246. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15297-9_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-15297-9_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15296-2
Online ISBN: 978-3-642-15297-9
eBook Packages: Computer ScienceComputer Science (R0)