Int J Performability Eng ›› 2017, Vol. 13 ›› Issue (8): 1312-1326.doi: 10.23940/ijpe.17.08.p13.13121326

• Original articles • Previous Articles     Next Articles

A Partial Supply Simulation Relation and its Proof System in PADS

Xinghua Yao and Hengyang Wu   

  1. 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

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