MODELING AND VERIFICATION OF REAL-TIME SYSTEMS

Abstract

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