{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T15:52:37Z","timestamp":1743090757805,"version":"3.40.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319174037"},{"type":"electronic","value":"9783319174044"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-17404-4_10","type":"book-chapter","created":{"date-parts":[[2015,4,16]],"date-time":"2015-04-16T08:45:59Z","timestamp":1429173959000},"page":"147-163","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Formal Semantics of Orc Based on TLA$$^+$$"],"prefix":"10.1007","author":[{"given":"Zhen","family":"You","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jinyun","family":"Xue","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Qimin","family":"Hu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yi","family":"Hong","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,4,17]]},"reference":[{"key":"10_CR1","unstructured":"Misra, J.: Structured Concurrent Programming (2013). http:\/\/www.cs.utexas.edu\/users\/misra\/temporaryFiles.dir\/Orc.pdf"},{"issue":"83","key":"10_CR2","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/s10270-006-0012-1","volume":"6","author":"J Misra","year":"2007","unstructured":"Misra, J., Cook, W.R.: Computation orchestration: a basis for wide-area computing. J. Softw. Syst. Model. 6(83), 83\u2013110 (2007)","journal-title":"J. Softw. Syst. Model."},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-02138-1_1","volume-title":"Formal Techniques for Distributed Systems","author":"D Kitchin","year":"2009","unstructured":"Kitchin, D., Quark, A., Cook, W., Misra, J.: The Orc programming language. In: Lee, D., Lopes, A., Poetzsch-Heffter, A. (eds.) FMOODS 2009. LNCS, vol. 5522, pp. 1\u201325. Springer, Heidelberg (2009)"},{"key":"10_CR4","unstructured":"Kitchin, D.: Orchestration and atomicity. Ph.D. dissertation, The University of Texas at Austin, August (2013)"},{"key":"10_CR5","unstructured":"Orc Language Project (2014). http:\/\/orc.csres.utexas.edu\/index.shtml"},{"key":"10_CR6","unstructured":"Jayadev, M.: Structured orchestration of data and computation. In: Keynotespeeach in 10th International Symposium on Formal Aspects of Component Software, 28\u201330 October 2013, Nanchang, China (2013). http:\/\/www.cs.utexas.edu\/users\/misra\/FACS.pdf"},{"key":"10_CR7","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-0335-6","volume-title":"Mathematical Logic for Computer Science","author":"M Ben-Ari","year":"2001","unstructured":"Ben-Ari, M.: Mathematical Logic for Computer Science, 2nd edn. Springer, New York (2001)","edition":"2"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on the Foundations of Computer Science, pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"issue":"2","key":"10_CR9","doi-asserted-by":"publisher","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":"10_CR10","unstructured":"Lamport, L.: The temporal logic of actions. Research report 79, digital equipment corporation, systems research center. To appear in transactions on programming language and systems (1991)"},{"key":"10_CR11","volume-title":"Specifying Systems: The TLA$$^+$$ Language and Tools for Hardware and Software Engineers","author":"L Lamport","year":"2003","unstructured":"Lamport, L.: Specifying Systems: The TLA$$^+$$ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Reading (2003)"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/3-540-58043-3_23","volume-title":"A Decade of Concurrency Reflections and Perspectives","author":"L Lamport","year":"1994","unstructured":"Lamport, L.: Verification and specification of concurrent programs. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) A Decade of Concurrency Reflections and Perspectives. LNCS, vol. 803, pp. 347\u2013374. Springer, Heidelberg (1994)"},{"key":"10_CR13","unstructured":"Jinyun, X.: An Abstract Programming Language Apla. Report of Jiangxi Normal University (2001)"},{"issue":"4","key":"10_CR14","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/BF02943151","volume":"12","author":"X Jinyun","year":"1997","unstructured":"Jinyun, X.: A unified approach for developing efficient algorithm of programs. J. Comput. Sci. Technol. 12(4), 314\u2013329 (1997)","journal-title":"J. Comput. Sci. Technol."},{"key":"10_CR15","unstructured":"Jinyun, X.: A practicable approach for formal development of algorithmic programs. In: Proceeding of the International Symposium on Future software Technology, Nanjing, China (1999)"},{"key":"10_CR16","unstructured":"Jinyun, X.: PAR method and its supporting platform. In: Proceeding of the 1st Asian Working Conference on Verified Software (AWCVS 2006), pp. 29\u201331 (2006)"},{"key":"10_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-540-88194-0_12","volume-title":"Formal Methods and Software Engineering","author":"Z Duan","year":"2008","unstructured":"Duan, Z., Tian, C.: A unified model checking approach with projection temporal logic. In: Liu, S., Araki, K. (eds.) ICFEM 2008. LNCS, vol. 5256, pp. 167\u2013186. Springer, Heidelberg (2008)"},{"issue":"1","key":"10_CR18","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/j.scico.2007.09.001","volume":"70","author":"Z Duan","year":"2008","unstructured":"Duan, Z., Yang, X., Koutny, M.: Framed temporal logic programming. Sci. Comput. Program. 70(1), 31\u201361 (2008)","journal-title":"Sci. Comput. Program."},{"key":"10_CR19","doi-asserted-by":"publisher","first-page":"1729","DOI":"10.1016\/j.tcs.2010.12.047","volume":"412","author":"C Tian","year":"2011","unstructured":"Tian, C., Duan, Z.: Expressiveness of propositional projection temporal logic with star. Theor. Comput. Sci. 412, 1729\u20131744 (2011)","journal-title":"Theor. Comput. Sci."},{"key":"10_CR20","unstructured":"Hoare, T., Menzel, G., Misra, J.: A tree semantics of an orchestration language. Lecture Notes for NATO summer school, Marktoberdorf (2004). http:\/\/orc.csres.utexas.edu\/papers\/Semantics.Orc.pdf"},{"key":"10_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"477","DOI":"10.1007\/11817949_32","volume-title":"CONCUR 2006\u2014Concurrency Theory","author":"DE Kitchin","year":"2006","unstructured":"Kitchin, D.E., Cook, W.R., Misra, J.: A language for task orchestration and its semantic properties. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 477\u2013491. Springer, Heidelberg (2006)"},{"key":"10_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-540-79230-7_11","volume-title":"Web Services and Formal Methods","author":"Sidney Rosario","year":"2008","unstructured":"Rosario, Sidney, Kitchin, David E., Benveniste, Albert, Cook, William, Haar, Stefan, Jard, Claude: Event structure semantics of Orc. In: Dumas, Marlon, Heckel, Reiko (eds.) WS-FM 2007. LNCS, vol. 4937, pp. 154\u2013168. Springer, Heidelberg (2008)"},{"issue":"2\u20133","key":"10_CR23","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1016\/j.tcs.2008.04.037","volume":"402","author":"I Wehrman","year":"2008","unstructured":"Wehrman, I., Kitchin, D., Cook, W.R., Misra, J.: Timed semantics of orc. Theor. Comput. Sci. 402(2\u20133), 234\u2013248 (2008)","journal-title":"Theor. Comput. Sci."},{"key":"10_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/978-3-642-14808-8_8","volume-title":"Theoretical Aspects of Computing\u2014ICTAC 2010","author":"Q Li","year":"2010","unstructured":"Li, Q., Zhu, H., He, J.: A denotational semantical model for orc language. In: Cavalcanti, A., Deharbe, D., Gaudel, M.-C., Woodcock, J. (eds.) ICTAC 2010. LNCS, vol. 6255, pp. 106\u2013120. Springer, Heidelberg (2010)"},{"key":"10_CR25","unstructured":"Orc Reference Manual v2.1.0 (2013). http:\/\/orc.csres.utexas.edu\/documentation\/html\/refmanual\/index.html"},{"key":"10_CR26","doi-asserted-by":"crossref","unstructured":"Dijkstra, E.W.: Hierarchical ordering of sequenial processes. In: Operating Systems Techniques. Academic Press, New York (1971)","DOI":"10.1007\/978-1-4757-3472-0_5"},{"key":"10_CR27","unstructured":"Try Orc! A example of Dining Philosophers (2014). http:\/\/orc.csres.utexas.edu\/tryorc.shtml#tryorc\/small-demos\/philosopher.orc"},{"key":"10_CR28","unstructured":"Slimani, Y., Dahoy, E.H.: Logic Abstract Modules: A new TLA-based model for Specifying and Verifying Concurrent Programs. Department Informatique, Faculte del Scineces de Tunis (1998). www.di.unipi.it\/brogi\/ResearchActivity\/COCL98\/Papers\/p6.ps"},{"key":"10_CR29","unstructured":"Palmer, R.L.: Formal anaysis for MPI-based high performance computing software. Doctoral Dissertation, The University of Utach (2007)"}],"container-title":["Lecture Notes in Computer Science","Structured Object-Oriented Formal Language and Method"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-17404-4_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T00:43:58Z","timestamp":1676940238000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-17404-4_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319174037","9783319174044"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-17404-4_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"17 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}