Research On Proof Systems In A Process Algebra For Demand And Supply

As component-based design has been widely accepted and used by workers in Cyber-Physical System (shortly, CPS), hierarchical scheduling analysis is stimulated and is devel-oped. Hierarchical scheduling analysis framework requires timing properties of component be abstracted and be composed. Process algebra supports modular specification and modular veri-fication. And its two advantages shows that it is an appropriate choice as a hierarchical schedul-ing analysis model. Process Algebra for Demand and Supply (PADS), proposed by Philippou et al., is a framework for the formal analysis of hierarchical scheduling. In PADS, every execution in tasks is modeled as a set of resources with priorities, and the aspect of supplying resources is represented to be a set of grant resources without priorities; then, tasks’schedulabilites are described to be a match between task process and supply process. To our knowledge, the tasks’ schedulability theories in PADS contain the following results, i.e. determining conditions about whether a task is schedulable or not, e.g. supply simulation relation, composing schedulabilities and tasks’hierarchies. For the gotten theory, it is still a challenge to formally analyze and veri-fy scheduling problems in CPS. In this paper, based on these results we will study some theories for the formal analysis and verification of hierarchical scheduling analysis in PADS model.Firstly, we explore the schedulability theory in PADS. We get some properties about op-erational semantics in PADS and properties about supply simulation relation; and based on these properties we give a proof system for the supply simulation relation by a decomposing-composing way. Moreover, the proof system is proved to be sound and complete with re-spect to the semantic definition of supply simulation relation. For the hierarchy of tasks’ schedulabilites, we extend the original demand relation, and present a local demand relation which more schedulable tasks. Then, for answering how to infer whether there exists a lo-cal demand relation between tasks, we give a proof system, and we prove the soundness and completeness for the proof system.Secondly, we propose a theory of partial schedulability in PADS. The original schedulabil-ity requires that every executable path in a task must successfully get all the requested resources. In order to describe and analyze some cases in which resource requests on some execution path of a task are satisfied by a supply, we propose a partial simulating supply relation and define task’s partial schedulability. We explore some related properties, and get that a supply simula- tion relation is a partial simulating supply relation, and present a proof system for the partial simulating supply relation, and give its proofs of the soundness and completeness. Besides, we study tasks’hierarchies for the partial schedulability. We propose a full-function demand relation, and get that if two task are in a full-function demand relation then their partial schedu-labilities are comparable. Further, we give a proof system in order to infer whether two tasks are in a full-function relation or not, and we prove that it is sound and complete with respect to the semantic definition of full-function demand relation.Thirdly, in order to describe and characterize supplying behaviour of supply processes and requesting behaviour of task processes, we present process equivalence theory in PADS, which contains a trace-equivalent relation between supply processes and a bisimulation over task pro-cesses. From the mathematical function view we define a trace of a supply process, and get some properties. Specially, a property says that the trace of a supply is just the set of all re-source supply set sequence contained in its evolution. Furthermore, we propose a sound and complete inference system for the trace-equivalent relation. Other side, we define a bisimuation between tasks based on tasks’operational semantics, and analyze some properties about the bisimulation. There is such a property that any task is bisimulted by a task without containing the operator. Then, we give a proof system for the bisimulation over tasks, and prove that it is sound and complete with respect to its semantic definition. Lastly, we investigate rela-tions between the process equivalence theory and the schedulability theory, and study relations between the process equivalence theory and the partial schedulability theory. We get two im-portant conclusions. One is that for two supplies in a process equivalence relation if one supply could schedule a task then so the other does. The other conclusion says that two tasks in a bisimulating relation have the same schedulability and the same partial schedulability.