{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T12:37:31Z","timestamp":1649162251759},"reference-count":27,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[1994,6,1]],"date-time":"1994-06-01T00:00:00Z","timestamp":770428800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":6986,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[1994,6]]},"DOI":"10.1016\/0304-3975(94)90166-x","type":"journal-article","created":{"date-parts":[[2002,7,26]],"date-time":"2002-07-26T00:17:21Z","timestamp":1027642641000},"page":"99-125","source":"Crossref","is-referenced-by-count":7,"title":["A compositional framework for fault tolerance by specification transformation"],"prefix":"10.1016","volume":"128","author":[{"given":"Doron","family":"Peled","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mathai","family":"Joseph","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/0304-3975(94)90166-X_BIB1","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1109\/LICS.1988.5115","article-title":"The existence of refinement mappings","author":"Abadi","year":"1988","journal-title":"Proc. Ann. Symp. on Logic in Computer Science"},{"key":"10.1016\/0304-3975(94)90166-X_BIB2","doi-asserted-by":"crossref","first-page":"388","DOI":"10.1145\/5956.6000","article-title":"Correctness proofs of distributed termination algorithms","volume":"8","author":"Apt","year":"1986","journal-title":"ACM Trans. Programming Languages and Systems"},{"key":"10.1016\/0304-3975(94)90166-X_BIB3","first-page":"240","article-title":"A compositional approach to superimposition","author":"Boug\u00e9","year":"1988","journal-title":"Proc. 5th Ann. ACM Symp. on Principles of Programming Languages"},{"key":"10.1016\/0304-3975(94)90166-X_BIB4","doi-asserted-by":"crossref","first-page":"811","DOI":"10.1109\/TSE.1986.6312984","article-title":"Error recovery in asynchronous systems","volume":"SE-12","author":"Campbell","year":"1986","journal-title":"IEEE Trans. Software Engrg."},{"key":"10.1016\/0304-3975(94)90166-X_BIB5","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1145\/214451.214456","article-title":"Distributed snapshots: determining the global state of distributed systems","volume":"3","author":"Chandy","year":"1985","journal-title":"ACM Trans. on Computation Systems"},{"key":"10.1016\/0304-3975(94)90166-X_BIB6","series-title":"Parallel Program Design: A Foundation","author":"Chandy","year":"1989"},{"issue":"1","key":"10.1016\/0304-3975(94)90166-X_BIB7","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1109\/TSE.1985.231534","article-title":"A rigorous approach to fault tolerant programming","volume":"SE-11","author":"Cristian","year":"1985","journal-title":"IEEE Trans. Software Engrg."},{"key":"10.1016\/0304-3975(94)90166-X_BIB8","series-title":"Fairness","author":"Francez","year":"1986"},{"key":"10.1016\/0304-3975(94)90166-X_BIB9","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/BF00264598","article-title":"Proving and applying program transformations expressed with second order patterns","volume":"11","author":"Huet","year":"1978","journal-title":"Acta Inform"},{"key":"10.1016\/0304-3975(94)90166-X_BIB10","article-title":"Temporal proof methodologies for real-time systems","author":"Henzinger","year":"1991","journal-title":"Proc. ACM Symp. on Principles of Programming Languages"},{"key":"10.1016\/0304-3975(94)90166-X_BIB11","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF01786251","article-title":"Algebraic specification and proof of a distributed recovery algorithm","volume":"2","author":"Jifeng","year":"1987","journal-title":"Distributed Computing"},{"key":"10.1016\/0304-3975(94)90166-X_BIB12","first-page":"21","article-title":"Interleaving set temporal logic","volume":"75","author":"Katz","year":"1992","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0304-3975(94)90166-X_BIB13","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1109\/TSE.1987.232562","article-title":"Checkpointing and rollback-recovery for distributed systems","volume":"SE-13","author":"Koo","year":"1987","journal-title":"IEEE Trans. Software Engrg."},{"key":"10.1016\/0304-3975(94)90166-X_BIB14","series-title":"Ph.D. Thesis","article-title":"Fairness for non-interleaving concurrency","author":"Kwiatkowska","year":"1989"},{"key":"10.1016\/0304-3975(94)90166-X_BIB15","series-title":"Inform. Process. 83","first-page":"657","article-title":"What good is temporal logic","author":"Lamport","year":"1983"},{"key":"10.1016\/0304-3975(94)90166-X_BIB16","doi-asserted-by":"crossref","unstructured":"L. Lamport, Time, clocks and the ordering of events in a distributed system Comm. ACM 21, 558-565.","DOI":"10.1145\/359545.359563"},{"key":"10.1016\/0304-3975(94)90166-X_BIB17","series-title":"Res. Report SRC57","article-title":"A temporal logic of actions","author":"Lamport","year":"1990"},{"key":"10.1016\/0304-3975(94)90166-X_BIB18","series-title":"Real-time: Theory in Practice","first-page":"1","article-title":"An old-fashioned recipe for real-time","volume":"Vol. 600","author":"Lamport","year":"1992"},{"issue":"5","key":"10.1016\/0304-3975(94)90166-X_BIB19","doi-asserted-by":"crossref","first-page":"442","DOI":"10.1007\/BF01211393","article-title":"Transformations of programs for fault tolerance","volume":"4","author":"Liu","year":"1992","journal-title":"Formal Aspects of Computing"},{"key":"10.1016\/0304-3975(94)90166-X_BIB20","first-page":"141","article-title":"How to cook a temporal proof system for your pet language","author":"Manna","year":"1983","journal-title":"Proc. ACM Symp. on Principles on Programming Languages"},{"key":"10.1016\/0304-3975(94)90166-X_BIB21","series-title":"Linear Time, Branching Time and Partial Orders in Logics and Models","first-page":"201","article-title":"The anchored version of the temporal framework","volume":"Vol. 254","author":"Manna","year":"1988"},{"key":"10.1016\/0304-3975(94)90166-X_BIB22","series-title":"Proc. of Advances in Petri Nets 1968","first-page":"279","article-title":"Trace semantics","volume":"Vol. 255","author":"Mazurkiewicz","year":"1987"},{"key":"10.1016\/0304-3975(94)90166-X_BIB23","series-title":"Proc. CONCUR 92","first-page":"192","article-title":"Sometimes \u2018some\u2019 is as good as \u2018all\u2019","volume":"Vol. 630","author":"Peled","year":"1992"},{"key":"10.1016\/0304-3975(94)90166-X_BIB24","first-page":"232","article-title":"Specifying and proving serializability in temporal logic","author":"Peled","year":"1991","journal-title":"Proc. Ann. Symp. on Logic in Computer Science"},{"key":"10.1016\/0304-3975(94)90166-X_BIB25","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/BF01843570","article-title":"Verification of multiprocess probabilistic protocols","volume":"1","author":"Pnueli","year":"1986","journal-title":"Distributed Computing"},{"key":"10.1016\/0304-3975(94)90166-X_BIB26","doi-asserted-by":"crossref","first-page":"222","DOI":"10.1145\/357369.357371","article-title":"Fail-stop processors: an approach to designing fault tolerant computing systems","volume":"1","author":"Schlichting","year":"1983","journal-title":"ACM Trans. Computer Systems"},{"key":"10.1016\/0304-3975(94)90166-X_BIB27","article-title":"Compositionality, Concurrency and Partial Correctness","volume":"Vol. 321","author":"Zwiers","year":"1987"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:030439759490166X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:030439759490166X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,2,5]],"date-time":"2020-02-05T09:17:48Z","timestamp":1580894268000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/030439759490166X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,6]]},"references-count":27,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[1994,6]]}},"alternative-id":["030439759490166X"],"URL":"https:\/\/doi.org\/10.1016\/0304-3975(94)90166-x","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[1994,6]]}}}