{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,20]],"date-time":"2025-08-20T12:25:12Z","timestamp":1755692712778,"version":"3.40.3"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319251493"},{"type":"electronic","value":"9783319251509"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-25150-9_29","type":"book-chapter","created":{"date-parts":[[2015,9,25]],"date-time":"2015-09-25T07:42:36Z","timestamp":1443166956000},"page":"505-523","source":"Crossref","is-referenced-by-count":5,"title":["CSP and Kripke Structures"],"prefix":"10.1007","author":[{"given":"Ana","family":"Cavalcanti","sequence":"first","affiliation":[]},{"given":"Wen-ling","family":"Huang","sequence":"additional","affiliation":[]},{"given":"Jan","family":"Peleska","sequence":"additional","affiliation":[]},{"given":"Jim","family":"Woodcock","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,12,25]]},"reference":[{"key":"29_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-642-14521-6_3","volume-title":"Unifying Theories of Programming","author":"H Anderson","year":"2010","unstructured":"Anderson, H., Ciobanu, G., Freitas, L.: UTP and temporal logic model checking. In: Butterfield, A. (ed.) UTP 2008. LNCS, vol. 5713, pp. 22\u201341. Springer, Heidelberg (2010)"},{"issue":"4","key":"29_CR2","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1145\/48022.48023","volume":"10","author":"RJ Back","year":"1988","unstructured":"Back, R.J., Kurki-Suonio, R.: Distributed cooperation with action systems. ACM Trans. Program. Lang. Syst. 10(4), 513\u2013554 (1988)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"3","key":"29_CR3","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L Burdy","year":"2005","unstructured":"Burdy, L., et al.: An overview of JML tools and applications. STTT 7(3), 212\u2013232 (2005)","journal-title":"STTT"},{"issue":"2","key":"29_CR4","first-page":"153","volume":"23","author":"A Butterfield","year":"2011","unstructured":"Butterfield, A.: A denotational semantics for Handel-C. FACJ 23(2), 153\u2013170 (2011)","journal-title":"FACJ"},{"issue":"4","key":"29_CR5","first-page":"465","volume":"23","author":"ALC Cavalcanti","year":"2011","unstructured":"Cavalcanti, A.L.C., Clayton, P., O\u2019Halloran, C.: From control law diagrams to Ada via \n                      \n                        \n                      \n                      $${\\sf Circus}$$\n                    . FACJ 23(4), 465\u2013512 (2011)","journal-title":"FACJ"},{"key":"29_CR6","unstructured":"Cavalcanti, A.L.C., Huang, W.L., Peleska, J., Woodcock, J.C.P.: Unified Runtime Verification for CSP - Extended version. Technical report, University of York, Department of Computer Science, York, UK (2015). \n                      www.cs.york.ac.uk\/circus\/hijac\/publication.html"},{"key":"29_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/11889229_6","volume-title":"Refinement Techniques in Software Engineering","author":"A Cavalcanti","year":"2006","unstructured":"Cavalcanti, A., Woodcock, J.: A tutorial introduction to CSP in unifying theories of programming. In: Cavalcanti, A., Sampaio, A., Woodcock, J. (eds.) PSSE 2004. LNCS, vol. 3167, pp. 220\u2013268. Springer, Heidelberg (2006)"},{"key":"29_CR8","unstructured":"Cavalcanti, A.L.C., Zeyda, F., Wellings, A., Woodcock, J.C.P., Wei, K.: Safety-critical Java programs from \n                      \n                        \n                      \n                      $${\\sf Circus}$$\n                     models. RTS 49(5), 614\u2013667 (2013)"},{"key":"29_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-642-54862-8_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Gibson-Robinson","year":"2014","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3 \u2014 a modern refinement checker for CSP. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 187\u2013201. Springer, Heidelberg (2014)"},{"key":"29_CR10","doi-asserted-by":"crossref","unstructured":"Haddad, G., Hussain, F., Leavens, G.T.: The design of SafeJML, a specification language for SCJ with support for WCET specification. In: JTRES. ACM (2010)","DOI":"10.1145\/1850771.1850793"},{"key":"29_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-540-85762-4_10","volume-title":"Theoretical Aspects of Computing - ICTAC 2008","author":"WT Harwood","year":"2008","unstructured":"Harwood, W.T., Cavalcanti, A., Woodcock, J.: A theory of pointers for the UTP. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol. 5160, pp. 141\u2013155. Springer, Heidelberg (2008)"},{"key":"29_CR12","volume-title":"Unifying Theories of Programming","author":"CAR Hoare","year":"1998","unstructured":"Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice-Hall, Upper Saddle River (1998)"},{"key":"29_CR13","unstructured":"Huang, W.L., Peleska, J., Schulze, U.: Contract Support for Evolving SoS. Public Document D34.3, COMPASS (2014)"},{"key":"29_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/11561163_9","volume-title":"Formal Methods for Components and Objects","author":"Z Liu","year":"2005","unstructured":"Liu, Z., Jifeng, H., Li, X.: rCOS: refinement of component and object systems. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2004. LNCS, vol. 3657, pp. 183\u2013221. Springer, Heidelberg (2005)"},{"key":"29_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-642-41202-8_17","volume-title":"Formal Methods and Software Engineering","author":"A Miyazawa","year":"2013","unstructured":"Miyazawa, A., Lima, L., Cavalcanti, A.: Formal models of SysML blocks. In: Groves, L., Sun, J. (eds.) ICFEM 2013. LNCS, vol. 8144, pp. 249\u2013264. Springer, Heidelberg (2013)"},{"key":"29_CR16","doi-asserted-by":"crossref","unstructured":"Oliveira, M.V.M., Cavalcanti, A.L.C., Woodcock, J.C.P.: A UTP semantics for \n                      \n                        \n                      \n                      $${\\sf Circus}$$\n                    . FACJ 21(1\u20132), 3\u201332 (2009)","DOI":"10.1007\/s00165-007-0052-5"},{"key":"29_CR17","doi-asserted-by":"crossref","unstructured":"Peleska, J.: Translating testing theories for concurrent systems. In: Correct System Design, Essays Dedicated to Ernst-R\u00fcdiger Olderog on the Occasion of his 60th Birthday, LNCS. Springer (2015)","DOI":"10.1007\/978-3-319-23506-6_10"},{"volume-title":"A Classical Mind: Essays in Honour of C. A. R. Hoare","year":"1994","key":"29_CR18","unstructured":"Roscoe, A.W. (ed.): A Classical Mind: Essays in Honour of C. A. R. Hoare. Prentice Hall International (UK) Ltd., Hertfordshire (1994)"},{"key":"29_CR19","series-title":"Texts in Computer Science","volume-title":"Understanding Concurrent Systems","author":"AW Roscoe","year":"2011","unstructured":"Roscoe, A.W.: Understanding Concurrent Systems. Texts in Computer Science. Springer, London (2011)"},{"issue":"2","key":"29_CR20","first-page":"153","volume":"22","author":"A Sherif","year":"2010","unstructured":"Sherif, A., Cavalcanti, A.L.C., He, J., Sampaio, A.C.A.: A process algebraic framework for specification and validation of real-time systems. FACJ 22(2), 153\u2013191 (2010)","journal-title":"FACJ"},{"key":"29_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"627","DOI":"10.1007\/978-3-319-06410-9_42","volume-title":"FM 2014: Formal Methods","author":"F Zeyda","year":"2014","unstructured":"Zeyda, F., Santos, T., Cavalcanti, A., Sampaio, A.: A modular theory of object orientation in higher-order UTP. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 627\u2013642. Springer, Heidelberg (2014)"},{"issue":"1","key":"29_CR22","first-page":"133","volume":"27","author":"H Zhu","year":"2015","unstructured":"Zhu, H., He, J., Qin, S., Brooke, P.: Denotational semantics and its algebraic derivation for an event-driven system-level language. FACJ 27(1), 133\u2013166 (2015)","journal-title":"FACJ"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing - ICTAC 2015"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-25150-9_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T21:48:15Z","timestamp":1559252895000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-25150-9_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319251493","9783319251509"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-25150-9_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}