A Partial Supply Simulation Relation and its Proof System in PADS

doi:10.23940/ijpe.17.08.p13.13121326

Abstract

Abstract: PADS (Process Algebra for Demand and Supply) is a formal framework to analyze hierarchical scheduling in real-time embedded systems. Inspired by the supply simulation relation in PADS, we introduce a partial supply simulation relation in order to describe the fact that an unschedulable task may finish on time. It is more general than the supply simulation relation. Then, we explore some properties of partial supply simulation relation. Furthermore, we establish a proof system for the partial supply simulation relation in a decomposing-composing way, which helps to infer tasks' partial schedulabilities. Finally, it is proved that the proof system is sound and complete with respect to the semantic definition of partial supply simulation relation.

Submitted on July 25, 2017; Revised on August 30, 2017; Accepted on September 15, 2017(This paper was presented at the Third International Symposium on System and Software Reliability.
References: 18

Xinghua Yao and Hengyang Wu. A Partial Supply Simulation Relation and its Proof System in PADS [J]. Int J Performability Eng, 2017, 13(8): 1312-1326.

Add to citation manager EndNote|Reference Manager|ProCite|BibTeX|RefWorks

References 0

	M. ?sberg, P. Pettersson, and T. Nolte, “Modeling, Verification and Synthesis of Two-Tier Hierarchical Fixed-Priority Preemptive Scheduling,” in Proceedings of the 23rd Euromicro Conference on Real-Time Systems, pp. 172-184, Porto, Portugal, July 2011
	H. Ben-Abdallah, J.-Y. Choi, D. Clarke, Y. S. Kim, I. Lee, and H.-L. Xie, “A Process Algebraic Approach to the Schedulability Analysis of Real-Time Systems,” Real-Time Systems, vol. 15, no. 3, pp. 189-219, November 1998
	G. Bucci, A. Fedeli, L. Sassoli, and E. Vicario, “Modeling Flexible Real Time Systems with Preemptive Time Petri Nets,” in Proceedings of the 15th Euromicro Conference on Real-Time Systems, pp. 279-286, Porto, Portugal, July 2003
	A. Easwaran, I. Lee, and O. Sokolsky, “Interface Algebra for Analysis of Hierarchical Real-Time Systems,” in Proceedings of the 2nd International Workshop on Foundations of Interface Technologies (FIT), Budapest, Hungary, April 2008
	X. Feng and A. Mok, “A Model of Hierarchical Real-Time Virtual Resources,” in Proceedings of the 23rd IEEE Real-Time Systems Symposium (RTSS), pp. 26-35, Austin, Texas, USA, December 2002
	E. Fersman, P. Krcál, P. Pettersson, and Y. Wang, “Task Automata: Schedulability, Decidability and Undecidability,” Information and Computation, vol. 205, no. 8, pp. 1149-1172, August 2007
	E. Fersman, P. Pettersson, and Y. Wang, “Timed Automata with Asynchronous Processes: Schedulability and Decidability,” in Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 67-82, Grenoble, France, April 2002
	T. A. Henzinger and S. Matic, “An Interface Algebra for Real-Time Components,” in Proceedings of the 12th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), pp.253-266, San Jose, California, United States, April 2006
	I. Lee, P. Brémond-Grégoire, and R. Gerber, “A Process Algebraic Approach to the Specification and Analysis of Resource-Bound Real-Time Systems,” Proceedings of the IEEE, vol. 82, no. 1, pp. 158-171, 1994
	I. Lee, A. Philippou, and O. Sokolsky, “Resources in Process Algebra,” Journal of Logic and Algebraic Programming, vol. 72, no. 1, pp. 98-122, January 2007
	M. Mousavi, M. Reniers, T. Basten, and M. Chaudron, “PARS: A Process Algebra with Resources and Schedulers,” in Proceedings of the 1st International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), pp.134-150, Marseille, France, September 2003
	M. Nú?ez and I. Rodríguez, “PAMR: A Process Algebra for the Management of Resources in Concurrent Systems,” in Proceedings of the 21st International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), pp.169-184, Cheju Island, Korea, August 2001
	J. Park, I. Lee, O. Sokolsky, D. Y. Hwang, S. Ahn, J. - Y. Choi, and I. Kang, “A Process Algebraic Approach to the Schedulability Analysis and Workload Abstraction of Hierarchical Real-Time Systems,” Journal of Logical and Algebraic Methods in Programming, vol. 92, pp. 1-18, November 2017
	A. Philippou, I. Lee, and O. Sokolsky, “PADS: An Approach to Modeling Resource Demand and Supply for the Formal Analysis of Hierarchical Scheduling,” Theoretical Computer Science, vol. 413, no. 1, pp. 2-20, January 2012
	I. Shin and I. Lee, “Compositional Real-Time Scheduling Framework,” in Proceedings of the 25th IEEE International Real-Time Systems Symposium (RTSS), pp. 57-67, Lisbon, Portugal, December 2004
	L. Thiele, E. Wandeler, and N. Stoimenov, “Real-Time Interfaces for Composing Real-Time Systems,” in Proceedings of the 6th ACM & IEEE International Conference on Embedded Software (EMSOFT), pp. 34-43, Seoul, Korea, October 2006
	X. Yao and Y. Chen, “A Proof System in Process Algebra for Demand and Supply,” in Proceedings of the 8th International Conference on Software Security and Reliability Companion (SERE-C), pp. 228-236. San Francisco, California, USA, June 30-July 2, 2014
	X. Yao, M. Zhang, and Y. Chen, “A Proof System in PADS,” in Proceedings of the 10th International Colloquium on Theoretical Aspects of Computing (ICTAC), pp. 391-408, Shanghai, China, September 2013