{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T16:20:17Z","timestamp":1742401217485},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1992,9,1]],"date-time":"1992-09-01T00:00:00Z","timestamp":715305600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Distrib Comput"],"published-print":{"date-parts":[[1992,9]]},"DOI":"10.1007\/bf02252683","type":"journal-article","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T14:56:36Z","timestamp":1132671396000},"page":"121-139","source":"Crossref","is-referenced-by-count":32,"title":["Using mappings to prove timing properties"],"prefix":"10.1007","volume":"6","author":[{"given":"Nancy A.","family":"Lynch","sequence":"first","affiliation":[]},{"given":"Hagit","family":"Attiya","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"BF02252683_CR1","unstructured":"Abadi M, Lamport L: The existence of refinement mappings. DEC SRC Res Rep 29 (1988)"},{"key":"BF02252683_CR2","doi-asserted-by":"crossref","unstructured":"Abadi M, Lamport L: An old-fashioned recipe for real time. Proc. REX Workshop \u201cReal-Time: Theory in Practice\u201d. Mook, The Netherlands 1991","DOI":"10.1007\/BFb0031985"},{"key":"BF02252683_CR3","doi-asserted-by":"crossref","unstructured":"Alur R, Henzinger T: Real-time logics: complexity and expressiveness. Proc 5th IEEE Symp on Logic in Computer Science, pp 390\u2013401 (1990)","DOI":"10.21236\/ADA323441"},{"key":"BF02252683_CR4","doi-asserted-by":"crossref","unstructured":"Alur R, Courcoubetis C, Dill D: Model-checking for real-time systems. Proc 5th IEEE Symp on Logic in Computer Science, 1990","DOI":"10.1109\/LICS.1990.113766"},{"key":"BF02252683_CR5","doi-asserted-by":"crossref","unstructured":"Alur R, Dill D: Automata for modelling real-time systems. Proc ICALP '90, Lect Notes Comp Sci vol 443: Springer, Berlin Heidelberg New York, pp 322\u2013335","DOI":"10.1007\/BFb0032042"},{"key":"BF02252683_CR6","doi-asserted-by":"crossref","unstructured":"Attiya H, Lynch N: Time bounds of real-time process control in the presence of timing uncertainty. Proc 10th Real-Time Systems Symposium, pp 268\u2013284, December 1989. Expanded version available as Tech Rep MIT\/LCS\/TR-403, Laboratory for Computer Science, MIT, July 1989","DOI":"10.21236\/ADA213791"},{"issue":"5","key":"BF02252683_CR7","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1067627.806585","volume":"15","author":"A Bernstein","year":"1981","unstructured":"Bernstein A, Harter P Jr: Proving real-time properties of programs with temporal logic. Proc 8th Symp on Operating System Principles. Operating Syst Rev 15 (5):1\u201311 (1981)","journal-title":"Operating Syst Rev"},{"issue":"5","key":"BF02252683_CR8","doi-asserted-by":"crossref","first-page":"603","DOI":"10.1109\/TSE.1983.235261","volume":"9","author":"JE Coolahan","year":"1983","unstructured":"Coolahan JE, Roussopoulus SN: Timing requirements for time-driven systems using augmented Petri nets. IEEE Trans Software Eng SE-9 (5):603\u2013616 (1983)","journal-title":"IEEE Trans Software Eng SE"},{"key":"BF02252683_CR9","doi-asserted-by":"crossref","unstructured":"Gabrielian A, Franklin MW: State-based specification of complex real-time systems. Proc 9th IEEE Real-Time Systems Symp, pp 2\u201311 (1988)","DOI":"10.1109\/REAL.1988.51095"},{"issue":"5","key":"BF02252683_CR10","doi-asserted-by":"crossref","first-page":"494","DOI":"10.1109\/TSE.1981.231111","volume":"7","author":"VH Hasse","year":"1981","unstructured":"Hasse VH: Real-time behavior of programs. IEEE Trans Software Eng SE-7 (5):494\u2013501 (1981)","journal-title":"IEEE Trans Software Eng SE"},{"key":"BF02252683_CR11","doi-asserted-by":"crossref","unstructured":"Harel E, Lichtenstein O, Pnueli A: Explicit clock temporal logic. Proc 5th IEEE Symp on Logic in Computer Science, pp 402\u2013413 (1990)","DOI":"10.1109\/LICS.1990.113765"},{"key":"BF02252683_CR12","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Manna Z, Pnueli A: Temporal proof methodologies for real-time systems. Proc ACM Symp on Principles of Programming Languages, pp 353\u2013366 (1991)","DOI":"10.1145\/99583.99629"},{"key":"BF02252683_CR13","unstructured":"Hooman J: A compositional proof theory for real-time distributed message passing. TR 4-1-1(1), Department of Mathematics and Computer Science, Eindhoven University of Technology 1987"},{"issue":"8","key":"BF02252683_CR14","doi-asserted-by":"crossref","first-page":"961","DOI":"10.1109\/TC.1987.5009519","volume":"36","author":"F Jahanian","year":"1987","unstructured":"Jahanian F, Mok A: A graph-theoretic approach for timing analysis and its implementation. IEEE Trans Comput C-36 (8):961\u2013975 (1987)","journal-title":"IEEE Trans Comput C"},{"key":"BF02252683_CR15","unstructured":"Jahanian F, Stuart DA: A method for verifying properties of modechart specifications. Proc 9th IEEE Real-Time Systems Symp, pp 12\u201321 (1988)"},{"key":"BF02252683_CR16","doi-asserted-by":"crossref","unstructured":"Koymans R, Vytopil J, deRoever WP: Real-time programming and asynchronous message passing. Proc 2nd ACM Symp on Principles of Distrib Comput, pp 187\u2013197 (1983)","DOI":"10.1145\/800221.806721"},{"issue":"2","key":"BF02252683_CR17","doi-asserted-by":"crossref","first-page":"190","DOI":"10.1145\/69624.357207","volume":"5","author":"L Lamport","year":"1983","unstructured":"Lamport L: Specifying concurrent program modules. ACM Trans Program Lang Syst. 5 (2):190\u2013222 (1983)","journal-title":"ACM Trans Program Lang Syst."},{"key":"BF02252683_CR18","unstructured":"Lamport L, Abadi M: Refining and composing real-time specifications (in progress)"},{"key":"BF02252683_CR19","unstructured":"Lewis HR: Finite-state analysis of asynchronous circuits with bounded temporal uncertainty. Tech Rep TR-15-89, Aiken Computation Laboratory, Harvard University"},{"key":"BF02252683_CR20","unstructured":"Lynch N, Harvey A, Perlman R, Varghese G: An analysis of the OSI network layer link state packet distribution protocol (in progress)"},{"key":"BF02252683_CR21","first-page":"335","volume":"3","author":"N Lynch","year":"1986","unstructured":"Lynch N: Concurrency control for resilient nested transactions. Adv Comput Res 3:335\u2013373 (1986)","journal-title":"Adv Comput Res"},{"key":"BF02252683_CR22","doi-asserted-by":"crossref","unstructured":"Lynch N, Attiya H: Using mappings to prove timing properties. Technical Memo MIT\/LCS\/TM-412.b, Laboratory for Computer Science, MIT, March 1990","DOI":"10.21236\/ADA234404"},{"key":"BF02252683_CR23","doi-asserted-by":"crossref","unstructured":"Lynch N, Attiya H: Using mappings to prove timing properties. Proc of the 9th Annu ACM Symp on Principles of Distributed Computing, Quebec, Canada, pp 265\u2013280 (1990)","DOI":"10.1145\/93385.93428"},{"key":"BF02252683_CR24","unstructured":"Lynch N, Goldman K: Lecture notes for 6.852. MIT\/LCS\/RSS-5, Laboratory for Computer Science, MIT, 1989"},{"key":"BF02252683_CR25","doi-asserted-by":"crossref","unstructured":"Lynch N, Tuttle M: Hierarchical correctness proofs for distributed algorithms. Proc 7th ACM Symp on Principles of Distributed Computing, pp 137\u2013151 (1987). Expanded version available as Technical Report MIT\/LCS\/TR-387, Laboratory for Computer Science, MIT, April 1987","DOI":"10.1145\/41840.41852"},{"key":"BF02252683_CR26","unstructured":"Lynch N, Tuttle M: 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"},{"key":"BF02252683_CR27","doi-asserted-by":"crossref","unstructured":"Lynch N, Vaandrager F: Forward and backward simulations for timing-based systems. Proc REX Workshop \u201cReal-Time: Theory in Practice\u201d, Mook, The Netherlands 1991","DOI":"10.1007\/BFb0032002"},{"key":"BF02252683_CR28","unstructured":"Manna Z: Mathematical theory of computation. McGraw-Hill Comput Sci Ser. MacGraw-Hill 1974"},{"key":"BF02252683_CR29","doi-asserted-by":"crossref","unstructured":"Merritt M, Modugno F, Tuttle M: Time constrained automata. In: Baeten JCM, Groote JF (eds) Proc CONCUR 91. Amsterdam, Lect Notes Comput Sci vol 527, Springer, Berlin Heidelberg New York, pp 408\u2013423","DOI":"10.1007\/3-540-54430-5_103"},{"key":"BF02252683_CR30","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0304-3975(83)90114-7","volume":"25","author":"R Milner","year":"1983","unstructured":"Milner R: Calculi for synchrony and asynchrony. TCS 25, pp 267\u2013310 (1983)","journal-title":"TCS"},{"key":"BF02252683_CR31","unstructured":"Neumann PG, Lamport L: Highly dependable distributed systems. Tech Rep, SRI International, Contract Number DAEA18-81-G-0062, SRI Project 4180, June 1983"},{"issue":"2","key":"BF02252683_CR32","doi-asserted-by":"crossref","first-page":"170","DOI":"10.1109\/71.80145","volume":"1","author":"JS Ostroff","year":"1990","unstructured":"Ostroff JS: Deciding properties of timed transion models. IEEE Trans Paral Distrib Sys 1 (2):170\u2013183 (1990)","journal-title":"IEEE Trans Paral Distrib Sys"},{"key":"BF02252683_CR33","unstructured":"Ostroff JS: Survey of formal methods for the specification and design of real-time systems IEEE Press (to appear)"},{"key":"BF02252683_CR34","doi-asserted-by":"crossref","unstructured":"Ostroff JS, Wonham WM: A framework for real-time discrete event control. IEEE Trans Autom Control (1990)","DOI":"10.1109\/9.52290"},{"key":"BF02252683_CR35","doi-asserted-by":"crossref","unstructured":"Peterson G, Fischer M: Economical solutions for the critical section problem in a distributed system. Proc 9th ACM Symp on Theory of Computing, pp 91\u201397 (1977)","DOI":"10.1145\/800105.803398"},{"key":"BF02252683_CR36","unstructured":"Schneider FB: Real-time reliable systems project. Foundations of Real-Time Computing Research Initiative, ONR Kickoff Workshop, pp 28\u201332 (1988)"},{"key":"BF02252683_CR37","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/BF01667079","volume":"2","author":"AU Shankar","year":"1987","unstructured":"Shankar AU, Lam S: Time-dependent distributed systems: proving safety, liveness and timing properties. Distrib Comput 2:61\u201379 (1987)","journal-title":"Distrib Comput"},{"issue":"7","key":"BF02252683_CR38","doi-asserted-by":"crossref","first-page":"875","DOI":"10.1109\/32.29487","volume":"15","author":"AC Shaw","year":"1989","unstructured":"Shaw AC: Reasoning about time in higher-level language software. IEEE Trans Software Eng SE-15 (7):875\u2013889 (1989)","journal-title":"IEEE Trans Software Eng SE"},{"key":"BF02252683_CR39","first-page":"75","volume-title":"Proc 3rd Symp IFIP Working Group 7.3","author":"J Sifakis","year":"1977","unstructured":"Sifakis J: Petri nets for performance evaluation. Measuring, modeling and evaluating computer systems. In: Beilner H, Gelenbe E (eds) Proc 3rd Symp IFIP Working Group 7.3, Amsterdam, North-Holland 1977, pp 75\u201393"},{"issue":"3","key":"BF02252683_CR40","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1145\/71021.71024","volume":"23","author":"J Stankovic","year":"1989","unstructured":"Stankovic J, Ramamritham K: The SPRING Kernel: a new paradigm for real-time operating systems. ACM Operating Syst Rev 23 (3):54\u201371 (1989)","journal-title":"ACM Operating Syst Rev"},{"key":"BF02252683_CR41","doi-asserted-by":"crossref","unstructured":"Tel G: Assertional verification of a timer based protocol. Proc ICALP '88, Lect Notes Comput Sci vol 317, Springer, Berlin Hiedelberg New York, pp 600\u2013614","DOI":"10.1007\/3-540-19488-6_145"},{"key":"BF02252683_CR42","unstructured":"Zwarico A: Timed acceptance: an algebra of time dependent computing, Ph.D. Thesis, Department of Computer and Information Science, University of Pennsylvania 1988"}],"container-title":["Distributed Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF02252683.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF02252683\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF02252683","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,5]],"date-time":"2023-05-05T14:56:14Z","timestamp":1683298574000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF02252683"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,9]]},"references-count":42,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1992,9]]}},"alternative-id":["BF02252683"],"URL":"https:\/\/doi.org\/10.1007\/bf02252683","relation":{},"ISSN":["0178-2770","1432-0452"],"issn-type":[{"value":"0178-2770","type":"print"},{"value":"1432-0452","type":"electronic"}],"subject":[],"published":{"date-parts":[[1992,9]]}}}