Verification of schedulability for real-time programs |
| |
Authors: | Zhiming Liu Mathai Joseph Tomasz Janowski |
| |
Affiliation: | (1) Department of Mathematics and Computer Science, University of Leicester, University Road, LE1 7RH Leicester, UK;(2) Department of Computer Science, University of Warwick, Coventry, UK |
| |
Abstract: | Assume that a real-time programP
T consisting of a number of parallel processes is executed on a system having a setPr of processors which are shared between the processes by a real-time schedulerS
T. Assume that PT must meet some timing deadlines. We show that such an implementation ofP
T can be represented as a transformationL(P
T) and that the deadlines ofP
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 schedulerS
T can be specifiedgenerically 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. |
| |
Keywords: | Real-time program Specification Refinement Real-time scheduler Schedulability Feasibility |
本文献已被 SpringerLink 等数据库收录! |
|