Username   Password       Forgot your password?  Forgot your username? 

A Partial Supply Simulation Relation and its Proof System in PADS

Volume 13, Number 8, December 2017, pp. 1312-1326
DOI: 10.23940/ijpe.17.08.p13.13121326

Xinghua Yao, Hengyang Wu

aSchool of Electronic and Electric Engineering, Shanghai University of Engineering Science, Shanghai 201620, China
bSchool of Computer Science and Software Engineering, East China Normal University, Shanghai 200062, China

(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.)



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.

 

References: 18

      1. 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
      2. 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
      3. 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
      4. 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
      5. 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
      6. 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
      7. 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
      8. 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
      9. 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
      10. 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
      11. 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
      12. 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
      13. 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
      14. 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
      15. 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
      16. 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
      17. 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
      18. 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

           

          Click here to download the paper.

          Please note : You will need Adobe Acrobat viewer to view the full articles.Get Free Adobe Reader

           
          This site uses encryption for transmitting your passwords. ratmilwebsolutions.com