This Article 
 Bibliographic References 
 Add to: 
Reasoning About Time in Higher-Level Language Software
July 1989 (vol. 15 no. 7)
pp. 875-889

A methodology for specifying and providing assertions about time in higher-level-language programs is described. The approach develops three ideas: the distinction between, and treatment of, both real-time and computer times; the use of upper and lower bounds on the execution times of program elements; and a simple extension of Hoare logic to include the effects of the passage of real-time. Schemas and examples of timing bounds and assertions are presented for a variety of statement types and programs, such as conventional sequential programs including loops, time-related statements such as delay, concurrent programs with synchronization, and software in the presence of interrupts. Examples of assertions that are proved include deadlines, timing invariants for periodic processes, and the specification of time-based events such as those needed for the recognition of single and double clicks from a mouse button.

[1] Military Standard Ada Programming Language, U.S. Dep. Defense, Washington, DC, ANSI/MIL-STD-1815A, Jan. 1983.
[2] L. L. Alger and J. H. Lala, "A real time operating system for a nuclear power plant computer," inProc. Real-Time Systems Symp., IEEE Comput. Soc., Dec. 1986, pp. 244-248.
[3] T. P. Baker and G. M. Scallon, "An architecture for real-time software systems,"IEEE Software, pp. 50-58, May 1986.
[4] G. Berry and L. Cosserat, "The Esterel synchronous programming language and its mathematical semantics," inProc. CMU Seminar on Concurrency, Lecture Notes in Computer Science 197, Springer-Verlag, 1985.
[5] L. Bic and A. Shaw,The Logical Design of Operating Systems, 2nd ed. Englewood Cliffs, NJ: Prentice-Hall, 1988.
[6] L. Cardelli and R. Pike, "Squeak: A language for communicating with mice,"Proc SIGGRAPH 85, ACM SIGGRAPH 19, pp. 199-204, July 1985.
[7] D. Cheriton, M. Malcolm, L. Melen, and G. Sager, "Thoth, A portable real time operating system,"Commun. ACM, vol. 22, pp. 105-115, 1979.
[8] R. Clapp et al., "Toward Real-Time Performance Benchmarks for Ada,"Comm. ACM, Vol. 29, No. 8, Aug. 1986, pp. 760-778.
[9] B. Dasarathy, "Timing constraints of real-time systems: Constructs for expressing them, methods for validating them,"Commun. ACM, vol. 29, pp. 80-86, Jan. 1985.
[10] V. H. Haase, "Real-time-behavior of programs,"IEEE Trans. Software Eng., vol. SE-7, pp. 454-501, Sept. 1981.
[11] V. H. Haase, "Modular design of real-time systems," inSystem Description Methodologies, D. Teichroew and G. David, Eds. Amsterdam, The Netherlands: Elsevier North-Holland, 1985, pp. 91-100.
[12] C. A. R. Hoare, "An axiomatic basis for computer programming,"Commun. ACM, vol. 12, no. 10, pp. 576-583, 1969.
[13] F. Jahanian and A. K. Mok, "Safety analysis of timing properties in real-time systems,"IEEE Trans. Software Eng., vol. SE-12, no. 9, pp. 890-904, Sept. 1986.
[14] A. D. Stoyenko and E. Kligerman, "Real-time Euclid: a language for reliable real-time systems,"IEEE Trans. Software Eng., vol. SE-12, pp. 940-949, Sept. 1986.
[15] D. E. Knuth,The Art of Computer Programming, Vol. 1. Reading, MA: Addison-Wesley, 1973.
[16] U. W. Kulish and W. L. Miranker, Eds.,A New Approach to Scientific Computation. New York: Academic, 1983.
[17] L. Lamport, "Time, clocks, and the ordering of events in a distributed system,"Commun. ACM, vol. 21, no. 7, pp. 558-565, July 1978.
[18] A. K.-L. Mok, "Fundamental design problems of distributed system. for the hard real-time environment," Ph.D. dissertation, Massachusetts Inst. Technol., Cambridge, May 1983.
[19] R. E. Moore.Interval Analysis. Englewood Cliffs. NJ: Prentice-Hall, 1966.
[20] A. Pnueli, presentation given at the Real-Time Systems Issues Workshop, Univ. Texas, Austin, Dec. 1986.
[21] A. Shaw, "Software clocks, concurrent programming, and slice-based scheduling," inProc. Real-Time Systems Symp., IEEE Comput. Soc., Dec. 1986, pp. 14-18.
[22] A. Shaw, "Reasoning about time in higher-level language software," Lab. MASI, Univ. Paris 6, Res. Rep., Apr. 1984.
[23] VAXElan Technical Summary, Digital Equipment Corp., 1983.
[24] R. A. Volz and T. N. Mudge, "Instruction level mechanisms for accurate real-time task scheduling," inProc Real-Time System. Symp., IEEE Comput. Soc., Dec. 1986, pp. 209-215.
[25] N. Werum and H. Windauer,lntroduction to PEARL. 2nd ed., Berlin, Germany: Vieweg, 1983.
[26] N. Wirth, "A fast and compact compiler for Modula-2," Inst. Informatik, ETH, Zurich, Tech. Rep. 64, July 1986.
[27] N. Wirth, "Microprocessor architectures: A comparison based on code generation by compiler,"CACM, vol. 29, no. 10, pp. 978-990, Oct. 1986.

Index Terms:
upper bounds; higher-level language software; assertions; real-time; computer times; lower bounds; execution times; program elements; Hoare logic; timing bounds; sequential programs; time-related statements; delay; concurrent programs; synchronization; deadlines; timing invariants; periodic processes; specification; formal logic; formal specification; real-time systems; synchronisation
A.C. Shaw, "Reasoning About Time in Higher-Level Language Software," IEEE Transactions on Software Engineering, vol. 15, no. 7, pp. 875-889, July 1989, doi:10.1109/32.29487
Usage of this product signifies your acceptance of the Terms of Use.