This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Static Analysis of Real-Time Distributed Systems
April 1990 (vol. 16 no. 4)
pp. 373-388

A static analysis for reasoning about the temporal behaviors of programs in real-time distributed programming languages is proposed. The analysis is based on the action set semantics using the pure maximal parallelism model. It is shown how to specify and verify various timing properties of real-time programs. The approach provides only an approximate timing behavior, because the state information is ignored. However, many interesting properties such as parallel actions, deadlocks, livelocks, terminations, temporal errors, and failures, can be identified. Furthermore, the approach is compositional and thus makes it possible to reason about the timing properties incrementally. The method not only leads to efficient algorithms for the static analysis of CSP programs but also applies to many other languages.

[1] A. V. Aho, R. Sethi, and J. D. Ullman,Compilers: Principles, Techniques, and Tools. Reading, MA: Addison-Wesley, 1986.
[2] K. R. Apt, "A static analysis of CSP programs," inProc. Workshop on Program Logic(Pittsburgh, PA), June 1983.
[3] A. Bernstein and P. K. Harter, Jr., "Proving real-time properties of programs with temporal logic,"Operat. Syst. Rev., Vol. 15, no. 5, pp. 1-11, Dec. 1981.
[4] B. Dasarathy, "Timing constraints of real-time systems: Constructs for expressing them, methods of validating them,"IEEE Trans. Software Eng., vol. SE-11, no. 1, pp, 80-86, Jan. 1985.
[5] Reference Manual for the Ada Programming Language, U.S. Dep. Defense, Amer. Nat. Standards Inst., Rep. MIL-STD-1815A, Jan. 1983.
[6] N. Francez, D. Lehmann, and A. Pnueli, "A linear history semantics for distributed programming,"Trans. Comput. Syst., vol. 32, pp. 25-46, 1984.
[7] C. A. R. Hoare, "Communicating sequential processes,"Commun. ACM, vol. 21, pp. 666-677, 1978.
[8] C. A. R. Hoare, "A calculus of total correctness for communicating processes,"Sci. Comput. Program., vol. 1, pp. 49-72, 1981.
[9] J. Hooman, "A compositional proof-system for an occam-like real-time language," Eindhoven Univ. Technol., Tech. Rep. CSN 87/14, 1987.
[10] F. Jahanian and A. K. Mok, "A graph-theoretic approach for timing analysis and its implementation,"IEEE Trans. Comput., vol. 36, pp. 961-975, Aug. 1987.
[11] R. Koymans, R. K. Shyamasundar, W. P. de Roever, R. Gerth, and S. Arun-Kumar, "Compositional semantics for real-time distributed computing," inProc. Logics of Programs (Lecture Notes Comput. Sci., vol. 193). New York: Springer-Verlag, 1985 (extended version appeared inInform. Computat., vol. 79, no. 3, pp. 201-256, Dec. 1988).
[12] L. Y. Liu and R. K. Shyamasundar, "Temporal behaviors for real-time distributed systems," Pennsylvania State Univ., Tech. Rep. CS- 87-38, Dec. 1987.
[13] L. Y. Liu and R. K. Shyamasundar, "Exception handling in RT-CDL," Pennsylvania State Univ., Tech. Rep, CS-89-21, Aug. 1989; alsoComput. Lang., to be published.
[14] L. Y. Liu and R. K. Shyamasundar, "RT-CDL: A real time design language and its semantics," presented at the 11th World Computer Congr., IFIP'89, San Francisco, CA, Sept. 1989.
[15] L. Y. Liu and R. K. Shyamasundar, "Static detection for deadlocks, distributed terminations, and timing errors of real-time distributed programs," Pennsylvania State Univ., Tech. Rep. CS-89-32, Oct. 1989.
[16] R. Milner,A Calculus of Communicating Systems (Lecture Notes in Computer Science 92). New York: Springer-Verlag, 1980.
[17] J. Misra and K. M. Chandy, "Proofs of networks of processes,"IEEE Trans. Software Eng., vol. SE-7, no. 4, pp. 417-426, July 1981.
[18] H. R. Nielson, "A Hoare-like proof system for analyzing the computation time of programs,"Sci. Comput. Program., vol. 9, no. 1, pp. 107-136, Aug. 1987.
[19] J. S. Ostroff, "Real-time computer control of discrete systems modelled by extended state machine: A temporal logic approach," Univ. Toronto, Tech. Rep., Jan. 1987.
[20] J. L. Peterson,Petri Net Theory and the Modeling of Systems. Englewood Cliffs, NJ: Prentice-Hall, 1981.
[21] A. Pnueli, "Specification and development of reactive systems," inInformation processing 86, H. J. Kugler, Ed., 1986, pp. 845-858.
[22] A. Pnueli, "Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of CurrentTrends," inCurrent Trends in Concurrency: Overviews and Tutorials. W.-P. de Roever and G. Rozenberg, eds., Lecture Notes in Computer Science 224, Springer-Verlag, N.Y., 1986, pp. 510-584.
[23] A. Pnueli and E. Harel, "Applications of temporal logic to the specification of real-time systems," inProc. Formal Techniques in Real-Time and Fault-Tolerant Systems (LNCS 331), pp. 84-98, 1988.
[24] A. Salwicki and T. Muldner,On the Algorithmic Properties of Concurrent Programs(Lecture Notes Comput. Sci., vol. 125). New York: Springer-Verlag, 1981.
[25] R. K. Shyamasundar, K. T. Narayana, and T. Pitassi, "Semantics for nondeterministic asynchronous broadcast networks," inProc. 14th Int. Colloquium Automata, Languages and Programming, Karlsruhe, July 1987, pp. 72-83.
[26] R. K. Shyamasundar, J. Hooman, and R. Gerth, "Proof systems for real-time distributed programming," Pennsylvania State Univ., Tech. Rep. CS-87-19, June 1987.
[27] N. Soundararajan, "Axiomatic semantics of CSP," inProc. ACM TOPLAS, 1984, pp. 647-662.
[28] R. N. Taylor, "A general purpose algorithm for analyzing concurrent programs,"Commun. ACM, vol. 26, no. 5, pp. 362-376, May 1983.
[29] P. Wolper, "Temporal logic can be more expressive,"Inform. Contr., vol. 56, pp. 72-99, 1983.
[30] A. Zwarico and I. Lee, "Proving a network of real-time processes correct," inProc. IEEE Real-Time Systems Symp., 1985, pp. 169- 177.

Index Terms:
real-time distributed systems; static analysis; reasoning; temporal behaviors; programs; maximal parallelism model; timing properties; parallel actions; deadlocks; livelocks; terminations; temporal errors; failures; CSP programs; distributed processing; parallel programming; programming languages; real-time systems; software engineering.
Citation:
L.Y. Liu, R.K. Shyamasundar, "Static Analysis of Real-Time Distributed Systems," IEEE Transactions on Software Engineering, vol. 16, no. 4, pp. 373-388, April 1990, doi:10.1109/32.54290
Usage of this product signifies your acceptance of the Terms of Use.