Verification of schedulability for real-time programs
Zhiming Liu, Mathai Joseph, Tomasz Janowski · Formal Aspects of Computing · 1995
Abstract Assume that a real-time program P T consisting of a number of parallel processes is executed on a system having a set Pr of processors which are shared between the processes by a real-time scheduler S T . Assume that P T must meet some timing deadlines. We show that such an implementation of P T can be represented as a transformationL( P T ) and that the deadlines of P T will be met if they are satisfied by the timing properties of the transformed program. The condition for feasibility of a real-time program executed under a scheduler is formalized and rules are provided for verification. The scheduler S T can be specified generically and applied to different programs, making it unnecessary to introduce low-level operations such as scheduling primitives into the programming language. Thus real-time program specification and Schedulability can be considered in the same framework and the timing properties of a program can be determined at the specification level. By separating the specification of the scheduler from that of the program, the feasibility of an implementation can be proved by considering a scheduling policy rather than its implementation details.