Abstract
This paper surveys some new tools and methods for formally verifying time performance properties of systems that satisfy timing assumptions. The techniques are potentially of practical benefit in the validation of real-time process control and communication systems. The tools and methods include nondeterministic timed automaton models, invariant assertion and simulation techniques for proving worst-case time bounds, probabilistic timed automaton models, and Markov-style techniques for proving probabilistic time bounds. All of these techniques are well suited for (partial) mechanization.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Download to read the full chapter text
Chapter PDF
References
Sudhanshu Aggarwal. Time optimal self-stabilizing spanning tree algorithms. Master’s thesis, MIT Electrical Engineering and Computer Science, May 1994.
Sudhanshu Aggarwal and Shay Kutten. Time optimal self stabilizing spanning tree algorithms. In R.K. Shyamasundar, editor, 13th International Conference on Foundations of Software Technology and Theoretical Computer Science, volume 761 of Lecture Notes in Computer Science, pages 400–410, Bombay, India., December 1993. Springer-Verlag.
Ernest Chang and Rosemary Roberts. An improved algorithm for decentralized extrema-finding in circular configurations of processes. Communications of the ACM, 22 (5): 281–283, May 1979.
E.W. Dijkstra. Solution of a problem in concurrent programming control. Communications of the ACM, 8 (9): 569, September 1965.
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.
C. L. Heitmeyer, R. D. Jeffords, and B. G. Labaw. A benchmark for comparing different approaches for specifying and verifying real-time systems. In Proc., Tenth Intern. Workshop on Real-Time Operating Systems and Software, May 1993.
Constance Heitmeyer and Nancy Lynch. The generalized railroad crossing: A case study in formal verification of real-time systems. In Proceedings of the 15th IEEE Real-Time Systems Symposium., San Juan, Puerto Rico, December 1994. To appear.
Constance Heitmeyer and Nancy Lynch. The generalized railroad crossing: A case study in formal verification of real-time systems. Technical Memo MIT/LCS/TM-511, Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MA, 1994. To appear.
G. LeLann. Distributed systems, towards a formal approach. In IFIP Congress, pages 155–160, Toronto, 1977.
Victor Luchangco. Using simulation techiniques to prove timing properties. Master’s thesis, MIT Electrical Engineering and Computer Science, 1994. In progress.
Victor Luchangco, Ekrem Söylemez, Stephen Garland, and Nancy Lynch. Verifying timing properties of concurrent algorithms. In Proceedings of the Seventh International Conference on Formal Description Techniques for Distributed Systems and Communications Protocols (FORTE’94), IFIP Transactions, Berne, Switzerland, October 1994. IFIP WG6.1, Elsevier Science Publishers B. V. (North Holland).
N. Lynch and M. Tuttle. An introduction to Input/Output automata. C WI-Quarterly, 2(3):219–246, September 1989. Centrum voor Wiskunde en Informatica, Amsterdam, The Netherlands.
Nancy Lynch. Simulation techniques for proving properties of real-time systems. In A Decade of Concurrency: Reflections and Perspectives, Lecture Notes in Computer Science, pages 375–424, REX School/Symposium, Noordwijkerhout, the Netherlands, June 1993. Springer-Verlag.
Nancy Lynch. Simulation techniques for proving properties of real-time systems. In Sang H. Son, editor, Principles of Real-Time Systems. Prentice Hall, 1994. To appear.
Nancy Lynch, Isaac Saias, and Roberto Segala. Proving time bounds for randomized distributed algorithms. In Thirteenth Annual ACM Symposium on the Principles of Distributed Computing, Los Angeles, CA, August 1994.
Nancy Lynch and Frits Vaandrager. Forward and backward simulations - Part II: Timing-based systems. Submitted for publication.
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.
Nancy A. Lynch and Hagit Attiya. Using mappings to prove timing properties. Distrib. Comput., 6: 121–139, 1992.
Michael Merritt, Francemary Modugno, and Mark R. Tuttle. Time constrained automata. In J. C. M. Baeten and J. F. Goote, editors, CONCUR’91: 2nd International Conference on Concurrency Theory, volume 527 of Lecture Notes in Computer Science, pages 408–423, Amsterdam, The Netherlands, August 1991. Springer-Verlag.
Roberto Segala. PhD thesis, MIT Dept. of Electrical Engineering and Computer Science, 1993. In progress.
Roberto Segala and Nancy Lynch. Probabilistic simulations for probabilistic processes. In Proceedings of the 5th International Conference on Concurrency Theory - CONCUR’94, Lecture Notes in Computer Science, Uppsala, Sweden, August 1994. Springer-Verlag.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1995 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Lynch, N. (1995). Proving Performance Properties (even Probabilistic Ones). In: Hogrefe, D., Leue, S. (eds) Formal Description Techniques VII. IFIP Advances in Information and Communication Technology. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-34878-0_1
Download citation
DOI: https://doi.org/10.1007/978-0-387-34878-0_1
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-5041-2881-0
Online ISBN: 978-0-387-34878-0
eBook Packages: Springer Book Archive