Abstract
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).
Supported by a research grant from the Office of Naval Research under ONR contract number N00014-89-J-1472.
Preview
Unable to display preview. Download preview PDF.
References
F. Jahanian and A. Mok, “A Graph-Theoretic Approach for Timing Analysis and Its Implementation”, IEEE Transactions on Computers, August 1987.
F. Jahanian and A. Mok, “Safety Analysis of Timing Properties in Real-Time Systems”, IEEE Transactions on Software Engineering, September 1986.
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.
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.
C. L. Liu and J. W. Layland, “Scheduling Algorithms for Multiprogramming in a Hard-Real-Time Environment”, JACM, vol. 20, 1973, pp. 46–61.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mok, A.K. (1992). Coping with implementation dependencies in real-time system verification. In: de Bakker, J.W., Huizing, C., de Roever, W.P., Rozenberg, G. (eds) Real-Time: Theory in Practice. REX 1991. Lecture Notes in Computer Science, vol 600. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0032004
Download citation
DOI: https://doi.org/10.1007/BFb0032004
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55564-3
Online ISBN: 978-3-540-47218-6
eBook Packages: Springer Book Archive