Abstract
The method of simulations is an important technique for reasoning about real-time and other timing-based systems. It is adapted from an analogous method for untimed systems. This paper presents the simulation method in the context of a very general automaton (i.e., labelled transition system) model for timing-based systems. Sketches are presented of several typical examples for which the method has been used successfully. Other complementary tools are also described, in particular, invariants for safety proofs, progress functions for timing proofs, and execution correspondences for liveness proofs.
Preview
Unable to display preview. Download preview PDF.
References
M. Abadi and L. Lamport. An old-fashioned recipe for real time. In Proceedings of REX Workshop “Real-Time: Theory in Practice”, volume 600 of Lecture Notes in Computer Science, pages 1–27, Mook, The Netherlands, June 1991. Springer-Verlag.
Baruch Awerbuch. Complexity of network synchronization. J. ACM, 32(4):804–823, October 1985.
K. M. Chandy and J. Misra. Parallel program design: a foundation. Addison-Wesley, 1988.
E. Chang and R. Roberts. An improved algorithm for decentralized extrema-finding in circular configurations of processes. Communications of the ACM, 22:281–283, May 1979.
Soma Chaudhuri, Rainer Gawlick, and Nancy Lynch. Designing algorithms for distributed systems with partially synchronized clocks. In Proceedings of the Twelve Annual ACM Symposium on the Principles of Distributed Computing, August 1993.
J. Davies and S. Schneider. An introduction to CSP, August 1989. Technical Monograph PRG-75.
Harish Devarajan. Correctness proof for a network synchronizer. Master's thesis, MIT Dept. of Electrical Engineering and Computer Science, May 1993.
E.W. Dijkstra. Solution of a problem in concurrent programming control. Communications of the ACM, 8(9):569, September 1965.
T. Elrad and N. Francez. Decomposition of distributed programs into communication-closed layers. Science of Computer Progamming, 2:155–173, 1982.
Michael Fischer. Re: Where are you? E-mail message to Leslie Lamport. Arpanet message number 8506252257.AA07636@YALE-BULLDOG.YALE.ARPA (47 lines), June 25, 1985 18:56:29EDT.
Stephen J. Garland and John V. Guttag. A guide to LP, the Larch Prover. Technical report, Digital Systems Research Center, 130 Lytton Avenue, Palo Alto, California 94301, December 1991. Research Report 82.
R. Gawlick, N. Lynch, R. Segala, and J. Søgaard-Andersen. Liveness in timed and untimed systems. In preparation, 1993.
C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.
Butler Lampson. Principles for computer system design, 1993. Turing Award Talk.
Butler Lampson, William Weihl, and Eric Brewer. 6.826 Principles of computer systems, Fall 1991. MIT/LCS/RSS 19, Massachusetts Institute of Technology, 1992. Lecture notes and Handouts.
G. LeLann. Distributed systems, towards a formal approach. In IFIP Congress, pages 155–160, Toronto, 1977.
B. Liskov, Luiba Shrira, and John Wroclawski. Efficient at-most-once messages based on synchronized clocks. Technical Report MIT/LCS/TR-476, Laboratory for Computer Science, Massachusetts Institute of Technology, April 1990.
Victor Luchangco. Using simulation techiniques to prove timing properties. Master's thesis, MIT Electrical Engineering and Computer Science, 1993. In progress.
N. Lynch. Multivalued possibilities mappings. In Rex Workshop, Volume 430 of Lecture Notes in Computer Science, Mook, The Netherlands, May 1989. Springer-Verlag. Also, MIT/LCS/TM-422.
N. Lynch and H. Attiya. Using mappings to prove timing properties. Distrib. Comput., 6(2):121–139, 1992.
N. Lynch, M. Merritt, W. Weihl, and A. Fekete. Atomic Transactions. Morgan Kaufmann Publishers, 1994.
N. Lynch and B. Patt-Shamir. Distributed algorithms. MIT/LCS/RSS 20, Massachusetts Institute of Technology, 1992. Lecture notes for 6.852.
N. Lynch and M. Tuttle. Hierarchical correctness proofs for distributed algorithms. Master's thesis, MIT Dept. of Electrical Engineering and Computer Science, April, 1987. Also, MIT/LCS/TR-387.
N. Lynch and M. Tuttle. An introduction to Input/Output automata. CWI-Quarterly, 2(3):219–246, September 1989. Also, MIT/LCS/TM-373.
N.A. Lynch and F.W. Vaandrager. Forward and backward simulations — Part I: Untimed systems. Submitted for publication. Also, MIT/LCS/TM-486.
N.A. Lynch and F.W. Vaandrager. Forward and backward simulations — Part II: Timing-based systems. Submitted for publication. Also, MIT/LCS/TM-487.
Nancy Lynch and Frits Vaandrager. Forward and backward simulations for timing-based systems. In Proceedings of REX Workshop “Real-Time: Theory in Practice”, volume 600 of Lecture Notes in Computer Science, pages 397–446, Mook, The Netherlands, June 1991. Springer-Verlag. Also, MIT/LCS/TM-458.
O. Maler, Z. Manna, and A. Pnueli. From timed to hybrid systems. In Proceedings of REX Workshop “Real-Time: Theory in Practice”, volume 600 of Lecture Notes in Computer Science, pages 447–484, Mook, The Netherlands, June 1991. Springer-Verlag.
M. Merritt, F. Modugno and M. Tuttle. Time constrained automata. In CONCUR'91 Proceedings Workshop on Theories of Concurrency: Unification and Extension, Amsterdam, August 1991.
Gil Neiger and Sam Toueg. Simulating synchronized clocks and common knowledge in distributed systems. J. ACM, 40(2):334–367, April 1993.
X. Nicollin and J. Sifakis. The algebra of timed processes ATP: Theory and application, November 1991. Technical Report RT-C26, LGI-IMAG (revised version).
Tobias Nipkow. Formal verification of data type refinement. In Proceedings of REX Workshop “Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness”, volume 430 of Lecture Notes in Computer Science, pages 561–591, Mook, The Netherlands, June 1989. Springer-Verlag.
Radia Perlman. Interconnections: bridge and routers. Addison Wesley, 1992.
A. Pnueli, 1988. Personal Communication.
G.M. Reed and A.W. Roscoe. A timed model for communicating sequential processes. Theor. Comp. Sci., pages 249–261, 58 1988.
Jørgen Søgaard-Andersen. Reliable at-most-once message delivery protocols, a protocol verification example. PhD thesis in progress.
Jørgen Søgaard-Andersen, Stephen J. Garland, John V. Guttag, Nancy A. Lynch, and Anna Pogosyants. Computer-assisted simulation proofs. In Proceedings of the Conference on Computer-Aided Verification, Heraklion, Crete, Greece, June 1993.
Jørgen Søgaard-Andersen, Nancy A. Lynch, and Butler Lampson. Correctness of at-most-once message delivery protocols. In FORTE '93 — Sixth International Conference on Formal Description Techniques, pages 387–402, Boston, MA, October 1993.
Ekrem Soylemez. Automatic verification of the timing properties of MMT automata. Master's thesis, MIT Dept. of Electrical Engineering and Computer Science, 1993. In progress.
E.W. Stark. Foundations of a Theory of Specification for Distributed Systems. PhD thesis, Massachusetts Institute of Technology, Laboratory for Computer Science, Cambridge, MA 02139, August 1984. Also, MIT/LCS/TM-342.
F.W. Vaandrager and N.A. Lynch. Action transducers and timed automata. In Proceedings of CONCUR '92, 3rd International Conference on Concurrency Theory, Lecture Notes in Computer Science, Stony Brook, NY, August 1992. Springer Verlag.
J.L. Welch, L. Lamport, and N. Lynch. A lattice-structured proof technique applied to a minimum spanning tree algorithm. In Proceedings of the 7th Annual ACM Symposium on Principles of Distributed Computing, pages 28–43, Toronto, Canada, August 1988. Also, MIT/LCS/TM-361.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lynch, N. (1994). Simulation techniques for proving properties of real-time systems. In: de Bakker, J.W., de Roever, W.P., Rozenberg, G. (eds) A Decade of Concurrency Reflections and Perspectives. REX 1993. Lecture Notes in Computer Science, vol 803. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58043-3_24
Download citation
DOI: https://doi.org/10.1007/3-540-58043-3_24
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58043-0
Online ISBN: 978-3-540-48423-3
eBook Packages: Springer Book Archive