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 implementationdependent 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).
KeywordsPredicate Symbol Execution Environment Occurrence Relation Constant Symbol Proof Method
Unable to display preview. Download preview PDF.
- F. Jahanian and A. Mok, “A Graph-Theoretic Approach for Timing Analysis and Its Implementation”, IEEE Transactions on Computers, August 1987.Google Scholar
- F. Jahanian and A. Mok, “Safety Analysis of Timing Properties in Real-Time Systems”, IEEE Transactions on Software Engineering, September 1986.Google Scholar
- F. Jahanian, R. Lee and A. Mok, “Semantics of Modechart in Real Time Logic”, Proceedings of the 21st Hawaii International Conference on System Science, January 1988.Google Scholar
- A. Mok, “Fundamental Design Problems of Distributed Systems for the Hard-Real-Time Environment”, PhD Thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, Massachusetts, May, 1983.Google Scholar