A Proof System in PADS

摘要

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