{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T00:17:20Z","timestamp":1760055440700,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":85,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319568409"},{"type":"electronic","value":"9783319568416"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-56841-6_2","type":"book-chapter","created":{"date-parts":[[2017,4,5]],"date-time":"2017-04-05T13:00:33Z","timestamp":1491397233000},"page":"16-50","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["UTP by Example: Designs"],"prefix":"10.1007","author":[{"given":"Jim","family":"Woodcock","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Simon","family":"Foster","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,4,6]]},"reference":[{"key":"2_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B Book - Assigning Programs to Meanings","author":"J-R Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B Book - Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Anderson, H., Ciobanu, G., Freitas, L.: UTP and temporal logic model checking. In: [11], pp. 22\u201341 (2008)","DOI":"10.1007\/978-3-642-14521-6_3"},{"key":"2_CR3","series-title":"Graduate Texts in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1674-2","volume-title":"Refinement Calculus: A Systematic Introduction","author":"R-J Back","year":"1998","unstructured":"Back, R.-J., Wright, J.: Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer, Heidelberg (1998)"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/3-540-47797-7_4","volume-title":"Algebraic and Coalgebraic Methods in the Mathematics of Program Construction","author":"R Backhouse","year":"2002","unstructured":"Backhouse, R.: Galois connections and fixed point calculus. In: Backhouse, R., Crole, R., Gibbons, J. (eds.) Algebraic and Coalgebraic Methods in the Mathematics of Program Construction. LNCS, vol. 2297, pp. 89\u2013150. Springer, Heidelberg (2002). doi:10.1007\/3-540-47797-7_4"},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-642-41071-0_3","volume-title":"Formal Methods: Foundations and Applications","author":"V Bandur","year":"2013","unstructured":"Bandur, V., Woodcock, J.: Unifying theories of logic and specification. In: Iyoda, J., Moura, L. (eds.) SBMF 2013. LNCS, vol. 8195, pp. 18\u201333. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-41071-0_3"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Banks, M.J., Jacob, J.L.: On modelling user observations in the UTP. In: [62], pp. 101\u2013119 (2010)","DOI":"10.1007\/978-3-642-16690-7_4"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Banks, M.J., Jacob, J.L.: Unifying theories of confidentiality. In: [62], pp. 120\u2013136 (2010)","DOI":"10.1007\/978-3-642-16690-7_5"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Beg, A., Butterfield, A.: Linking a state-rich process algebra to a state-free algebra to verify software\/hardware implementation. In: FIT, Proceedings of the 8th International Conference on Frontiers of Information Technology (2010)","DOI":"10.1145\/1943628.1943675"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Bresciani, R., Butterfield, A.: A probabilistic theory of designs based on distributions. In: [73], pp. 105\u2013123 (2012)","DOI":"10.1007\/978-3-642-35705-3_5"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Butterfield, A.: Saoith\u00edn: a theorem prover for UTP. In: [62], pp. 137\u2013156 (2010)","DOI":"10.1007\/978-3-642-16690-7_6"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14521-6","volume-title":"Unifying Theories of Programming","year":"2010","unstructured":"Butterfield, A. (ed.): UTP 2008. LNCS, vol. 5713. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-14521-6"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Butterfield, A.: The logic of U\n$$\\cdot $$ (TP)2. In: [73], pp. 124\u2013143 (2012)","DOI":"10.1007\/978-3-642-35705-3_6"},{"issue":"4","key":"2_CR13","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1016\/j.scico.2008.09.014","volume":"74","author":"A Butterfield","year":"2009","unstructured":"Butterfield, A., Freitas, L., Woodcock, J.: Mechanising a formal model of flash memory. Sci. Comput. Program. 74(4), 219\u2013237 (2009)","journal-title":"Sci. Comput. Program."},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/978-3-540-73210-5_5","volume-title":"Integrated Formal Methods","author":"A Butterfield","year":"2007","unstructured":"Butterfield, A., Sherif, A., Woodcock, J.: Slotted-circus. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 75\u201397. Springer, Heidelberg (2007). doi:10.1007\/978-3-540-73210-5_5"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Butterfield, A., Woodcock, J., Formalising flash memory: first steps. In: 12th International Conference on Engineering of Complex Computer Systems (ICECCS 2007), 10\u201314 July 2007, Auckland, New Zealand, pp. 251\u2013260. IEEE Computer Society (2007)","DOI":"10.1109\/ICECCS.2007.23"},{"key":"2_CR16","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). doi:10.1007\/11889229_6"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Cavalcanti, A., Gaudel, M.-C.: A note on traces refinement and the conf relation in the unifying theories of programming. In: [11], pp. 42\u201361 (2008)","DOI":"10.1007\/978-3-642-14521-6_4"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Cavalcanti, A., Gaudel, M.-C.: Specification coverage for testing in Circus. In: [62], pp. 1\u201345 (2010)","DOI":"10.1007\/978-3-642-16690-7_1"},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/978-3-642-39698-4_6","volume-title":"Theories of Programming and Formal Methods","author":"A Cavalcanti","year":"2013","unstructured":"Cavalcanti, A., Mota, A., Woodcock, J.: Simulink timed models for program verification. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 82\u201399. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-39698-4_6"},{"issue":"3","key":"2_CR20","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/s10270-005-0085-2","volume":"4","author":"A Cavalcanti","year":"2005","unstructured":"Cavalcanti, A., Sampaio, A., Woodcock, J.: Unifying classes and processes. Softw. Syst. Model. 4(3), 277\u2013296 (2005)","journal-title":"Softw. Syst. Model."},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-642-21437-0_20","volume-title":"FM 2011: Formal Methods","author":"A Cavalcanti","year":"2011","unstructured":"Cavalcanti, A., Wellings, A., Woodcock, J.: The safety-critical Java memory model: a formal account. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 246\u2013261. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-21437-0_20"},{"issue":"1","key":"2_CR22","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/s00165-012-0253-4","volume":"25","author":"A Cavalcanti","year":"2013","unstructured":"Cavalcanti, A., Wellings, A.J., Woodcock, J.: The safety-critical Java memory model formalised. Formal Asp. Comput. 25(1), 37\u201357 (2013)","journal-title":"Formal Asp. Comput."},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Cavalcanti, A., Wellings, A.J., Woodcock, J., Wei, K., Zeyda, F.: Safety-critical Java in circus. In: Wellings, A.J., Ravn, A.P. (eds.) The 9th International Workshop on Java Technologies for Real-time and Embedded Systems, JTRES 2011, York, 26\u201328 September 2011, pp. 20\u201329. ACM (2011)","DOI":"10.1145\/2043910.2043915"},{"issue":"2","key":"2_CR24","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/j.entcs.2005.04.024","volume":"137","author":"A Cavalcanti","year":"2005","unstructured":"Cavalcanti, A., Woodcock, J.: Angelic nondeterminism and unifying theories of programming. Electr. Notes Theor. Comput. Sci. 137(2), 45\u201366 (2005)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"3","key":"2_CR25","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/s00165-006-0001-8","volume":"18","author":"A Cavalcanti","year":"2006","unstructured":"Cavalcanti, A., Woodcock, J., Dunne, S.: Angelic nondeterminism in the unifying theories of programming. Formal Asp. Comput. 18(3), 288\u2013307 (2006)","journal-title":"Formal Asp. Comput."},{"issue":"5","key":"2_CR26","doi-asserted-by":"publisher","first-page":"614","DOI":"10.1007\/s11241-013-9182-4","volume":"49","author":"A Cavalcanti","year":"2013","unstructured":"Cavalcanti, A., Zeyda, F., Wellings, A.J., Woodcock, J., Wei, K.: Safety-critical Java programs from circus models. Real-Time Syst. 49(5), 614\u2013667 (2013)","journal-title":"Real-Time Syst."},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"Chen, X., Ye, N., Ding, W.: A formal approach to analyzing interference problems in aspect-oriented designs. In: [62], pp. 157\u2013171 (2010)","DOI":"10.1007\/978-3-642-16690-7_7"},{"key":"2_CR28","doi-asserted-by":"crossref","unstructured":"Chen, Y.: Programmable verifiers in imperative programming. In: [62], pp. 172\u2013187 (2010)","DOI":"10.1007\/978-3-642-16690-7_8"},{"key":"2_CR29","doi-asserted-by":"crossref","unstructured":"Deutsch, M., Henson, M.C.: A relational investigation of UTP designs and prescriptions. In: [34], pp. 101\u2013122 (2006)","DOI":"10.1007\/11768173_7"},{"issue":"8","key":"2_CR30","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"EW Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453\u2013457 (1975)","journal-title":"Commun. ACM"},{"key":"2_CR31","volume-title":"A Discipline of Programming","author":"EW Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Upper Saddle River (1976)"},{"key":"2_CR32","doi-asserted-by":"crossref","unstructured":"Dunne, S.: Conscriptions: a new relational model for sequential computations. In: [73], pp. 144\u2013163 (2012)","DOI":"10.1007\/978-3-642-35705-3_7"},{"key":"2_CR33","doi-asserted-by":"crossref","unstructured":"Dunne, S.E., Hayes, I.J., Galloway, A.J.: Reasoning about loops in total and general correctness. In: [11], pp. 62\u201381 (2008)","DOI":"10.1007\/978-3-642-14521-6_5"},{"key":"2_CR34","series-title":"Lecture Notes in Computer Science","volume-title":"Unifying Theories of Programming","year":"2006","unstructured":"Dunne, S., Stoddart, B. (eds.): UTP 2006. LNCS, vol. 4010. Springer, Heidelberg (2006)"},{"key":"2_CR35","doi-asserted-by":"crossref","unstructured":"Feliachi, A., Gaudel, M.-C., Wolff, B.: Unifying theories in Isabelle\/HOL. In: [62], pp. 188\u2013206 (2010)","DOI":"10.1007\/978-3-642-16690-7_9"},{"key":"2_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-319-14806-9_2","volume-title":"Unifying Theories of Programming","author":"S Foster","year":"2015","unstructured":"Foster, S., Zeyda, F., Woodcock, J.: Isabelle\/UTP: a mechanised theory engineering framework. In: Naumann, D. (ed.) UTP 2014. LNCS, vol. 8963, pp. 21\u201341. Springer, Heidelberg (2015). doi:10.1007\/978-3-319-14806-9_2"},{"key":"2_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-642-39721-9_3","volume-title":"Unifying Theories of Programming and Formal Engineering Methods","author":"S Foster","year":"2013","unstructured":"Foster, S., Woodcock, J.: Unifying theories of programming in Isabelle. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Unifying Theories of Programming and Formal Engineering Methods. LNCS, vol. 8050, pp. 109\u2013155. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-39721-9_3"},{"key":"2_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-319-46750-4_17","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2016","author":"S Foster","year":"2016","unstructured":"Foster, S., Zeyda, F., Woodcock, J.: Unifying heterogeneous state-spaces with lenses. In: Sampaio, A., Wang, F. (eds.) ICTAC 2016. LNCS, vol. 9965, pp. 295\u2013314. Springer, Heidelberg (2016). doi:10.1007\/978-3-319-46750-4_17"},{"key":"2_CR39","doi-asserted-by":"crossref","unstructured":"Guttmann, W.: Lazy UTP. In: [11], pp. 82\u2013101 (2008)","DOI":"10.1007\/978-3-642-14521-6_6"},{"key":"2_CR40","doi-asserted-by":"crossref","unstructured":"Guttmann, W.: Unifying recursion in partial, total and general correctness. In: [62], pp. 207\u2013225 (2010)","DOI":"10.1007\/978-3-642-16690-7_10"},{"key":"2_CR41","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":"W Harwood","year":"2008","unstructured":"Harwood, W., 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). doi:10.1007\/978-3-540-85762-4_10"},{"key":"2_CR42","doi-asserted-by":"crossref","unstructured":"Hayes, I.J.: Termination of real-time programs: definitely, definitely not, or maybe. In: [34], pp. 141\u2013154 (2006)","DOI":"10.1007\/11768173_9"},{"key":"2_CR43","doi-asserted-by":"crossref","unstructured":"Jifeng, H.: Transaction calculus. In: [11], pp. 2\u201321 (2008)","DOI":"10.1007\/978-3-642-14521-6_2"},{"key":"2_CR44","doi-asserted-by":"crossref","unstructured":"Jifeng, H.: A probabilistic BPEL-like language. In: [62], pp. 74\u2013100 (2010)","DOI":"10.1007\/978-3-642-16690-7_3"},{"key":"2_CR45","doi-asserted-by":"crossref","unstructured":"He, J., Hoare, T.: Csp is a retract of CCS. In: [34], pp. 38\u201362 (2006)","DOI":"10.1007\/11768173_3"},{"key":"2_CR46","doi-asserted-by":"crossref","unstructured":"He, J., Qin, S., Sherif, A.: Constructing property-oriented models for verification. In: [34], pp. 85\u2013100 (2006)","DOI":"10.1007\/11768173_6"},{"key":"2_CR47","doi-asserted-by":"crossref","unstructured":"He, J., Sanders, J.W.: Unifying probability. In: [34], pp. 173\u2013199 (2006)","DOI":"10.1007\/11768173_11"},{"key":"2_CR48","doi-asserted-by":"crossref","unstructured":"Hehner, E.: Retrospective and prospective for unifying theories of programming. In: [34], pp. 1\u201317 (2006)","DOI":"10.1007\/11768173_1"},{"issue":"8","key":"2_CR49","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/27651.27653","volume":"30","author":"CAR Hoare","year":"1987","unstructured":"Hoare, C.A.R., Hayes, I.J., Jifeng, H., Morgan, C., Roscoe, A.W., Sanders, J.W., S\u00f8rensen, I.H., Spivey, J.M., Sufrin, B.: Laws of programming. Commun. ACM 30(8), 672\u2013686 (1987)","journal-title":"Commun. ACM"},{"key":"2_CR50","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":"2_CR51","volume-title":"Systematic Software Development Using VDM","author":"CB Jones","year":"1986","unstructured":"Jones, C.B.: Systematic Software Development Using VDM. Prentice-Hall International, Upper Saddle River (1986)"},{"key":"2_CR52","doi-asserted-by":"crossref","unstructured":"McEwan, A.A., Woodcock, J.: Unifying theories of interrupts. In: [11], pp. 122\u2013141 (2008)","DOI":"10.1007\/978-3-642-14521-6_8"},{"key":"2_CR53","volume-title":"Programming from Specifications","author":"C Morgan","year":"1994","unstructured":"Morgan, C.: Programming from Specifications, 2nd edn. Prentice-Hall International, Upper Saddle River (1994)","edition":"2"},{"key":"2_CR54","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/0167-6423(87)90011-6","volume":"9","author":"JM Morris","year":"1987","unstructured":"Morris, J.M.: A theoretical basis for stepwise refinement and the programming calculus. Sci. Comput. Program. 9, 287\u2013306 (1987)","journal-title":"Sci. Comput. Program."},{"key":"2_CR55","doi-asserted-by":"crossref","unstructured":"Nuka, G., Woodcock, J.: Mechanising a unifying theory. In: [34], pp. 217\u2013235 (2006)","DOI":"10.1007\/11768173_13"},{"key":"2_CR56","doi-asserted-by":"crossref","unstructured":"Oliveira, M., Cavalcanti, A., Woodcock, J.: Unifying theories in ProofPower-Z. In: [34], pp. 123\u2013140 (2006)","DOI":"10.1007\/11768173_8"},{"key":"2_CR57","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/j.entcs.2006.08.047","volume":"187","author":"M Oliveira","year":"2007","unstructured":"Oliveira, M., Cavalcanti, A., Woodcock, J.: A denotational semantics for circus. Electr. Notes Theor. Comput. Sci. 187, 107\u2013123 (2007)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"1\u20132","key":"2_CR58","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s00165-007-0052-5","volume":"21","author":"M Oliveira","year":"2009","unstructured":"Oliveira, M., Cavalcanti, A., Woodcock, J.: A UTP semantics for circus. Formal Asp. Comput. 21(1\u20132), 3\u201332 (2009)","journal-title":"Formal Asp. Comput."},{"issue":"1","key":"2_CR59","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/s00165-007-0044-5","volume":"25","author":"M Oliveira","year":"2013","unstructured":"Oliveira, M., Cavalcanti, A., Woodcock, J.: Unifying theories in ProofPower-Z. Formal Asp. Comput. 25(1), 133\u2013158 (2013)","journal-title":"Formal Asp. Comput."},{"key":"2_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-540-76650-6_16","volume-title":"Formal Methods and Software Engineering","author":"JI Perna","year":"2007","unstructured":"Perna, J.I., Woodcock, J.: A denotational semantics for Handel-C hardware compilation. In: Butler, M., Hinchey, M.G., Larrondo-Petrie, M.M. (eds.) ICFEM 2007. LNCS, vol. 4789, pp. 266\u2013285. Springer, Heidelberg (2007). doi:10.1007\/978-3-540-76650-6_16"},{"key":"2_CR61","doi-asserted-by":"crossref","unstructured":"Perna, J.I., Woodcock, J.: UTP semantics for Handel-C. In: [11], pp. 142\u2013160 (2008)","DOI":"10.1007\/978-3-642-14521-6_9"},{"key":"2_CR62","series-title":"Lecture Notes in Computer Science","volume-title":"Unifying Theories of Programming","year":"2010","unstructured":"Qin, S. (ed.): UTP 2010. LNCS, vol. 6445. Springer, Heidelberg (2010)"},{"key":"2_CR63","doi-asserted-by":"crossref","unstructured":"Ribeiro, P., Cavalcanti, A.: Designs with angelic nondeterminism. In: Seventh International Symposium on Theoretical Aspects of Software Engineering, TASE 2013, 1\u20133 July 2013, Birmingham, pp. 71\u201378. IEEE (2013)","DOI":"10.1109\/TASE.2013.18"},{"key":"2_CR64","doi-asserted-by":"crossref","unstructured":"Santos, T., Cavalcanti, A., Sampaio, A.: Object-orientation in the UTP. In: [34], pp. 18\u201337 (2006)","DOI":"10.1007\/11768173_2"},{"issue":"2","key":"2_CR65","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/s00165-009-0119-6","volume":"22","author":"A Sherif","year":"2010","unstructured":"Sherif, A., Cavalcanti, A., He, J., Sampaio, A.: A process algebraic framework for specification and validation of real-time systems. Formal Asp. Comput. 22(2), 153\u2013191 (2010)","journal-title":"Formal Asp. Comput."},{"key":"2_CR66","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"613","DOI":"10.1007\/3-540-36103-0_62","volume-title":"Formal Methods and Software Engineering","author":"A Sherif","year":"2002","unstructured":"Sherif, A., Jifeng, H.: Towards a time model for Circus. In: George, C., Miao, H. (eds.) ICFEM 2002. LNCS, vol. 2495, pp. 613\u2013624. Springer, Heidelberg (2002). doi:10.1007\/3-540-36103-0_62"},{"key":"2_CR67","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/978-3-540-31862-0_34","volume-title":"Theoretical Aspects of Computing - ICTAC 2004","author":"A Sherif","year":"2005","unstructured":"Sherif, A., Jifeng, H., Cavalcanti, A., Sampaio, A.: A framework for specification and validation of real-time systems using circus actions. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 478\u2013493. Springer, Heidelberg (2005). doi:10.1007\/978-3-540-31862-0_34"},{"key":"2_CR68","doi-asserted-by":"crossref","unstructured":"Smith, M.A., Gibbons, J.: Unifying theories of locations. In: [11], pp. 161\u2013180 (2008)","DOI":"10.1007\/978-3-642-14521-6_10"},{"key":"2_CR69","doi-asserted-by":"crossref","unstructured":"Stoddart, B., Bell, P.: Probabilistic choice, reversibility, loops, and miracles. In: [62], pp. 253\u2013270 (2010)","DOI":"10.1007\/978-3-642-16690-7_13"},{"key":"2_CR70","doi-asserted-by":"crossref","unstructured":"Stoddart, B., Zeyda, F., Lynas, R.: A design-based model of reversible computation. In: [34], pp. 63\u201383 (2006)","DOI":"10.1007\/11768173_4"},{"key":"2_CR71","doi-asserted-by":"crossref","unstructured":"Wei, K., Woodcock, J., Cavalcanti, A.: Circus time with reactive designs. In: [73], pp. 68\u201387 (2012)","DOI":"10.1007\/978-3-642-35705-3_3"},{"key":"2_CR72","doi-asserted-by":"crossref","unstructured":"Weiglhofer, M., Aichernig, B.K.: Unifying input output conformance. In: [11], pp. 181\u2013201 (2008)","DOI":"10.1007\/978-3-642-14521-6_11"},{"key":"2_CR73","series-title":"Lecture Notes in Computer Science","volume-title":"Unifying Theories of Programming","year":"2013","unstructured":"Wolff, B., Gaudel, M.-C., Feliachi, A. (eds.): UTP 2012. LNCS, vol. 7681. Springer, Heidelberg (2013)"},{"key":"2_CR74","doi-asserted-by":"crossref","unstructured":"Woodcock, J.: The miracle of reactive programming. In: [11], pp. 202\u2013217 (2008)","DOI":"10.1007\/978-3-642-14521-6_12"},{"key":"2_CR75","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-319-06410-9_3","volume-title":"FM 2014: Formal Methods","author":"J Woodcock","year":"2014","unstructured":"Woodcock, J.: Engineering UToPiA. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 22\u201341. Springer, Heidelberg (2014). doi:10.1007\/978-3-319-06410-9_3"},{"key":"2_CR76","doi-asserted-by":"crossref","unstructured":"Woodcock, J., Bandur, V.: Unifying theories of undefinedness in UTP. In: [73], pp. 1\u201322 (2012)","DOI":"10.1007\/978-3-642-35705-3_1"},{"key":"2_CR77","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-540-24756-2_4","volume-title":"Integrated Formal Methods","author":"J Woodcock","year":"2004","unstructured":"Woodcock, J., Cavalcanti, A.: A tutorial introduction to designs in unifying theories of programming. In: Boiten, E.A., Derrick, J., Smith, G. (eds.) IFM 2004. LNCS, vol. 2999, pp. 40\u201366. Springer, Heidelberg (2004). doi:10.1007\/978-3-540-24756-2_4"},{"key":"2_CR78","doi-asserted-by":"crossref","unstructured":"Woodcock, J., Cavalcanti, A., Fitzgerald, J.S., Larsen, P.G., Miyazawa, A., Perry, S.: Features of CML: a formal modelling language for systems of systems. In: 7th International Conference on System of Systems Engineering, SoSE 2012, Genova, 16\u201319 July 2012, pp. 445\u2013450. IEEE (2012)","DOI":"10.1109\/SYSoSE.2012.6384144"},{"key":"2_CR79","doi-asserted-by":"crossref","unstructured":"Zeyda, F., Cavalcanti, A.: Encoding Circus programs in ProofPowerZ. In: [11], pp. 218\u2013237 (2008)","DOI":"10.1007\/978-3-642-14521-6_13"},{"key":"2_CR80","doi-asserted-by":"crossref","unstructured":"Zeyda, F., Cavalcanti, A.: Higher-order UTP for a theory of methods. In: [73], pp. 204\u2013223 (2012)","DOI":"10.1007\/978-3-642-35705-3_10"},{"key":"2_CR81","doi-asserted-by":"crossref","unstructured":"Zhan, N., Kang, E.Y., Liu, Z.: Component publications and compositions. In: [11], pp. 238\u2013257 (2008)","DOI":"10.1007\/978-3-642-14521-6_14"},{"key":"2_CR82","doi-asserted-by":"crossref","unstructured":"Zhu, H., He, J., Peng, X., Jin, N.: Denotational approach to an event-driven system-level language. In: [11], pp. 258\u2013278 (2008)","DOI":"10.1007\/978-3-642-14521-6_15"},{"key":"2_CR83","doi-asserted-by":"crossref","unstructured":"Zhu, H., Liu, P., He, J., Qin, S.: Mechanical approach to linking operational semantics and algebraic semantics for Verilog using Maude. In: [73], pp. 164\u2013185 (2012)","DOI":"10.1007\/978-3-642-35705-3_8"},{"key":"2_CR84","doi-asserted-by":"crossref","unstructured":"Zhu, H., Sanders, J.W., He, J., Qin, S.: Denotational semantics for a probabilistic timed shared-variable language. In: [73], pp. 224\u2013247 (2012)","DOI":"10.1007\/978-3-642-35705-3_11"},{"key":"2_CR85","doi-asserted-by":"crossref","unstructured":"Zhu, H., Yang, F., He, J.: Generating denotational semantics from algebraic semantics for event-driven system-level language. In: [62], pp. 286\u2013308 (2010)","DOI":"10.1007\/978-3-642-16690-7_15"}],"container-title":["Lecture Notes in Computer Science","Engineering Trustworthy Software Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-56841-6_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T05:23:33Z","timestamp":1759987413000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-56841-6_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319568409","9783319568416"],"references-count":85,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-56841-6_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"6 April 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SETSS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"School on Engineering Trustworthy Software Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Chongqing","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 March 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 April 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"setss2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}