
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
L.Y. Liu, R.K. Shyamasundar, "Static Analysis of RealTime Distributed Systems," IEEE Transactions on Software Engineering, vol. 16, no. 4, pp. 373388, April, 1990.  
BibTex  x  
@article{ 10.1109/32.54290, author = {L.Y. Liu and R.K. Shyamasundar}, title = {Static Analysis of RealTime Distributed Systems}, journal ={IEEE Transactions on Software Engineering}, volume = {16}, number = {4}, issn = {00985589}, year = {1990}, pages = {373388}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.54290}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Static Analysis of RealTime Distributed Systems IS  4 SN  00985589 SP373 EP388 EPD  373388 A1  L.Y. Liu, A1  R.K. Shyamasundar, PY  1990 KW  realtime 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; realtime systems; software engineering. VL  16 JA  IEEE Transactions on Software Engineering ER   
A static analysis for reasoning about the temporal behaviors of programs in realtime 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 realtime 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: AddisonWesley, 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 realtime properties of programs with temporal logic,"Operat. Syst. Rev., Vol. 15, no. 5, pp. 111, Dec. 1981.
[4] B. Dasarathy, "Timing constraints of realtime systems: Constructs for expressing them, methods of validating them,"IEEE Trans. Software Eng., vol. SE11, no. 1, pp, 8086, Jan. 1985.
[5] Reference Manual for the Ada Programming Language, U.S. Dep. Defense, Amer. Nat. Standards Inst., Rep. MILSTD1815A, Jan. 1983.
[6] N. Francez, D. Lehmann, and A. Pnueli, "A linear history semantics for distributed programming,"Trans. Comput. Syst., vol. 32, pp. 2546, 1984.
[7] C. A. R. Hoare, "Communicating sequential processes,"Commun. ACM, vol. 21, pp. 666677, 1978.
[8] C. A. R. Hoare, "A calculus of total correctness for communicating processes,"Sci. Comput. Program., vol. 1, pp. 4972, 1981.
[9] J. Hooman, "A compositional proofsystem for an occamlike realtime language," Eindhoven Univ. Technol., Tech. Rep. CSN 87/14, 1987.
[10] F. Jahanian and A. K. Mok, "A graphtheoretic approach for timing analysis and its implementation,"IEEE Trans. Comput., vol. 36, pp. 961975, Aug. 1987.
[11] R. Koymans, R. K. Shyamasundar, W. P. de Roever, R. Gerth, and S. ArunKumar, "Compositional semantics for realtime distributed computing," inProc. Logics of Programs (Lecture Notes Comput. Sci., vol. 193). New York: SpringerVerlag, 1985 (extended version appeared inInform. Computat., vol. 79, no. 3, pp. 201256, Dec. 1988).
[12] L. Y. Liu and R. K. Shyamasundar, "Temporal behaviors for realtime distributed systems," Pennsylvania State Univ., Tech. Rep. CS 8738, Dec. 1987.
[13] L. Y. Liu and R. K. Shyamasundar, "Exception handling in RTCDL," Pennsylvania State Univ., Tech. Rep, CS8921, Aug. 1989; alsoComput. Lang., to be published.
[14] L. Y. Liu and R. K. Shyamasundar, "RTCDL: 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 realtime distributed programs," Pennsylvania State Univ., Tech. Rep. CS8932, Oct. 1989.
[16] R. Milner,A Calculus of Communicating Systems (Lecture Notes in Computer Science 92). New York: SpringerVerlag, 1980.
[17] J. Misra and K. M. Chandy, "Proofs of networks of processes,"IEEE Trans. Software Eng., vol. SE7, no. 4, pp. 417426, July 1981.
[18] H. R. Nielson, "A Hoarelike proof system for analyzing the computation time of programs,"Sci. Comput. Program., vol. 9, no. 1, pp. 107136, Aug. 1987.
[19] J. S. Ostroff, "Realtime 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: PrenticeHall, 1981.
[21] A. Pnueli, "Specification and development of reactive systems," inInformation processing 86, H. J. Kugler, Ed., 1986, pp. 845858.
[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, SpringerVerlag, N.Y., 1986, pp. 510584.
[23] A. Pnueli and E. Harel, "Applications of temporal logic to the specification of realtime systems," inProc. Formal Techniques in RealTime and FaultTolerant Systems (LNCS 331), pp. 8498, 1988.
[24] A. Salwicki and T. Muldner,On the Algorithmic Properties of Concurrent Programs(Lecture Notes Comput. Sci., vol. 125). New York: SpringerVerlag, 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. 7283.
[26] R. K. Shyamasundar, J. Hooman, and R. Gerth, "Proof systems for realtime distributed programming," Pennsylvania State Univ., Tech. Rep. CS8719, June 1987.
[27] N. Soundararajan, "Axiomatic semantics of CSP," inProc. ACM TOPLAS, 1984, pp. 647662.
[28] R. N. Taylor, "A general purpose algorithm for analyzing concurrent programs,"Commun. ACM, vol. 26, no. 5, pp. 362376, May 1983.
[29] P. Wolper, "Temporal logic can be more expressive,"Inform. Contr., vol. 56, pp. 7299, 1983.
[30] A. Zwarico and I. Lee, "Proving a network of realtime processes correct," inProc. IEEE RealTime Systems Symp., 1985, pp. 169 177.