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.
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
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 ECRT 2003, pp. 279–285. IEEE Computer Society, Los Alamitos (2003)
Easwaran, A., Lee, I., Sokolsky, O.: Interface Algebra for Analysis of Hierarchical Real-Time Systems. Presented at Foundations of Interface Technologies, FIT 2008, Satellite Workshop of ETAPS 2008 (April 2008), http://repository.upenn.edu/cis_papers/373
Feng, X., Mok, A.: A Model of Hierarchical Real-Time Virtual Resources. In: Proceeding of RTSS 2002, 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)
Henzinger, T.A., Matic, S.: An Interface Algebra for Real-Time Components. In: Proceedings of RTAS 2006, 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 82(1), 158–171 (1994)
Lee, I., Philippou, A., Sokolsky, O.: Resources in Process Algebra. Journal of Logic and Algebraic Programming 72, 98–122 (2007)
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)
Núñez, M., Rodríguez, I.: PAMR: A Process Algebra for the Management of Resources in Concurrent Systems. In: Kim, M., Chin, B., Kang, S., Lee, D. (eds.) FORTE 2001. IFIP, vol. 69, pp. 169–184. Springer, Heidelberg (2002)
Philippou, A., Lee, I., Sokolsky, O.: PADS: An Approach to Modeling Resource Demand and Supply for the Formal Analysis of Hierarchical Scheduling. Theoretical Computer Science 413(1), 2–20 (2012)
Shin, I., Lee, I.: Compositional Real-Time Scheduling Framework. In: Proceeding of RTSS 2004, 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 2006, pp. 34–43. ACM, New York (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yao, X., Zhang, M., Chen, Y. (2013). A Proof System in PADS. In: Liu, Z., Woodcock, J., Zhu, H. (eds) Theoretical Aspects of Computing – ICTAC 2013. ICTAC 2013. Lecture Notes in Computer Science, vol 8049. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39718-9_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-39718-9_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39717-2
Online ISBN: 978-3-642-39718-9
eBook Packages: Computer ScienceComputer Science (R0)