{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:35:30Z","timestamp":1761597330846},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540512851"},{"type":"electronic","value":"9783540461845"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1989]]},"DOI":"10.1007\/3-540-51285-3_56","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T15:52:00Z","timestamp":1330185120000},"page":"424-441","source":"Crossref","is-referenced-by-count":19,"title":["A temporal-logic based compositional proof system for real-time message passing"],"prefix":"10.1007","author":[{"given":"Jozef","family":"Hooman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jennifer","family":"Widom","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"28_CR1","unstructured":"The Programming Language Ada, Reference Manual. LNCS 155, Springer-Verlag, 1983."},{"key":"28_CR2","doi-asserted-by":"crossref","unstructured":"A. Bernstein and P.K. Harter, Jr. Proving real-time properties of programs with temporal logic. In Proc. of the 8th Symp. on Operating System Principles, pages 1\u201311, 1981.","DOI":"10.1145\/800216.806585"},{"key":"28_CR3","doi-asserted-by":"crossref","unstructured":"H. Barringer, R. Kuiper, and A. Pnueli. Now you may compose temporal logic specifications. In Proc. of the 16th Symp. on Theory of Computing, pages 51\u201363, 1984.","DOI":"10.1145\/800057.808665"},{"key":"28_CR4","unstructured":"Zhou Chao Chen and C.A.R. Hoare. Partial correctness of Communicating Sequential Processes. In Proc. of the IEEE International Conf. on Distributed Computing Systems, pages 1\u201312, 1981."},{"key":"28_CR5","doi-asserted-by":"crossref","unstructured":"C. Huizing, R. Gerth, and W.P. de Roever. Full abstraction of a real-time denotational semantics for an OCCAM-like language. In Proc. of the 14th POPL, pages 223\u2013237, 1987.","DOI":"10.1145\/41625.41645"},{"key":"28_CR6","volume-title":"A temporal logic for proving real-time properties of distributed programs","author":"K. Hay","year":"1988","unstructured":"K. Hay, S. Manchanda, and R. Schlichting. A temporal logic for proving real-time properties of distributed programs. Technical Report TR 88-40, Department of Computer Science, The University of Arizona, Tucson, Arizona, 1988."},{"issue":"8","key":"28_CR7","doi-asserted-by":"crossref","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"C.A.R. Hoare","year":"1978","unstructured":"C.A.R. Hoare. Communicating Sequential Processes. Comm. of the ACM, 21(8):666\u2013677, 1978.","journal-title":"Comm. of the ACM"},{"key":"28_CR8","doi-asserted-by":"crossref","unstructured":"J. Hooman. A compositional proof theory for real-time distributed message passing. In Parallel Architectures and Languages Europe, pages 315\u2013332. LNCS 259, Springer-Verlag, 1987.","DOI":"10.1007\/3-540-17945-3_18"},{"key":"28_CR9","volume-title":"A temporal-logic based compositional proof system for real-time message passing","author":"J. Hooman","year":"1989","unstructured":"J. Hooman and J. Widom. A temporal-logic based compositional proof system for real-time message passing. Technical report, Department of Mathematics and Computing Science, Eindhoven University of Technology, The Netherlands, 1989."},{"key":"28_CR10","doi-asserted-by":"crossref","unstructured":"R. Koymans and W.P. de Roever. Examples of a real-time temporal logic specification. In The Analysis of Concurrent Systems, pages 231\u2013252. LNCS 207, Springer-Verlag, 1983.","DOI":"10.1007\/3-540-16047-7_50"},{"key":"28_CR11","doi-asserted-by":"crossref","unstructured":"R. Koymans, R. Kuiper, and E. Zijlstra. Specifying real-time and message passing systems with real-time temporal logic. In Proc. of the 4th Esprit Conf., pages 311\u2013324, 1987.","DOI":"10.1145\/41840.41856"},{"issue":"3","key":"28_CR12","doi-asserted-by":"crossref","first-page":"210","DOI":"10.1016\/0890-5401(88)90020-X","volume":"79","author":"R. Koymans","year":"1988","unstructured":"R. Koymans, R.K. Shyamasundar, W.P. de Roever, R. Gerth, and S. Arun-Kumar. Compositional semantics for real-time distributed computing. Information and Computation, 79(3):210\u2013256, 1988.","journal-title":"Information and Computation"},{"key":"28_CR13","doi-asserted-by":"crossref","unstructured":"R. Koymans, J. Vytopyl, and W.P. de Roever. Real-time programming and asynchronous message passing. In Proc. of the 2nd PODC, pages 187\u2013197, 1983.","DOI":"10.1145\/800221.806721"},{"key":"28_CR14","unstructured":"Z. Manna and A. Pnueli. Verification of concurrent programs: a temporal proof system. In Foundations of Computer Science IV, Distributed Systems: Part 2, volume 159 of Mathematical Centre Tracts, pages 163\u2013255, 1982."},{"issue":"1","key":"28_CR15","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1007\/BF01843567","volume":"1","author":"V. Nguyen","year":"1986","unstructured":"V. Nguyen, A. Demers, D. Gries, and S. Owicki. A model and temporal proof system for networks of processes. Distributed Computing, 1(1):7\u201325, 1986.","journal-title":"Distributed Computing"},{"key":"28_CR16","unstructured":"INMOS Limited. OCCAM 2 Reference Manual, 1988."},{"issue":"3","key":"28_CR17","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1145\/357172.357178","volume":"4","author":"S. Owicki","year":"1982","unstructured":"S. Owicki and L. Lamport. Proving liveness poperties of concurrent programs. ACM Transactions on Programming Languages and Systems, 4(3):455\u2013495, 1982.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"28_CR18","doi-asserted-by":"crossref","unstructured":"A. Pnueli and E. Harel. Applications of temporal logic to the specification of real-time systems. In Formal Techniques in Real-Time and Fault-Tolerant Systems, pages 84\u201398. LNCS 331, 1988.","DOI":"10.1007\/3-540-50302-1_4"},{"key":"28_CR19","doi-asserted-by":"crossref","unstructured":"A. Pnueli. The temporal logic of programs. In Proc. of the 18th FOCS, pages 46\u201357, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"28_CR20","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/BF01667079","volume":"2","author":"A.U. Shankar","year":"1987","unstructured":"A.U. Shankar and S.S. Lam. Time-dependent distributed systems: proving safety, liveness and real-time properties. Distributed Computing, 2:61\u201379, 1987.","journal-title":"Distributed Computing"},{"key":"28_CR21","doi-asserted-by":"crossref","unstructured":"D.E. Shasha, A. Pnueli, and W. Ewald. Temporal verification of carrier-sense local area network protocols. In Proc. of the 11th POPL, pages 54\u201365, 1984.","DOI":"10.1145\/800017.800516"},{"key":"28_CR22","doi-asserted-by":"crossref","unstructured":"J. Widom, D. Gries, and F.B. Schneider. Completeness and incompleteness of trace-based network proof systems. In Proc. of the 14th POPL, pages 27\u201338, 1987.","DOI":"10.1145\/41625.41628"},{"key":"28_CR23","doi-asserted-by":"crossref","unstructured":"J. Zwiers, W.P. de Roever, and P. van Emde Boas. Compositionality and concurrent networks: soundness and completeness of a proofsystem. In Proc. of the 12th ICALP, pages 509\u2013519. LNCS 194, Springer-Verlag, 1985.","DOI":"10.1007\/BFb0015776"}],"container-title":["Lecture Notes in Computer Science","PARLE '89 Parallel Architectures and Languages Europe"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-51285-3_56.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T13:57:19Z","timestamp":1687269439000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-51285-3_56"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1989]]},"ISBN":["9783540512851","9783540461845"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-51285-3_56","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1989]]}}}