Using mappings to prove timing properties

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Using mappings to prove timing properties

Full text

Pdf (1.87 MB)

Source

Annual ACM Symposium on Principles of Distributed Computing archive
Proceedings of the ninth annual ACM symposium on Principles of distributed computing table of contents

Quebec City, Quebec, Canada

Pages: 265 - 280

Year of Publication: 1990

ISBN:0-89791-404-X

Authors

Nancy Lynch	Laboratory for Computer Science, MIT, Cambridge, MA
Hagit Attiya	Laboratory for Computer Science, MIT, Cambridge, MA

Sponsors

SIGOPS: ACM Special Interest Group on Operating Systems
SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 1, Downloads (12 Months): 20, Citation Count: 3

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/93385.93428 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	M. Abadi and L. Lamport, "The Existence of Refinement Mappings," DEC SRC Research Report 29, August 1988.
	2	H. Attiya and N. Lynch, "Time Bounds for Real- Time Process Control in the Presence of Timing Uncertainty," in proc. lOtla Real-Time Systems Symposium, pp. 268-284, December 1989. Expanded version available as Technical Report MIT/LCS/TR-403, Laboratory for Computer Science, MIT, July 1989.
	3	Arthur Bernstein , Paul K. Harter, Jr., Proving real-time properties of programs with temporal logic, Proceedings of the eighth ACM symposium on Operating systems principles, p.1-11, December 14-16, 1981, Pacific Grove, California, United States
	4	M. W. Franklin and A. Gabrielian, "A TrnnsformationM Method for Verifying Safety Properties in Real-Time Systems," in Proc. l Oth IEEE Real-Time Systems Syrup., pp. I12-123, December 1989. Also available as Technical Report, 89- 12, Tomson-CSF, Inc., July 1989.
	5	A. Gabrielian and M. W. Franklin, "State-Based Specification of Complex Real-Time Systems," in Proc. 9th IEEE Real-Time Systems Syrup., 1988, pp. 2-11.
	6	V. H. lJasse, "Real-time behavior of programs," IEEE Transactions on Software Engineering, Vol. SE-7, No. 5 (September 1981), pp. 494-501.
	7	J. Hooman, A Compositional Proof Theory for Real-Time Distributed Message Passing, Tit. 4- 1-1(1), Department of Mathematics and Computer Science, Eindhoven University of technology, March 1987.
	8	F. Jahanian , A. K.-L. Mok, A graph-theoretic approach for timing analysis and its implementation, IEEE Transactions on Computers, v.36 n.8, p.961-975, Aug. 1987 [doi>10.1109/TC.1987.5009519]
	9	F. Jahanian and D. A. Stuart, "A Method for Verifying Properties of Modechart Specifications," in Proc. 9th IEEE Real-Time Systems Syrup., 1988, pp. 12-21.
	10	Ron Koymans , Jan Vytopil , Willem P. de Roever, Real-time programming and asynchronous message passing, Proceedings of the second annual ACM symposium on Principles of distributed computing, p.187-197, August 17-19, 1983, Montreal, Quebec, Canada [doi>10.1145/800221.806721]
	11	Leslie Lamport, Specifying Concurrent Program Modules, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.2, p.190-222, April 1983 [doi>10.1145/69624.357207]
	12	H. R. Lewis, "Finite-State Analysis of Asynchronous Circuits with Bounded Temporal Uncertainty," Technical Report TR-15-89, Aiken Computation Laboratory, Harvard University.
	13	N. Lynch, "Concurrency Control for Resilient Nested transactions," Advances in Computing Research, Vol. 3, 1986, pp. 335-373.
	14	N. Lynch, "Modelling Real-Time Systems," in Foundations of Real-Time Computing Research Initiative, ONR Kickoff Workshop, November 1988, pp. 1-16.
	15	N. A. Lynch, Multivalued possibilities mappings, Proceedings on Stepwise refinement of distributed systems: models, formalisms, correctness, p.519-543, May 1990, Mook, The Netherlands
	16	N. Lynch and H. Attiya, "Using Mappings to Prove Timing Properties," Technical Memo MIT/LCS/TM-412.b, Laboratory for Computer Science, MIT, December 1989.
	17	N. Lynch and K. Goldman, Lecture notes for 6.852. MIT/LCS/RSS-5, Laboratory for Computer Science, MIT, 1989.
	18	Nancy A. Lynch , Mark R. Tuttle, Hierarchical correctness proofs for distributed algorithms, Proceedings of the sixth annual ACM Symposium on Principles of distributed computing, p.137-151, August 10-12, 1987, Vancouver, British Columbia, Canada [doi>10.1145/41840.41852]
	19	N. Lynch and M. Tuttle, "An Introduction to Input/Output Automata," CWI-Quarterly, Vol. 2, No. 3, 1989. Also: Technical Memo, MIT/LCS/TM-373, Laboratory for Computer Science Massachusetts Institute of Technology, November 1988.
	20	M. Merritt, Completeness theorems for automata, Proceedings on Stepwise refinement of distributed systems: models, formalisms, correctness, p.544-560, May 1990, Mook, The Netherlands
	21	M. Merritt, F. Modugno and M. Tuttle "Time Constrained Automata," manuscript, November 1988.
	22	Gary L. Peterson , Michael J. Fischer, Economical solutions for the critical section problem in a distributed system (Extended Abstract), Proceedings of the ninth annual ACM symposium on Theory of computing, p.91-97, May 04-04, 1977, Boulder, Colorado, United States [doi>10.1145/800105.803398]
	23	F. B. Schneider, "Real-Time Reliable Systems Project," in Foundations of Real-Time Computing Research Initiative, ONR Kickoff Workshop, November 1988, pp. 28-32.
	24	A. U. Shankar and S. Lam, "Time-Dependent Distributed Systems: Proving Safety, Liveness and Timing Properties," Distributed Computing, 2 (1987), pp. 61-79.
	25	A. C. Shaw, Reasoning About Time in Higher-Level Language Software, IEEE Transactions on Software Engineering, v.15 n.7, p.875-889, July 1989 [doi>10.1109/32.29487]
	26	J. A. Stankovic , K. Ramamritham, The Spring kernel: a new paradigm for real-time operating systems, ACM SIGOPS Operating Systems Review, v.23 n.3, p.54-71, July 1989 [doi>10.1145/71021.71024]
	27	Gerard Tel, Assertional Verification of a Timer Based Protocol, Proceedings of the 15th International Colloquium on Automata, Languages and Programming, p.600-614, July 11-15, 1988
	28	Amy E. Zwarico, Timed acceptances: an algebra of time-dependent computing, University of Pennsylvania, Philadelphia, PA, 1988

CITED BY 3

	Angelo Morzenti , Dino Mandrioli , Carlo Ghezzi, A model parametric real-time logic, ACM Transactions on Programming Languages and Systems (TOPLAS), v.14 n.4, p.521-573, Oct. 1992
	E. Jane Cameron , Yow-Jian Lin, A real-time transition model for analyzing behavioral compatibility of telecommunications services, ACM SIGSOFT Software Engineering Notes, v.16 n.5, p.101-111, Dec. 1991
	Nancy A. Lynch , Hagit Attiya, Using mappings to prove timing properties, Distributed Computing, v.6 n.2, p.121-139, September 1992