Title :
A Proof System in Process Algebra for Demand and Supply
Author :
Xinghua Yao ; Yixiang Chen
Author_Institution :
MoE Eng. Res. Center for Software/Hardware Co.-design Technol. & Applic., East China Normal Univ., Shanghai, China
fDate :
June 30 2014-July 2 2014
Abstract :
Process Algebra for Demand and Supply (shortly, PADS), proposed by Philippou et al., is a process algebra model for the formal analysis of hierarchical scheduling. They introduce a basic notion of supply simulation relation to characterize task´s schedulability. In this paper, we first investigate some properties of supply simulation relation. And then based on these properties, we present a proof system for the supply simulation relation in a decomposing-composing way and prove its soundness and completeness with respect to the semantic definition of a supply simulation relation. The soundness and completeness guarantee that the proof system is used to determine whether a task is schedulable by a supply or not.
Keywords :
embedded systems; process algebra; scheduling; theorem proving; PADS; hierarchical scheduling formal analysis; process algebra for demand and supply; process algebra model; proof system; supply simulation relation; task schedulability; Algebra; Analytical models; Computational modeling; Real-time systems; Semantics; Silicon; Software; process algebra for supply and demand; proof system; scheduling analysis; supply simulation relation;
Conference_Titel :
Software Security and Reliability-Companion (SERE-C), 2014 IEEE Eighth International Conference on
Conference_Location :
San Francisco, CA
DOI :
10.1109/SERE-C.2014.44
