research-article

Static Analysis of Real-Time Distributed Systems

Authors:

Leo Yuhsiang Liu,

R. K. ShyamasundarAuthors Info & Claims

IEEE Transactions on Software Engineering, Volume 16, Issue 4

Pages 373 - 388

https://doi.org/10.1109/32.54290

Published: 01 April 1990 Publication History

Publisher Site

Abstract

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.

References

[1]

{1} A. V. Aho, R. Sethi, and J. D. Ullman, Compilers Principles, Techniques, and Tools. Reading, MA: Addison-Welsley, 1985.

Digital Library

Google Scholar

[2]

{2} K. R. Apt, A Static Analysis of CSP Programs (Lecture Notes Comput. Sci., vol. 164). New York: Springer-Verlag, 1984, pp. 1-17.

Digital Library

Google Scholar

[3]

{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.

Digital Library

Google Scholar

[4]

{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.

Digital Library

Google Scholar

[5]

{5} Reference Manual for the Ada Programming Language, U.S. Dep. Defense, Amer. Nat. Standards Inst., Rep. MIL-STD-1815A, Jan. 1983.

Google Scholar

[6]

{6} N. Francez, D. Lehmann, and A. Pnueli, "A linear-history semantics for languages for distributed programming," Theoretical Comput. Sci., vol. 32, pp. 25-47, 1984.

Digital Library

Google Scholar

[7]

{7} C. A. R. Hoare, "Communicating sequential processes," Commun. ACM, vol. 21, no. 8, pp. 666-677, Aug. 1978.

Digital Library

Google Scholar

[8]

{8} C. A. R. Hoare, "A calculus of total correctness for communicating processes," Sci. Comput. Program., vol. 1, pp. 49-72, 1981.

Crossref

Google Scholar

[9]

{9} J. Hooman, "A compositional proof-system for an occam-like real-time language," Eindhoven Univ. Technol., Tech. Rep. CSN 87/14, 1987.

Google Scholar

[10]

{10} F. Jahanian and A. K. Mok, "A graph-theoretic approach for timing analysis and its implementation," IEEE Trans. Comput., vol. C-36, pp. 961-974, Aug. 1987.

Digital Library

Google Scholar

[11]

{11} R. Koymans, R. K. Shyamasundar, W. P. de Roever, R. Gerth, and S. Arun-Kumar, "Compositional semantics for real-time distributed computing," in Proc. Logics of Programs (Lecture Notes Comput. Sci., vol. 193). New York: Springer-Verlag, 1985 (extended version appeared in Inform. Computat., vol. 79, no. 3, pp. 201-256, Dec. 1988).

Digital Library

Google Scholar

[12]

{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.

Google Scholar

[13]

{13} L. Y. Liu and R. K. Shyamasundar, "Exception handling in RT-CDL," Pennsylvania State Univ., Tech. Rep, CS-89-21, Aug. 1989; also Comput. Lang., to be published.

Google Scholar

[14]

{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.

Google Scholar

[15]

{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.

Google Scholar

[16]

{16} R. Milner, A Calculus of Communicating Systems (Lecture Notes Comput. Sci., vol. 92). New York: Springer-Verlag, 1980.

Digital Library

Google Scholar

[17]

{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.

Digital Library

Google Scholar

[18]

{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.

Digital Library

Google Scholar

[19]

{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.

Google Scholar

[20]

{20} J. L. Peterson, Petri Net Theory and the Modeling of Systems. Englewood Cliffs, NJ: Prentice-Hall, 1981.

Digital Library

Google Scholar

[21]

{21} A. Pnueli, "Specification and development of reactive systems," in Information processing 86, H. J. Kugler, Ed., 1986, pp. 845-858.

Google Scholar

[22]

{22} A. Pnueli, Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of Current Trends (Lecture Notes Comput. Sci., vol. 224). New York: Springer-Verlag, 1986, pp, 511-584.

Digital Library

Google Scholar

[23]

{23} A. Pnueli and E. Harel, "Applications of temporal logic to the specification of real time systems," in Proc. 1988 Symp. Formal Techniques in Real-Time and Fault-Tolerant Systems, Univ. Warwick, U.K. Sept. 1988, pp. 84-98.

Digital Library

Google Scholar

[24]

{24} A. Salwicki and T. Muldner, On the Algorithmic Properties of Concurrent Programs (Lecture Notes Comput. Sci., vol. 125). New York: Springer-Verlag, 1981.

Google Scholar

[25]

{25} R. K. Shyamasundar, K. T. Narayana, and T. Pitassi, "Semantics for nondeterministic asynchronous broadcast networks," in Proc. 14th Int. Colloquium Automata, Languages and Programming, Karlsruhe, July 1987, pp. 72-83.

Digital Library

Google Scholar

[26]

{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.

Google Scholar

[27]

{27} N. Soundararajan, "Axiomatic semantics of communicating sequentiat processes," ACM Trans. Program. Lang. Syst., vol. 6, pp. 647- 662, Oct. 1984.

Digital Library

Google Scholar

[28]

{28} R. N. Taylor, "A general-purpose algorithm for analyzing concurrent programs," Commun. ACM, vol. 26, pp. 362-376, May 1983.

Digital Library

Google Scholar

[29]

{29} P. Wolper, "Temporal logic can be more expressive," Inform. Contr., vol. 56, pp. 72-99, 1983.

Crossref

Google Scholar

[30]

{30} A. Zwarico and I. Lee, "Proving a network of real-time processes correct," in Proc. IEEE Real-Time Systems Symp., 1985, pp. 169- 177.

Google Scholar

Cited By

View all

Felder MPezzè M(2002)A formal design notation for real-time systemsACM Transactions on Software Engineering and Methodology10.1145/505145.50514611:2(149-190)Online publication date: 1-Apr-2002
https://dl.acm.org/doi/10.1145/505145.505146
Yen TWolf W(2001)Performance estimation for real-time distributed embedded systemsReadings in hardware/software co-design10.5555/567003.567019(195-206)Online publication date: 1-Jun-2001
https://dl.acm.org/doi/10.5555/567003.567019
Anand KShyamasundar R(2000)Formal Verification of Activity-Based Specification of ProtocolsJournal of Parallel and Distributed Computing10.1006/jpdc.2000.162260:5(639-676)Online publication date: 1-May-2000
https://dl.acm.org/doi/10.1006/jpdc.2000.1622
Show More Cited By

Index Terms

Recommendations

Constructing distributed real-time systems with DROL real-time objects
RTCSA '95: Proceedings of the 2nd International Workshop on Real-Time Computing Systems and Applications

In this paper, the semantics of inter-object communication protocols supported by the distributed real-time programming language DROL that is an extension of C++ based on the Distributed Real-time Object (DRO) model is described. A characteristic common ...
Testing of fault-tolerant and real-time distributed systems via protocol fault injection
FTCS '96: Proceedings of the The Twenty-Sixth Annual International Symposium on Fault-Tolerant Computing (FTCS '96)

As software for distributed systems becomes more complex, ensuring that a system meets its prescribed specification is a growing challenge that confronts software developers. This is particularly important for distributed applications with strict ...
Communicating Real-Time State Machines
Special issue: specification and analysis of real-time systems

Communicating real-time state machines (CRSMs), a complete and executable notation for specifying concurrent real-time systems including the monitored and controlled physical environment, are introduced. They are essentially state machines that ...

Reviews

Reviewer: Ramaswamy Ramanujam

CSP-R is CSP enriched with wait guards. This paper provides a simple static analysis of programs written in CSP-R. The authors study program behavior without using state information—in a sense, with uninterpreted atomic actions. The authors assume that each atomic action takes one unit of time, constituting one tick. The semantics uses sequences of sets of actions; each action set comprises actions that can be done concurrently. A maximal parallelism model is used, where processes wait only when they must. For each process, the possible sequences form a regular language. Parallel composition is implemented by a max-parallel merge, again giving a regular language. From this the authors obtain a finite state automaton for the whole program and use it to study properties such as termination, deadlock, and distributed termination. The result is intuitively clear and not surprising. The strength of the paper lies in its detailed examples. The example programs demonstrate various kinds of timed behavior. The specifications of a factory assembly-line system and a reactor system are quite interesting. This paper should interest researchers working on CSP-style specifications of reactive systems.

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image IEEE Transactions on Software Engineering

IEEE Transactions on Software Engineering Volume 16, Issue 4

April 1990

116 pages

ISSN:0098-5589

Editor:
Victor R. Basili
Univ. of Maryland, College Park

Issue’s Table of Contents

Publisher

IEEE Press

Publication History

Published: 01 April 1990

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 30 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Felder MPezzè M(2002)A formal design notation for real-time systemsACM Transactions on Software Engineering and Methodology10.1145/505145.50514611:2(149-190)Online publication date: 1-Apr-2002
https://dl.acm.org/doi/10.1145/505145.505146
Yen TWolf W(2001)Performance estimation for real-time distributed embedded systemsReadings in hardware/software co-design10.5555/567003.567019(195-206)Online publication date: 1-Jun-2001
https://dl.acm.org/doi/10.5555/567003.567019
Anand KShyamasundar R(2000)Formal Verification of Activity-Based Specification of ProtocolsJournal of Parallel and Distributed Computing10.1006/jpdc.2000.162260:5(639-676)Online publication date: 1-May-2000
https://dl.acm.org/doi/10.1006/jpdc.2000.1622
Yen TWolf W(1998)Performance Estimation for Real-Time Distributed Embedded SystemsIEEE Transactions on Parallel and Distributed Systems10.1109/71.7359599:11(1125-1136)Online publication date: 1-Nov-1998
https://dl.acm.org/doi/10.1109/71.735959
Burns SHulgaard HAmon TBorriello G(1995)An Algorithm for Exact Bounds on the Time Separation of Events in Concurrent SystemsIEEE Transactions on Computers10.1109/12.47512644:11(1306-1317)Online publication date: 1-Nov-1995
https://dl.acm.org/doi/10.1109/12.475126
Liu LShyamasundar R(1994)RT-CDLComputer Languages10.1016/0096-0551(94)90011-620:1(1-23)Online publication date: 1-Mar-1994
https://dl.acm.org/doi/10.1016/0096-0551%2894%2990011-6
Kurki-Suonio R(1993)Stepwise Design of Real-Time SystemsIEEE Transactions on Software Engineering10.1109/32.21030719:1(56-69)Online publication date: 1-Jan-1993
https://dl.acm.org/doi/10.1109/32.210307
Kurki-Suonio RSystä KVain JFinance JGhezzi CRoman G(1991)Real-time specification and modeling with joint actionsProceedings of the 6th international workshop on Software specification and design10.5555/952786.952800(84-91)Online publication date: 25-Oct-1991
https://dl.acm.org/doi/10.5555/952786.952800
Smith R(1991)Quality assurance through direct implementation of analysis and design constructsACM SIGSOFT Software Engineering Notes10.1145/127099.12712816:3(93-94)Online publication date: 1-Jul-1991
https://dl.acm.org/doi/10.1145/127099.127128
Kurki-Suonio RMoriconi M(1991)Stepwise design of real-time systemsProceedings of the conference on Software for citical systems10.1145/125083.123063(120-131)Online publication date: 1-Sep-1991
https://dl.acm.org/doi/10.1145/125083.123063
Show More Cited By

Abstract

References

Cited By

Index Terms

Recommendations

Constructing distributed real-time systems with DROL real-time objects

Testing of fault-tolerant and real-time distributed systems via protocol fault injection

Communicating Real-Time State Machines

Reviews

Access critical reviews of Computing literature here

Comments

Information

Published In

Publisher

Publication History

Author Tags

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations