Modeling and Verification of Processes Scheduling Based on Projection Temporal Logic for Multi-Core CPU
Zhenhua Duan · Xi'an Jiaotong Daxue xuebao · 2010
Software testing is unable to meet the verification needs of process scheduling for multi-core CPU,therefore a theorem proving approach with projection temporal logic(PTL) is adapted to verify the process scheduler.A general model supporting the most commonly used scheduling algorithms for multi-core CPU is constructed by a PTL formula S,and the desired property of the system is described by a PTL formula P,then whether the system possesses the property can be identified by proving whether or not S implying P is a theorem based on the axiomatization of PTL.As a case study,the correctness of the processes scheduling with the multilevel feedback queue scheduling algorithm over a two-core CPU is proved,which indicates that the proposed approach can be used to verify system properties of process scheduling over multi-core CPU and hence to ensure the reliability of the process scheduler.Since the process scheduler over multi-core CPU has the typical features of concurrent system,the method can also be applied to verify general concurrent systems.