{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T12:08:31Z","timestamp":1762862911666,"version":"3.37.3"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319668444"},{"type":"electronic","value":"9783319668451"}],"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":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66845-1_2","type":"book-chapter","created":{"date-parts":[[2017,8,26]],"date-time":"2017-08-26T11:37:20Z","timestamp":1503747440000},"page":"18-33","source":"Crossref","is-referenced-by-count":9,"title":["Modelling and Verification of Timed Robotic Controllers"],"prefix":"10.1007","author":[{"given":"Pedro","family":"Ribeiro","sequence":"first","affiliation":[]},{"given":"Alvaro","family":"Miyazawa","sequence":"additional","affiliation":[]},{"given":"Wei","family":"Li","sequence":"additional","affiliation":[]},{"given":"Ana","family":"Cavalcanti","sequence":"additional","affiliation":[]},{"given":"Jon","family":"Timmis","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,27]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Chen, J., Gauci, M., Gross, R.: A strategy for transporting tall objects with a swarm of miniature mobile robots. In: 2013 IEEE International Conference on Robotics and Automation (ICRA), pp. 863\u2013869, May 2013","DOI":"10.1109\/ICRA.2013.6630674"},{"issue":"14","key":"2_CR2","doi-asserted-by":"crossref","first-page":"1743","DOI":"10.1177\/0278364910375139","volume":"29","author":"W Liu","year":"2010","unstructured":"Liu, W., Winfield, A.F.T.: Modeling and optimization of adaptive foraging in swarm robotic systems. Int. J. Robot. Res. 29(14), 1743\u20131760 (2010)","journal-title":"Int. J. Robot. Res."},{"key":"2_CR3","volume-title":"Distributed Autonomous Robotic Systems","author":"W Li","year":"2016","unstructured":"Li, W., Miyazawa, A., Ribeiro, P., Cavalcanti, A.L.C., Woodcock, J.C.P., Timmis, J.: From formalised state machines to implementation of robotic controllers. In: Chong, N.-Y., Cho, Y.-J. (eds.) DARS 2016. Springer, London (2016)"},{"key":"2_CR4","series-title":"Worldwide Series in Computer Science","volume-title":"Concurrent and Real-time Systems: the CSP Approach","author":"S Schneider","year":"2000","unstructured":"Schneider, S.: Concurrent and Real-time Systems: the CSP Approach. Worldwide Series in Computer Science. Wiley, Chichester (2000)"},{"issue":"2","key":"2_CR5","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1007\/s00165-009-0119-6","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. Formal Aspects Comput. 22(2), 153\u2013191 (2010)","journal-title":"Formal Aspects Comput."},{"key":"2_CR6","volume-title":"Using Z-Specification, Refinement, and Proof","author":"JCP Woodcock","year":"1996","unstructured":"Woodcock, J.C.P., Davies, J.: Using Z-Specification, Refinement, and Proof. Prentice-Hall, Englewood Cliffs (1996)"},{"key":"2_CR7","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, Heidelberg (2011)"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-642-14521-6_12","volume-title":"Unifying Theories of Programming","author":"J Woodcock","year":"2010","unstructured":"Woodcock, J.: The miracle of reactive programming. In: Butterfield, A. (ed.) UTP 2008. LNCS, vol. 5713, pp. 202\u2013217. Springer, Heidelberg (2010). doi:\n10.1007\/978-3-642-14521-6_12"},{"key":"2_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. LNCS, vol. 8413, pp. 187\u2013201. Springer, Heidelberg (2014). doi:\n10.1007\/978-3-642-54862-8_13"},{"issue":"6","key":"2_CR10","doi-asserted-by":"crossref","first-page":"1730","DOI":"10.1109\/TSMCC.2012.2218236","volume":"42","author":"JA Hilder","year":"2012","unstructured":"Hilder, J.A., Owens, N.D.L., Neal, M.J., Hickey, P.J., Cairns, S.N., Kilgour, D.P.A., Timmis, J., Tyrrell, A.M.: Chemical detection using the receptor density algorithm. IEEE Trans. Syst. Man Cybern. C Appl. Rev. 42(6), 1730\u20131741 (2012)","journal-title":"IEEE Trans. Syst. Man Cybern. C Appl. Rev."},{"issue":"11","key":"2_CR11","doi-asserted-by":"crossref","first-page":"1429","DOI":"10.1016\/j.robot.2012.03.003","volume":"60","author":"C Dixon","year":"2012","unstructured":"Dixon, C., Winfield, A.F.T., Fisher, M., Zeng, C.: Towards temporal verification of swarm robotic systems. Robot. Auton. Syst. 60(11), 1429\u20131441 (2012)","journal-title":"Robot. Auton. Syst."},{"key":"2_CR12","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). doi:\n10.1007\/978-3-319-14806-9_2"},{"issue":"4","key":"2_CR13","doi-asserted-by":"crossref","first-page":"695","DOI":"10.1109\/TEVC.2008.2011746","volume":"13","author":"S Nouyan","year":"2009","unstructured":"Nouyan, S., Gross, R., Bonani, M., Mondada, F., Dorigo, M.: Teamwork in self-organized robot colonies. IEEE Trans. Evol. Comput. 13(4), 695\u2013711 (2009)","journal-title":"IEEE Trans. Evol. Comput."},{"issue":"3","key":"2_CR14","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1162\/ARTL_a_00132","volume":"20","author":"G Pini","year":"2014","unstructured":"Pini, G., Brutschy, A., Scheidler, A., Dorigo, M., Birattari, M.: Task partitioning in a robot swarm: object retrieval as a sequence of subtasks with direct object transfer. Artif. Life 20(3), 291\u2013317 (2014)","journal-title":"Artif. Life"},{"issue":"1","key":"2_CR15","first-page":"75","volume":"7","author":"A Nordmann","year":"2016","unstructured":"Nordmann, A., Hochgeschwender, N., Wigand, D., Wrede, S.: A survey on domain-specific modeling and languages in Robotics. J. Softw. Eng. Robot. 7(1), 75\u201399 (2016)","journal-title":"J. Softw. Eng. Robot."},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-319-47846-3_24","volume-title":"Formal Methods and Software Engineering","author":"M Foughali","year":"2016","unstructured":"Foughali, M., Berthomieu, B., Dal Zilio, S., Ingrand, F., Mallet, A.: Model checking real-time properties on the functional layer of autonomous robots. In: Ogata, K., Lawford, M., Liu, S. (eds.) ICFEM 2016. LNCS, vol. 10009, pp. 383\u2013399. Springer, Cham (2016). doi:\n10.1007\/978-3-319-47846-3_24"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"606","DOI":"10.1007\/978-3-642-04425-0_47","volume-title":"Model Driven Engineering Languages and Systems","author":"F Fleurey","year":"2009","unstructured":"Fleurey, F., Solberg, A.: A domain specific modeling language supporting specification, simulation and execution of dynamic adaptive systems. In: Sch\u00fcrr, A., Selic, B. (eds.) MODELS 2009. LNCS, vol. 5795, pp. 606\u2013621. Springer, Heidelberg (2009). doi:\n10.1007\/978-3-642-04425-0_47"},{"issue":"6","key":"2_CR18","doi-asserted-by":"crossref","first-page":"1561","DOI":"10.1109\/21.257754","volume":"23","author":"DJ Musliner","year":"1993","unstructured":"Musliner, D.J., Durfee, E.H., Shin, K.G.: CIRCA: a cooperative intelligent real-time control architecture. IEEE Trans. Syst. Man Cybern. 23(6), 1561\u20131574 (1993)","journal-title":"IEEE Trans. Syst. Man Cybern."},{"key":"2_CR19","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1007\/978-1-4471-1021-7_26","volume-title":"Robotics Research","author":"B Espiau","year":"1996","unstructured":"Espiau, B., Kapellos, K., Jourdan, M.: Formal verification in robotics: why and how? In: Giralt, G., Hirzinger, G. (eds.) Robotics Research, pp. 225\u2013236. Springer, London (1996)"},{"key":"2_CR20","unstructured":"Schlegel, C., Hassler, T., Lotz, A., Steck, A.: Robotic software systems: from code-driven to model-driven designs. In: International Conference on Advanced Robotics, ICAR 2009, 1\u20138 June 2009"},{"key":"2_CR21","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). doi:\n10.1007\/978-3-642-34327-8_16"},{"key":"2_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-540-39958-2_16","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"H Rasch","year":"2003","unstructured":"Rasch, H., Wehrheim, H.: Checking consistency in UML diagrams: classes and state machines. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 229\u2013243. Springer, Heidelberg (2003). doi:\n10.1007\/978-3-540-39958-2_16"},{"issue":"2\u20133","key":"2_CR23","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1007\/s00165-003-0008-3","volume":"15","author":"J Davies","year":"2003","unstructured":"Davies, J., Crichton, C.: Concurrency and refinement in the unified modeling language. Formal Aspects Comput. 15(2\u20133), 118\u2013145 (2003)","journal-title":"Formal Aspects Comput."},{"key":"2_CR24","volume-title":"Modeling and Analysis of Real-Time and Embedded Systems with UML and MARTE: Developing Cyber-Physical Systems","author":"B Selic","year":"2013","unstructured":"Selic, B., Grard, S.: Modeling and Analysis of Real-Time and Embedded Systems with UML and MARTE: Developing Cyber-Physical Systems. Morgan Kaufmann Publishers Inc., Burlington (2013)"},{"key":"2_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/BFb0057795","volume-title":"Languages, Compilers, and Tools for Embedded Systems","author":"B Selic","year":"1998","unstructured":"Selic, B.: Using UML for modeling complex real-time systems. In: Mueller, F., Bestavros, A. (eds.) LCTES 1998. LNCS, vol. 1474, pp. 250\u2013260. Springer, Heidelberg (1998). doi:\n10.1007\/BFb0057795"},{"key":"2_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/11494881_7","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"R Ramos","year":"2005","unstructured":"Ramos, R., Sampaio, A., Mota, A.: A semantics for UML-RT active classes via mapping into circus. In: Steffen, M., Zavattaro, G. (eds.) FMOODS 2005. LNCS, vol. 3535, pp. 99\u2013114. Springer, Heidelberg (2005). doi:\n10.1007\/11494881_7"},{"issue":"1","key":"2_CR27","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1016\/j.scico.2006.08.005","volume":"65","author":"KB Akhlaki","year":"2007","unstructured":"Akhlaki, K.B., Tunon, M.I.C., Terriza, J.A.H., Morales, L.E.M.: A methodological approach to the formal specification of real-time systems by transformation of UML-RT design models. Sci. Comput. Program. 65(1), 41\u201356 (2007)","journal-title":"Sci. Comput. Program."},{"issue":"6","key":"2_CR28","doi-asserted-by":"crossref","first-page":"1661","DOI":"10.1145\/197320.197322","volume":"16","author":"JJ Zic","year":"1994","unstructured":"Zic, J.J.: Time-constrained buffer specifications in CSP + T and timed CSP. ACM Trans. Program. Lang. Syst. 16(6), 1661\u20131674 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"2","key":"2_CR29","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theoret. Comput. Sci."},{"key":"2_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/BFb0020949","volume-title":"Hybrid Systems III","author":"J Bengtsson","year":"1996","unstructured":"Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: UPPAAL \u2014 a tool suite for automatic verification of real-time systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, pp. 232\u2013243. Springer, Heidelberg (1996). doi:\n10.1007\/BFb0020949"},{"key":"2_CR31","unstructured":"Miyazawa, A., et al.: RoboChart reference manual. Technical report, University of York (2017). \nhttp:\/\/bit.ly\/2plUry4"},{"key":"2_CR32","unstructured":"RoboCalc Project: RoboChart Case Studies (2017).\nwww.cs.york.ac.uk\/circus\/RoboCalc\/case-studies\/"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66845-1_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,8,26]],"date-time":"2017-08-26T11:38:07Z","timestamp":1503747487000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66845-1_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319668444","9783319668451"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66845-1_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}