MODELING AND VERIFICATION OF REAL-TIME SYSTEMS

摘要

One aspect that separates real-time programs from sequential and concurrent programs is thatrncorrectness depends not only on the logical correctness but also on the temporal properties of thernsystem. In a multiprocessor environment, the allocation of processes among processors and thernscheduling policy of each processor are two essential parameters that affect timing behavior of thernsystem, and should be considered in formal modeling and verification techniques. In this paper, wernintroduce a precedence graph based model for real-time systems. Then, based on this model, werndevelop an axiomatic approach to reason about the timing behavior of real-time programs. Thernapproach is demonstrated for maximal parallelism and priority based preemptive scheduling.