COPING WITH IMPLEMENTATION DEPENDENCIES IN REAL-TIME SYSTEM VERIFICATION

A major difficulty in verifying real-time systems is that behavior involving quantitative timing often depends on assumptions about the execution environment, in particular the availability of resources (e.g., number of CPUs) and the resource sharing policy of the run-time system (e.g., process scheduling algorithm). Thus a proof that a real-time program satisfies its quantitative specification is sensitive to assumptions about implementation dependencies. While these dependencies are in general unavoidable, it is important to isolate them in a proof of correctness so that if the execution environment changes, the impact of a change can be readily identified and understood. In this paper, we discuss a proof method that observes the principle of separation of concerns. This method involves two steps. In the first step, we determine if a timing property can be proved from the system specification, and identify implementation-dependent assumptions, if any, that are required to derive a proof. In the second step, we determine if the system specification and other required implementation dependencies can be enforced by control structures that meet the required timing constraints. The advantage of this method is that implementation dependencies are explicitly identified and are brought in as needed. This separation of concerns is especially important for the maintenance of real-time programs. We show that both steps of this method can be accomplished by making use of the logic RTL (Real Time Logic).