{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:10:02Z","timestamp":1762459802548,"version":"3.37.3"},"publisher-location":"Cham","reference-count":65,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030310370"},{"type":"electronic","value":"9783030310387"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","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":[[2019]]},"DOI":"10.1007\/978-3-030-31038-7_5","type":"book-chapter","created":{"date-parts":[[2019,9,22]],"date-time":"2019-09-22T19:03:06Z","timestamp":1569178986000},"page":"80-105","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Probabilistic Semantics for RoboChart"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7955-2702","authenticated-orcid":false,"given":"Jim","family":"Woodcock","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0831-1976","authenticated-orcid":false,"given":"Ana","family":"Cavalcanti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9889-9514","authenticated-orcid":false,"given":"Simon","family":"Foster","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4416-8123","authenticated-orcid":false,"given":"Alexandre","family":"Mota","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kangfeng","family":"Ye","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,9,23]]},"reference":[{"issue":"1","key":"5_CR1","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1008739929481","volume":"15","author":"R Alur","year":"1999","unstructured":"Alur, R., Henzinger, T.A.: Reactive modules. Formal Methods Syst. Des. 15(1), 7\u201348 (1999)","journal-title":"Formal Methods Syst. Des."},{"key":"5_CR2","unstructured":"Bousmalis, K.: Closing the simulation-to-reality gap for deep robotic learning (2019). Google AI Blog \n                      http:\/\/ai.googleblog.com\/2017\/10\/closing-simulation-to-reality-gap-for.html"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Brunner, S.G., Steinmetz, F., Belder, R., D\u00f6mel, A.: RAFCON: a graphical tool for engineering complex, robotic tasks. In: 2016 IEEE\/RSJ International Conference on Intelligent Robots and Systems, IROS 2016, Daejeon, South Korea, 9\u201314 October 2016, pp. 3283\u20133290 (2016)","DOI":"10.1109\/IROS.2016.7759506"},{"key":"5_CR4","unstructured":"Cavalcanti, A., Ribeiro, P., Miyazawa, A., Sampaio, A., Filho, M.C., Didier, A.: RoboSim: Reference Manual (2019). \n                      www.cs.york.ac.uk\/robostar\/robosim\/robosim-reference.pdf"},{"issue":"3","key":"5_CR5","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1016\/S1571-0661(05)80489-X","volume":"70","author":"A Cavalcanti","year":"2002","unstructured":"Cavalcanti, A., Sampaio, A., Woodcock, J.: Refinement of actions in Circus. Electr. Notes Theor. Comput. Sci. 70(3), 132\u2013162 (2002)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"5_CR6","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). \n                      https:\/\/doi.org\/10.1007\/11889229_6"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-642-34327-8_16","volume-title":"Simulation, Modeling, and Programming for Autonomous Robots","author":"S Dhouib","year":"2012","unstructured":"Dhouib, S., Kchir, S., Stinckwich, S., Ziadi, T., Ziane, M.: RobotML, a domain-specific language to design, simulate and deploy robotic applications. In: Noda, I., Ando, N., Brugali, D., Kuffner, J.J. (eds.) SIMPAR 2012. LNCS (LNAI), vol. 7628, pp. 149\u2013160. Springer, Heidelberg (2012). \n                      https:\/\/doi.org\/10.1007\/978-3-642-34327-8_16"},{"key":"5_CR8","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":"5_CR9","unstructured":"FDR: Failures-Divergences Refinement. \n                      www.cs.ox.ac.uk\/projects\/fdr\/"},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/978-3-030-03044-5_13","volume-title":"Formal Methods: Foundations and Applications","author":"MS Conserva Filho","year":"2018","unstructured":"Conserva Filho, M.S., Marinho, R., Mota, A., Woodcock, J.: Analysing RoboChart with probabilities. In: Massoni, T., Mousavi, M.R. (eds.) SBMF 2018. LNCS, vol. 11254, pp. 198\u2013214. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-030-03044-5_13"},{"issue":"6","key":"5_CR11","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1145\/358669.358692","volume":"24","author":"MA Fischler","year":"1981","unstructured":"Fischler, M.A., Bolles, R.C.: Random sample consensus: a paradigm for model fitting with applications to image analysis and automated cartography. Commun. ACM 24(6), 381\u2013395 (1981)","journal-title":"Commun. ACM"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Fitzgerald, J.S., Gamble, C., Larsen, P.G., Pierce, K., Woodcock, J.: Cyber-physical systems design: Formal foundations, methods and integrated tool chains. In: Gnesi, S., Plat, N. (eds.) 3rd IEEE\/ACM FME Workshop on Formal Methods in Software Engineering, FormaliSE 2015, Florence, 18 May 2015, pp. 40\u201346. IEEE Computer Society (2015)","DOI":"10.1109\/FormaliSE.2015.14"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-030-02146-7_7","volume-title":"Formal Aspects of Component Software","author":"S Foster","year":"2018","unstructured":"Foster, S., Baxter, J., Cavalcanti, A., Miyazawa, A., Woodcock, J.: Automating verification of state machines with reactive designs and Isabelle\/UTP. In: Bae, K., \u00d6lveczky, P.C. (eds.) FACS 2018. LNCS, vol. 11222, pp. 137\u2013155. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-030-02146-7_7"},{"key":"5_CR14","unstructured":"Foster, S., Cavalcanti, A., Canham, S., Woodcock, J., Zeyda, F.: Unifying theories of reactive design contracts. CoRR abs\/1712.10233 (2017). \n                      arxiv.org\/abs\/1712.10233"},{"key":"5_CR15","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/j.ipl.2018.02.017","volume":"135","author":"S Foster","year":"2018","unstructured":"Foster, S., Cavalcanti, A., Woodcock, J., Zeyda, F.: Unifying theories of time with generalised reactive processes. Inf. Process. Lett. 135, 47\u201352 (2018)","journal-title":"Inf. Process. Lett."},{"key":"5_CR16","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). \n                      https:\/\/doi.org\/10.1007\/978-3-642-39721-9_3"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-319-51046-0_3","volume-title":"Concurrency, Security, and Puzzles","author":"S Foster","year":"2017","unstructured":"Foster, S., Woodcock, J.: Towards verification of cyber-physical systems with UTP and Isabelle\/HOL. In: Gibson-Robinson, T., Hopcroft, P., Lazi\u0107, R. (eds.) Concurrency, Security, and Puzzles. LNCS, vol. 10160, pp. 39\u201364. Springer, Cham (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-51046-0_3"},{"key":"5_CR18","unstructured":"Foster, S., Zeyda, F., Nemouchi, Y., Ribeiro, P., Wolff, B.: Isabelle\/UTP: mechanised theory engineering for unifying theories of programming. Arch. Formal Proofs (2019)"},{"key":"5_CR19","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, Cham (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-319-14806-9_2"},{"key":"5_CR20","unstructured":"Goldsmith, M.: CSP: the best concurrent-system description language in the world\u2013probably! In: Communicating Process Architectures, pp. 227\u2013232 (2004)"},{"issue":"2","key":"5_CR21","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1016\/j.jlap.2009.07.002","volume":"79","author":"W Guttmann","year":"2010","unstructured":"Guttmann, W., M\u00f6ller, B.: Normal design algebra. J. Log. Algebr. Program. 79(2), 144\u2013173 (2010)","journal-title":"J. Log. Algebr. Program."},{"issue":"3","key":"5_CR22","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D Harel","year":"1987","unstructured":"Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8(3), 231\u2013274 (1987)","journal-title":"Sci. Comput. Program."},{"key":"5_CR23","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). \n                      https:\/\/doi.org\/10.1007\/978-3-540-85762-4_10"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-540-30482-1_17","volume-title":"Formal Methods and Software Engineering","author":"H Jifeng","year":"2004","unstructured":"Jifeng, H., Morgan, C., McIver, A.: Deriving probabilistic semantics via the \u2018Weakest Completion\u2019. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 131\u2013145. Springer, Heidelberg (2004). \n                      https:\/\/doi.org\/10.1007\/978-3-540-30482-1_17"},{"issue":"2","key":"5_CR25","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1145\/69610.357988","volume":"27","author":"ECR Hehner","year":"1984","unstructured":"Hehner, E.C.R.: Predicative programming, part I. Commun. ACM 27(2), 134\u2013143 (1984)","journal-title":"Commun. ACM"},{"issue":"2","key":"5_CR26","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1145\/69610.357990","volume":"27","author":"ECR Hehner","year":"1984","unstructured":"Hehner, E.C.R.: Predicative programming, part II. Commun. ACM 27(2), 144\u2013151 (1984)","journal-title":"Commun. ACM"},{"issue":"5","key":"5_CR27","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1007\/BF00288466","volume":"23","author":"ECR Hehner","year":"1986","unstructured":"Hehner, E.C.R., Gupta, L.E., Malton, A.J.: Predicative methodology. Acta Inf. 23(5), 487\u2013505 (1986)","journal-title":"Acta Inf."},{"issue":"6","key":"5_CR28","doi-asserted-by":"publisher","first-page":"1730","DOI":"10.1109\/TSMCC.2012.2218236","volume":"42","author":"JA Hilder","year":"2012","unstructured":"Hilder, J.A., et al.: Chemical detection using the receptor density algorithm. IEEE Trans. Syst. Man Cybern. Part C 42(6), 1730\u20131741 (2012)","journal-title":"IEEE Trans. Syst. Man Cybern. Part C"},{"key":"5_CR29","unstructured":"Hoare, C.A.R.: Programs are predicates. In: FGCS, pp. 211\u2013218 (1992)"},{"issue":"2","key":"5_CR30","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/0020-0190(87)90106-2","volume":"24","author":"CAR Hoare","year":"1987","unstructured":"Hoare, C.A.R., He, J.: The weakest prespecification. Inf. Process. Lett. 24(2), 127\u2013132 (1987)","journal-title":"Inf. Process. Lett."},{"key":"5_CR31","volume-title":"Unifying Theories of Programming","author":"CAR Hoare","year":"1998","unstructured":"Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall, Upper Saddle River (1998)"},{"key":"5_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"704","DOI":"10.1007\/3-540-59496-5_337","volume-title":"Advances in Artificial Life","author":"N Jakobi","year":"1995","unstructured":"Jakobi, N., Husbands, P., Harvey, I.: Noise and the reality gap: the use of simulation in evolutionary robotics. In: Mor\u00e1n, F., Moreno, A., Merelo, J.J., Chac\u00f3n, P. (eds.) ECAL 1995. LNCS, vol. 929, pp. 704\u2013720. Springer, Heidelberg (1995). \n                      https:\/\/doi.org\/10.1007\/3-540-59496-5_337"},{"key":"5_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/3-540-45739-9_21","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"DN Jansen","year":"2002","unstructured":"Jansen, D.N., Hermanns, H., Katoen, J.-P.: A probabilistic extension of UML statecharts. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 355\u2013374. Springer, Heidelberg (2002). \n                      https:\/\/doi.org\/10.1007\/3-540-45739-9_21"},{"key":"5_CR34","unstructured":"Jansen, D.: Extensions of Statecharts with probability, time, and stochastic timing. Ph.D. thesis, University of Twente (2003)"},{"key":"5_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-46029-2_13","volume-title":"Computer Performance Evaluation: Modelling Techniques and Tools","author":"MZ Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM: probabilistic symbolic model checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol. 2324, pp. 200\u2013204. Springer, Heidelberg (2002). \n                      https:\/\/doi.org\/10.1007\/3-540-46029-2_13"},{"key":"5_CR36","doi-asserted-by":"crossref","unstructured":"Larsen, P.G., et al.: Integrated tool chain for model-based design of cyber-physical systems: the INTO-CPS project. In: 2016 2nd International Workshop on Modelling, Analysis, and Control of Complex CPS, CPS Data 2016, Vienna, 11 April 2016, pp. 1\u20136. IEEE Computer Society (2016)","DOI":"10.1109\/CPSData.2016.7496424"},{"key":"5_CR37","volume-title":"Introduction to Embedded Systems: A Cyber-Physical Systems Approach","author":"EA Lee","year":"2016","unstructured":"Lee, E.A., Seshia, S.A.: Introduction to Embedded Systems: A Cyber-Physical Systems Approach, 2nd edn. The MIT Press, Cambridge (2016)","edition":"2"},{"key":"5_CR38","doi-asserted-by":"crossref","unstructured":"Liu, Y., Sun, J., Dong, J.S.: PAT 3: an extensible architecture for building multi-domain model checkers. In: Dohi, T., Cukic, B. (eds.) IEEE 22nd International Symposium on Software Reliability Engineering, ISSRE 2011, Hiroshima, 29 November\u20132 December 2011, pp. 190\u2013199. IEEE Computer Society (2011)","DOI":"10.1109\/ISSRE.2011.19"},{"key":"5_CR39","unstructured":"Miyazawa, A.: RoboTool: RoboChart Tool Manual. University of York (2018). \n                      http:\/\/tinyurl.com\/RoboTool-Manual"},{"key":"5_CR40","doi-asserted-by":"crossref","unstructured":"Miyazawa, A., Ribeiro, P., Li, W., Cavalcanti, A., Timmis, J.: Automatic property checking of robotic applications. In: 2017 IEEE\/RSJ International Conference on Intelligent Robots and Systems, IROS 2017, Vancouver, 24\u201328 September 2017, pp. 3869\u20133876 (2017)","DOI":"10.1109\/IROS.2017.8206238"},{"key":"5_CR41","doi-asserted-by":"publisher","first-page":"3097","DOI":"10.1007\/s10270-018-00710-z","volume":"18","author":"A Miyazawa","year":"2019","unstructured":"Miyazawa, A., Ribeiro, P., Li, W., Cavalcanti, A., Timmis, J., Woodcock, J.: RoboChart: modelling and verification of the functional behaviour of robotic applications. Softw. Syst. Model. 18, 3097\u20133149 (2019)","journal-title":"Softw. Syst. Model."},{"key":"5_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). \n                      https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"5_CR43","unstructured":"Nokovic, B., Sekerinski, E.: Verification and code generation for timed transitions in pCharts. In: Desai, B.C. (ed.) International C* Conference on Computer Science & Software Engineering, C3S2E 2014, Montreal, 3\u20135 August 2014, pp. 3:1\u20133:10. ACM (2014)"},{"key":"5_CR44","unstructured":"Object Management Group: OMG Unified Modeling Language (OMG UML), superstructure, version 2.4.1"},{"key":"5_CR45","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":"5_CR46","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."},{"key":"5_CR47","doi-asserted-by":"crossref","unstructured":"Pembeci, I., Nilsson, H., Hager, G.D.: Functional reactive robotics: an exercise in principled integration of domain-specific languages. In: Proceedings of the 4th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 6\u20138 October 2002, Pittsburgh (Affiliated with PLI 2002), pp. 168\u2013179 (2002)","DOI":"10.1145\/571157.571174"},{"key":"5_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-319-66845-1_2","volume-title":"Integrated Formal Methods","author":"P Ribeiro","year":"2017","unstructured":"Ribeiro, P., Miyazawa, A., Li, W., Cavalcanti, A., Timmis, J.: Modelling and verification of timed robotic controllers. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 18\u201333. Springer, Cham (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-66845-1_2"},{"key":"5_CR49","unstructured":"RoboCalc. \n                      www.cs.york.ac.uk\/circus\/RoboCalc"},{"key":"5_CR50","unstructured":"RoboCalc Project: The foraging robot example. University of York (2019). \n                      http:\/\/tinyurl.com\/y4h9aq2l"},{"issue":"2","key":"5_CR51","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/s00165-005-0065-x","volume":"17","author":"AW Roscoe","year":"2005","unstructured":"Roscoe, A.W.: On the expressive power of CSP refinement. Formal Asp. Comput. 17(2), 93\u2013112 (2005)","journal-title":"Formal Asp. Comput."},{"key":"5_CR52","series-title":"Texts in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-258-0","volume-title":"Understanding Concurrent Systems","author":"AW Roscoe","year":"2010","unstructured":"Roscoe, A.W.: Understanding Concurrent Systems. Texts in Computer Science. Springer, Heidelberg (2010). \n                      https:\/\/doi.org\/10.1007\/978-1-84882-258-0"},{"key":"5_CR53","volume-title":"The Z Notation: A Reference Manual","author":"J Spivey","year":"1989","unstructured":"Spivey, J.: The Z Notation: A Reference Manual, 2nd edn. Prentice-Hall, Upper Saddle River (1989)","edition":"2"},{"key":"5_CR54","unstructured":"V-REP: Virtual Robot Experimentation Platform, User Manual, Version 3.6.1. \n                      www.coppeliarobotics.com\/helpFiles\/en\/importExport.htm"},{"key":"5_CR55","doi-asserted-by":"publisher","first-page":"33","DOI":"10.3389\/frobt.2016.00033","volume":"3","author":"M W\u00e4chter","year":"2016","unstructured":"W\u00e4chter, M., Ottenhaus, S., Kr\u00f6hnert, M., Vahrenkamp, N., Asfour, T.: The ArmarX Statechart concept: graphical programming of robot behavior. Front. Robot. AI 3, 33 (2016)","journal-title":"Front. Robot. AI"},{"key":"5_CR56","unstructured":"Webots: Reference Manual, Rel. R2019a. \n                      www.cyberbotics.com\/doc\/reference\/"},{"key":"5_CR57","doi-asserted-by":"publisher","first-page":"3682","DOI":"10.1007\/978-0-387-30440-3_217","volume-title":"Encyclopedia of Complexity and Systems Science","author":"AFT Winfield","year":"2009","unstructured":"Winfield, A.F.T.: Foraging robots. In: Meyers, R.A. (ed.) Encyclopedia of Complexity and Systems Science, pp. 3682\u20133700. Springer, Heidelberg (2009). \n                      https:\/\/doi.org\/10.1007\/978-0-387-30440-3_217"},{"key":"5_CR58","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: formal semantics for CML. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 22\u201341. Springer, Cham (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-319-06410-9_3"},{"key":"5_CR59","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). \n                      https:\/\/doi.org\/10.1007\/978-3-540-24756-2_4"},{"key":"5_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-319-56841-6_2","volume-title":"Engineering Trustworthy Software Systems","author":"J Woodcock","year":"2017","unstructured":"Woodcock, J., Foster, S.: UTP by example: designs. In: Bowen, J.P., Liu, Z., Zhang, Z. (eds.) SETSS 2016. LNCS, vol. 10215, pp. 16\u201350. Springer, Cham (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-56841-6_2"},{"key":"5_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1007\/978-3-319-47166-2_26","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques","author":"J Woodcock","year":"2016","unstructured":"Woodcock, J., Foster, S., Butterfield, A.: Heterogeneous semantics and unifying theories. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 374\u2013394. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-47166-2_26"},{"key":"5_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/3-540-52513-0_18","volume-title":"VDM \u201990 VDM and Z \u2014 Formal Methods in Software Development","author":"JCP Woodcock","year":"1990","unstructured":"Woodcock, J.C.P., Morgan, C.: Refinement of state-based concurrent systems. In: Bj\u00f8rner, D., Hoare, C.A.R., Langmaack, H. (eds.) VDM 1990. LNCS, vol. 428, pp. 340\u2013351. Springer, Heidelberg (1990). \n                      https:\/\/doi.org\/10.1007\/3-540-52513-0_18"},{"issue":"4","key":"5_CR63","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1145\/158431.158438","volume":"2","author":"P Zave","year":"1993","unstructured":"Zave, P., Jackson, M.: Conjunction as composition. ACM Trans. Softw. Eng. Methodol. 2(4), 379\u2013411 (1993)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"5_CR64","doi-asserted-by":"crossref","unstructured":"Zhang, S.J., Liu, Y.: An automatic approach to model checking UML state machines. In: Fourth International Conference on Secure Software Integration and Reliability Improvement, SSIRI 2010, Singapore, 9\u201311 June 2010, pp. 1\u20136. IEEE Computer Society (2010)","DOI":"10.1109\/SSIRI-C.2010.11"},{"issue":"7","key":"5_CR65","doi-asserted-by":"publisher","first-page":"793","DOI":"10.4304\/jsw.5.7.793-800","volume":"5","author":"Y Zhao","year":"2010","unstructured":"Zhao, Y., Yang, Z., Xie, J., Liu, Q.: Quantitative analysis of system based on extended UML state diagrams and probabilistic model checking. JSW 5(7), 793\u2013800 (2010)","journal-title":"JSW"}],"container-title":["Lecture Notes in Computer Science","Unifying Theories of Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-31038-7_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,22]],"date-time":"2019-09-22T19:23:06Z","timestamp":1569180186000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-31038-7_5"}},"subtitle":["A Weakest Completion Approach"],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030310370","9783030310387"],"references-count":65,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-31038-7_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"23 September 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"UTP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Unifying Theories of Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Porto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 October 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"utp2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cs.york.ac.uk\/circus\/utp2019\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"100% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}