乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:01:07Z","timestamp":1725663667150},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540544302"},{"type":"electronic","value":"9783540383574"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3-540-54430-5_99","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T22:48:47Z","timestamp":1330210127000},"page":"346-360","source":"Crossref","is-referenced-by-count":27,"title":["Simulations between specifications of distributed systems"],"prefix":"10.1007","author":[{"given":"Bengt","family":"Jonsson","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,4]]},"reference":[{"key":"25_CR1","doi-asserted-by":"crossref","unstructured":"M. Abadi and L. Lamport. The existence of refinement mappings. In Proc. 3 rd IEEE Int. Symp. on Logic in Computer Science, Edinburgh, 1988.","DOI":"10.1109\/LICS.1988.5115"},{"issue":"4","key":"25_CR2","doi-asserted-by":"crossref","first-page":"513","DOI":"10.1145\/48022.48023","volume":"10","author":"R.J.R. Back","year":"1988","unstructured":"R.J.R. Back and R. Kurki-Suonio. Distributed cooperation with action systems. ACM Trans. on Programming Languages and Systems, 10(4):513\u2013554, Oct. 1988.","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"25_CR3","unstructured":"R.J.R. Back and K. Sere. Stepwise refinement of parallel algorithms. Technical Report A. 64, \u00c5bo Akademi, Dept. of Computer Science and Mathematics, 1988."},{"key":"25_CR4","doi-asserted-by":"crossref","unstructured":"K.M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"R. de Nicola and F.W. Vaandrager. Three logics for branching bisimulation. In Proc. 5 th IEEE Int. Symp. on Logic in Computer Science, pages 118\u2013129, 1990.","DOI":"10.1109\/LICS.1990.113739"},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"R. Gerth. Foundations of compositional program refinement \u2014 safety properties. Volume 430 of Lecture Notes in Computer Science, pages 777\u2013808. Springer Verlag, 1990.","DOI":"10.1007\/3-540-52559-9_87"},{"key":"25_CR7","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1016\/0020-0190(87)90224-9","volume":"25","author":"C.A.R. Hoare","year":"1987","unstructured":"C.A.R. Hoare, H. Jifeng, and J.W. Sanders. Prespecification in data refinement. Information Processing Letters, 25:71\u201376, 1987.","journal-title":"Information Processing Letters"},{"issue":"4","key":"25_CR8","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"C.A.R. Hoare","year":"1972","unstructured":"C.A.R. Hoare. Proof of correctness of data representation. Acta Informatica, 1(4):271\u2013281, 1972.","journal-title":"Acta Informatica"},{"key":"25_CR9","unstructured":"J.E. Hopcroft and J.D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979."},{"key":"25_CR10","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1007\/BF01887207","volume":"1","author":"H. Jifeng","year":"1989","unstructured":"H. Jifeng. Process simulation and refinement. Formal Aspects of Computing, 1:229\u2013241, 1989.","journal-title":"Formal Aspects of Computing"},{"key":"25_CR11","unstructured":"B. Jonsson. Compositional Verification of Distributed Systems. PhD thesis, Dept. of Computer Systems, Uppsala University, Sweden, Uppsala, Sweden, 1987. Available as report DoCS 87\/09."},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"B. Jonsson. Modular verification of asynchronous networks. In Proc. 6 th ACM Symp. on Principles of Distributed Computing, Vancouver, Canada, pages 152\u2013166, Vancouver, Canada, 1987. Extended Version as SICS Research Report R90010.","DOI":"10.1145\/41840.41853"},{"key":"25_CR13","doi-asserted-by":"crossref","unstructured":"B. Jonsson. On decomposing and refining specifications of distributed systems. Volume 430 of Lecture Notes in Computer Science, pages 361\u2013385. Springer Verlag, 1990.","DOI":"10.1007\/3-540-52559-9_71"},{"key":"25_CR14","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1007\/BF01788563","volume":"3","author":"M.B. Josephs","year":"1988","unstructured":"M.B. Josephs. A state-based approach to communicating processes. Distributed Computing, 3:9\u201318, 1988.","journal-title":"Distributed Computing"},{"key":"25_CR15","doi-asserted-by":"crossref","unstructured":"A. Kleinman, Y. Moscowitz, A. Pnueli, and E. Shapiro. Communication with directed logic variables. In Proc. 18 th ACM Symp. on Principles of Programming Languages, 1991.","DOI":"10.1145\/99583.99615"},{"key":"25_CR16","series-title":"Technical Report","volume-title":"Verifying safety properties using infinite-state automata","author":"N. Klarlund","year":"1989","unstructured":"N. Klarlund and F.B. Schneider. Verifying safety properties using infinite-state automata. Technical Report TR 89-1039, Cornell University, Ithaca, New York, 1989."},{"issue":"2","key":"25_CR17","doi-asserted-by":"crossref","first-page":"190","DOI":"10.1145\/69624.357207","volume":"5","author":"L. Lamport","year":"1983","unstructured":"L. Lamport. Specifying concurrent program modules. ACM Trans. on Programming Languages and Systems, 5(2):190\u2013222, 1983.","journal-title":"ACM Trans. on Programming Languages and Systems"},{"issue":"1","key":"25_CR18","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1145\/63238.63240","volume":"32","author":"L. Lamport","year":"1989","unstructured":"L. Lamport. A simple approach to specifying concurrent systems, Communications of the ACM, 32(1):32\u201345, Jan. 1989.","journal-title":"Communications of the ACM"},{"issue":"4","key":"25_CR19","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1109\/TSE.1984.5010246","volume":"SE-10","author":"S.S. Lam","year":"1984","unstructured":"S.S. Lam and A.U. Shankar. Protocol verfication via projections. IEEE Trans. on Software Engineering, SE-10(4):325\u2013342, July 1984.","journal-title":"IEEE Trans. on Software Engineering"},{"key":"25_CR20","doi-asserted-by":"crossref","first-page":"454","DOI":"10.1007\/3-540-52559-9_75","volume":"430","author":"S.S. Lam","year":"1990","unstructured":"S.S. Lam and A.U. Shankar. Refinement and projection of relational specifications. Volume 430 of Lecture Notes in Computer Science, pages 454\u2013486. Springer Verlag, 1990.","journal-title":"Lecture Notes in Computer Science"},{"key":"25_CR21","doi-asserted-by":"crossref","unstructured":"N.A. Lynch and M.R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proc. 6 th ACM Symp. on Principles of Distributed Computing, Vancouver, Canada, pages 137\u2013151, 1987.","DOI":"10.1145\/41840.41852"},{"key":"25_CR22","doi-asserted-by":"crossref","first-page":"544","DOI":"10.1007\/3-540-52559-9_78","volume":"430","author":"M. Merritt","year":"1990","unstructured":"M. Merritt. Completeness theorems for automata. Volume 430 of Lecture Notes in Computer Science, pages 544\u2013560. Springer Verlag, 1990.","journal-title":"Lecture Notes in Computer Science"},{"key":"25_CR23","unstructured":"R. Milner. An algebraic definition of simulation between programs. pages 481\u2013489. Also as Report No. CS-205, Computer Science Department, Stanford University."},{"key":"25_CR24","unstructured":"Z. Manna and A. Pnueli. The temporal framework for concurrent programs. In Boyer and Moore, editors, The Correctness Problem in Computer Science, pages 215\u2013274. Academic Press, 1981."},{"issue":"4","key":"25_CR25","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1016\/0167-6423(84)90003-0","volume":"4","author":"Z. Manna","year":"1984","unstructured":"Z. Manna and A. Pnueli. Adequate proof principles for invariance and liveness properties of concurrent programs. Science of Computer Programming, 4(4):257\u2013289, 1984.","journal-title":"Science of Computer Programming"},{"key":"25_CR26","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1007\/BFb0013024","volume":"354","author":"Z. Manna","year":"1989","unstructured":"Z. Manna and A. Pnueli. The anchored version of the temporal framework. In de Bakker, de Roever, and Rozenberg, editors, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, volume 354 of Lecture Notes in Computer Science, pages 201\u2013284. Springer Verlag, 1989.","journal-title":"Lecture Notes in Computer Science"},{"key":"25_CR27","doi-asserted-by":"crossref","first-page":"629","DOI":"10.1007\/BF00263649","volume":"22","author":"T. Nipkow","year":"1986","unstructured":"T. Nipkow. Non-deterministic data types. Acta Informatica, 22:629\u2013661, 1986.","journal-title":"Acta Informatica"},{"key":"25_CR28","unstructured":"F. Orava. Verifying safety and deadlock properties of networks of asynchronously communicating processes. In Proc. 9 th IFIP WG6.1 Symp. on Protocol Specification, Testing, and Verification, Twente, Holland, 1989."},{"key":"25_CR29","series-title":"Technical Report","volume-title":"A structural approach to operational semantics","author":"G. Plotkin","year":"1981","unstructured":"G. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Denmark, 1981."},{"key":"25_CR30","doi-asserted-by":"crossref","first-page":"510","DOI":"10.1007\/BFb0027047","volume":"224","author":"A. Pnueli","year":"1986","unstructured":"A. Pnueli. Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends. Volume 224 of Lecture Notes in Computer Science, pages 510\u2013584. Springer Verlag, 1986.","journal-title":"Lecture Notes in Computer Science"},{"key":"25_CR31","unstructured":"A.P. Sistla. On verifying that a concurrent program satisfies a non-deterministic specification. Technical Report TR 88-378.01.1, Computer and Intelligent Systems Lab. GTE Laboratories, May 1988."},{"issue":"4","key":"25_CR32","doi-asserted-by":"crossref","first-page":"331","DOI":"10.1145\/357377.357384","volume":"1","author":"A.U. Shankar","year":"1983","unstructured":"A.U. Shankar and S.S. Lam. An HDLC protocol specification and its verification using image protocols. ACM Transactions on Computer Systems, 1(4):331\u2013368, Nov. 1983.","journal-title":"ACM Transactions on Computer Systems"},{"key":"25_CR33","unstructured":"E.W. Stark. Foundations of a Theory of Specification for Distributed Systems. PhD thesis, Massachussetts Inst. of Technology, 1984. Available as Report No. MIT\/LCS\/TR-342."},{"key":"25_CR34","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0304-3975(86)90007-1","volume":"56","author":"E.W. Stark","year":"1988","unstructured":"E.W. Stark. Proving entailment between conceptual state specifications. Theoretical Computer Science, 56:135\u2013154, 1988.","journal-title":"Theoretical Computer Science"},{"key":"25_CR35","unstructured":"M.Y. Vardi. Verification of concurrent programs: The automata theoretic framework. In Proc. 2 nd IEEE Int. Symp. on Logic in Computer Science, 1987."},{"key":"25_CR36","unstructured":"J. Lundelius Welch, L. Lamport, and N. Lynch. A lattice-structured proof technique applied to a minimum spanning tree algorithm, July 1988."}],"container-title":["Lecture Notes in Computer Science","CONCUR '91"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-54430-5_99.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T03:47:56Z","timestamp":1640922476000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-54430-5_99"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540544302","9783540383574"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/3-540-54430-5_99","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}