{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,31]],"date-time":"2025-12-31T00:18:37Z","timestamp":1767140317930,"version":"build-2238731810"},"reference-count":69,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2025,3,12]],"date-time":"2025-03-12T00:00:00Z","timestamp":1741737600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,3,12]],"date-time":"2025-03-12T00:00:00Z","timestamp":1741737600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/R025479\/1EP\/V026801\/1"],"award-info":[{"award-number":["EP\/R025479\/1EP\/V026801\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000287","name":"Royal Academy of Engineering","doi-asserted-by":"publisher","award":["CiET1718\/45"],"award-info":[{"award-number":["CiET1718\/45"]}],"id":[{"id":"10.13039\/501100000287","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2025,10]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Simulation is a favoured technique in robotics. It is, however, costly, in terms of development time, and its usability is limited by the lack of standardisation and portability of simulators. We present RoboSim, a diagrammatic tool-independent domain-specific language to model robotic platforms and their controllers. It can be regarded as a profile of UML\/SysML enriched with time primitives, differential equations, and a mathematical semantics. Our previous work on RoboSim described a notation to specify control software. In this paper, we present a novel notation to describe physical models: block diagrams that can be linked to the platform-independent software model to characterise how services required by the software are realised by actuators and sensors. Behaviours are specified by differential equations, and simulations and mathematical models of the whole system can be generated automatically. Our main contributions are a modular and extensible diagrammatic notation that supports the explicit specification of physical behaviours; a set of validation rules that identify well-formed models; a model-to-model transformation from RoboSim to an input format accepted by several simulators; and a formal semantics for mathematical reasoning.<\/jats:p>","DOI":"10.1007\/s10270-025-01270-9","type":"journal-article","created":{"date-parts":[[2025,3,12]],"date-time":"2025-03-12T02:20:13Z","timestamp":1741746013000},"page":"1549-1593","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Diagrammatic physical robot models"],"prefix":"10.1007","volume":"24","author":[{"given":"Alvaro","family":"Miyazawa","sequence":"first","affiliation":[]},{"given":"Sharar","family":"Ahmadi","sequence":"additional","affiliation":[]},{"given":"Ana","family":"Cavalcanti","sequence":"additional","affiliation":[]},{"given":"James","family":"Baxter","sequence":"additional","affiliation":[]},{"given":"Mark","family":"Post","sequence":"additional","affiliation":[]},{"given":"Pedro","family":"Ribeiro","sequence":"additional","affiliation":[]},{"given":"Jon","family":"Timmis","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Wright","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,3,12]]},"reference":[{"key":"1270_CR1","doi-asserted-by":"crossref","unstructured":"Aladjev, V.: Computer algebra system maple: a new software library. In: International Conference on Computational Science, pp. 711\u2013717. Springer (2003)","DOI":"10.1007\/3-540-44860-8_73"},{"key":"1270_CR2","doi-asserted-by":"crossref","unstructured":"Aravind, G., Vasan, G., Kumar, T.\u00a0S.\u00a0B.\u00a0G.,Balajiand R.\u00a0N., Ilango, G.\u00a0S.: A control strategy for an autonomous robotic vacuum cleaner for solar panels. In: Texas Instruments India Educators\u2019 Conference, pp. 53\u201361 (2014)","DOI":"10.1109\/TIIEC.2014.018"},{"issue":"3","key":"1270_CR3","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/s10846-021-01386-2","volume":"102","author":"M Askarpour","year":"2021","unstructured":"Askarpour, M., Lestingi, L., Longoni, S., Iannacci, N., Rossi, M., Vicentini, F.: Formally-based model-driven development of collaborative robotic applications. J. Intell. Robot. Syst. 102(3), 59 (2021)","journal-title":"J. Intell. Robot. Syst."},{"key":"1270_CR4","doi-asserted-by":"crossref","unstructured":"Baxter, J., Carvalho, G., Cavalcanti, A.\u00a0L.\u00a0C., Rodrigues, F.: RoboWorld: verification of robotic systems with environment in the loop. Formal Aspects of Comput. (2023)","DOI":"10.1145\/3625563"},{"key":"1270_CR5","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/s00236-020-00394-3","volume":"59","author":"J Baxter","year":"2022","unstructured":"Baxter, J., Ribeiro, P., Cavalcanti, A.L.C.: Sound reasoning in tock-CSP. Acta Inform. 59, 125\u2013162 (2022)","journal-title":"Acta Inform."},{"key":"1270_CR6","doi-asserted-by":"crossref","unstructured":"Bellamy, D.\u00a0D., Chance, G., Caleb-Solly, P. Dogramadzi, S.: Safety assessment review of a dressing assistance robot. Front. Robotics AI 8 (2021)","DOI":"10.3389\/frobt.2021.667316"},{"issue":"5","key":"1270_CR7","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1002\/rob.4620060505","volume":"6","author":"B Benhabib","year":"1989","unstructured":"Benhabib, B., Zak, G., Lipton, M.G.: A generalized kinematic modeling method for modular robots. J. Robot. Syst. 6(5), 545\u2013571 (1989)","journal-title":"J. Robot. Syst."},{"key":"1270_CR8","doi-asserted-by":"crossref","unstructured":"Bi, Z.\u00a0M., Zhang, W.\u00a0J., Chen, I.-M., Lang, S.\u00a0Y.\u00a0T.: Automated generation of the D-H parameters for configuration design of modular manipulators. Robotics Comput. Integr. Manuf. 23(5)(2007)","DOI":"10.1016\/j.rcim.2006.02.014"},{"key":"1270_CR9","doi-asserted-by":"crossref","unstructured":"Bonani, M., Longchamp, V., Magnenat, S., R\u00e9tornaz, P., Burnier, D., Roulet, G., Vaussard, F., Bleuler, H., Mondada, F.: The marXbot, a miniature mobile robot opening new perspectives for the collective-robotic research. In: IEEE\/RSJ International Conference on Intelligent Robots and Systems, pp. 4187\u20134193 (2010)","DOI":"10.1109\/IROS.2010.5649153"},{"key":"1270_CR10","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1016\/j.jss.2019.02.021","volume":"151","author":"D Bozhinoski","year":"2019","unstructured":"Bozhinoski, D., Di Ruscio, D., Malavolta, I., Pelliccione, P., Crnkovic, I.: Safety for mobile robotic systems: a systematic mapping study from a software engineering perspective. J. Syst. Softw. 151, 150\u2013179 (2019)","journal-title":"J. Syst. Softw."},{"key":"1270_CR11","doi-asserted-by":"crossref","unstructured":"Brambilla, M., Brutschy, A., Dorigo, M., Birattari, M.: Property-driven design for robot swarms: a design method based on prescriptive modeling and model checking. ACM Trans. Auton. Adapt. Syst. 9(4) (2014)","DOI":"10.1145\/2700318"},{"issue":"1","key":"1270_CR12","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1109\/TASE.2019.2932150","volume":"18","author":"A Casalino","year":"2021","unstructured":"Casalino, A., Zanchettin, A.M., Piroddi, L., Rocco, P.: Optimal scheduling of human\u2013robot collaborative assembly operations with time petri nets. IEEE Trans. Autom. Sci. Eng. 18(1), 70\u201384 (2021)","journal-title":"IEEE Trans. Autom. Sci. Eng."},{"key":"1270_CR13","doi-asserted-by":"crossref","unstructured":"Cavalcanti, A.\u00a0L.\u00a0C., Barnett, W., Baxter, J., Carvalho, G., Filho, M.\u00a0C., Miyazawa, A., Ribeiro, P., Sampaio, A.\u00a0C.\u00a0A.: RoboStar Technology: A Roboticist\u2019s Toolbox for Combined Proof, Simulation, and Testing. Springer International Publishing, pp. 249\u2013293 (2021)","DOI":"10.1007\/978-3-030-66494-7_9"},{"issue":"4","key":"1270_CR14","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/s00165-010-0170-3","volume":"23","author":"ALC Cavalcanti","year":"2011","unstructured":"Cavalcanti, A.L.C., Clayton, P., O\u2019Halloran, C.: From control law diagrams to Ada via Circus. Formal Aspects Comput. 23(4), 465\u2013512 (2011)","journal-title":"Formal Aspects Comput."},{"key":"1270_CR15","doi-asserted-by":"crossref","unstructured":"Cavalcanti, A.\u00a0L.\u00a0C., Dongol, B., Hierons, R., Timmis, J., Woodcock, J.\u00a0C.\u00a0P. (eds): Software Engineering for Robotics. Springer International Publishing (2021)","DOI":"10.1007\/978-3-030-66494-7"},{"key":"1270_CR16","doi-asserted-by":"crossref","unstructured":"Cavalcanti, A.\u00a0L.\u00a0C., Conserva Filho, M., Ribeiro, P., Sampaio, A.\u00a0C.A.: Laws of timed state machines. Comput. J. (2023)","DOI":"10.1093\/comjnl\/bxad124"},{"key":"1270_CR17","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-319-67425-4_11","volume-title":"Present and Ulterior Software Engineering","author":"ALC Cavalcanti","year":"2017","unstructured":"Cavalcanti, A.L.C., Miyazawa, A., Payne, R., Woodcock, J.: Sound simulation and co-simulation for robotics. In: Mazzara, M., Meyer, B. (eds.) Present and Ulterior Software Engineering, pp. 173\u2013194. Springer International Publishing, Berlin (2017)"},{"key":"1270_CR18","unstructured":"Cavalcanti, A.\u00a0L.\u00a0C., Ribeiro, P., Miyazawa, A., Sampaio, A.\u00a0C.\u00a0A., Conserva Filho, M.\u00a0S., Didier, A.: RoboSim Reference Manual. University of York (2019). http:\/\/robostar.cs.york.ac.uk\/notations\/"},{"key":"1270_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.scico.2019.01.004","volume":"174","author":"ALC Cavalcanti","year":"2019","unstructured":"Cavalcanti, A.L.C., Sampaio, A.C.A., Miyazawa, A., Ribeiro, P., Conserva Filho, M., Didier, A., Li, W., Timmis, J.: Verified simulation for robotics. Sci. Comput. Program. 174, 1\u201337 (2019)","journal-title":"Sci. Comput. Program."},{"key":"1270_CR20","unstructured":"Cavalcanti, A.\u00a0L.\u00a0C., Sampaio, A.\u00a0C.\u00a0A., Ribeiro, P., Miyazawa, A., Conserva Filho, M., Didier, A.: RoboSim Reference Manual. Technical report, University of York, Department of Computer Science, York, UK, (2020). http:\/\/robostar.cs.york.ac.uk\/notations\/"},{"key":"1270_CR21","doi-asserted-by":"crossref","unstructured":"Chance, G., Camilleri, A., Winstone, B., Caleb-Solly, P., Dogramadzi, S.: An assistive robot to support dressing\u2014strategies for planning and error handling. In: 6th IEEE International Conference on Biomedical Robotics and Biomechatronics, pp. 774\u2013780 (2016)","DOI":"10.1109\/BIOROB.2016.7523721"},{"issue":"2","key":"1270_CR22","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1177\/027836499901800207","volume":"18","author":"I-M Chen","year":"1999","unstructured":"Chen, I.-M., Yeo, S.H., Chen, G., Yang, G.: Kernel for modular robot applications: automatic modeling techniques. Int. J. Robot. Res. 18(2), 225\u2013242 (1999)","journal-title":"Int. J. Robot. Res."},{"key":"1270_CR23","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-39799-8_18","volume-title":"Computer Aided Verification","author":"X Chen","year":"2013","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification, pp. 258\u2013263. Springer, Berlin (2013)"},{"key":"1270_CR24","doi-asserted-by":"crossref","unstructured":"Ciszewski, M., Mitka, L., Buratowski, T., Giergiel, M.: Modeling and simulation of a tracked mobile inspection robot in Matlab and V-Rep software. J. Autom. Mob. Robotics Intell. Syst. 5\u201311 (2017)","DOI":"10.14313\/JAMRIS_2-2017\/11"},{"issue":"1","key":"1270_CR25","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1109\/MRA.2012.2205652","volume":"20","author":"Tinne De Laet","year":"2013","unstructured":"De Laet, Tinne, Bellens, Steven, Smits, Ruben, Aertbelien, Erwin, Bruyninckx, Herman, De Schutter, Joris: Geometric relations between rigid bodies (part 1): semantics for standardization. IEEE Robotics Autom. Mag. 20(1), 84\u201393 (2013)","journal-title":"IEEE Robotics Autom. Mag."},{"key":"1270_CR26","doi-asserted-by":"crossref","unstructured":"De\u00a0Laet, T., Bruyninckx, H., De\u00a0Schutter, J.: Rigid body pose and twist scene graph founded on geometric relations semantics for robotic applications. In: 2013 IEEE\/RSJ International Conference on Intelligent Robots and Systems, pp. 2398\u20132405 (2013)","DOI":"10.1109\/IROS.2013.6696693"},{"key":"1270_CR27","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1115\/1.4011045","volume":"22","author":"J Denavit","year":"1955","unstructured":"Denavit, J., Hartenberg, R.S.: A kinematic notation for lower-pair mechanisms based on matrices. Trans. Assoc. Mech. Eng. J. Appl. Mech. 22, 215\u2013221 (1955)","journal-title":"Trans. Assoc. Mech. Eng. J. Appl. Mech."},{"key":"1270_CR28","doi-asserted-by":"crossref","unstructured":"Farrell, M., Luckcuck, M., Fisher, M.: Robotics and integrated formal methods: necessity meets opportunity. In: Furia, C.\u00a0A., Winter, K. (eds) Integrated Formal Methods, Volume 11023 of Lecture Notes in Computer Science, pp. 161\u2013171. Springer (2018)","DOI":"10.1007\/978-3-319-98938-9_10"},{"key":"1270_CR29","doi-asserted-by":"crossref","unstructured":"Fleurey, F., Solberg, A.: A domain specific modeling language supporting specification, simulation and execution of dynamic adaptive systems. In: 12th International Conference on Model Driven Engineering Languages and Systems, pp. 606\u2013621. Springer (2009)","DOI":"10.1007\/978-3-642-04425-0_47"},{"key":"1270_CR30","doi-asserted-by":"crossref","unstructured":"Foster, S.: Hybrid relations in Isabelle\/UTP. In: 7th International Symposium on Unifying Theories of Programming, Volume 11885 of Lecture Notes in Computer Science, pp. 130\u2013153. Springer (2019)","DOI":"10.1007\/978-3-030-31038-7_7"},{"key":"1270_CR31","doi-asserted-by":"crossref","unstructured":"Foster, S., Baxter, J., Cavalcanti, A.\u00a0L.\u00a0C., Miyazawa, A., Woodcock, J.\u00a0C.\u00a0P.: Automating verification of state machines with reactive designs and Isabelle\/UTP. In: Bae, K., \u00d6lveczky, P.\u00a0C. (eds.) Formal Aspects of Component Software. pp. 137\u2013155. Springer, Cham (2018)","DOI":"10.1007\/978-3-030-02146-7_7"},{"key":"1270_CR32","doi-asserted-by":"crossref","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) Formal Methods and Software Engineering, pp. 383\u2013399. Springer (2016)","DOI":"10.1007\/978-3-319-47846-3_24"},{"key":"1270_CR33","doi-asserted-by":"crossref","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.\u00a0W.: FDR3\u2014a modern refinement checker for CSP. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 187\u2013201 (2014)","DOI":"10.1007\/978-3-642-54862-8_13"},{"key":"1270_CR34","doi-asserted-by":"crossref","unstructured":"Giese, H., Sch\u00e4fer, W.: Model-Driven Development of Safe Self-optimizing Mechatronic Systems with MechatronicUML. In: C\u00e1mara, J., Lemos, R., Ghezzi, C., Lopes, A. (eds) Assurances for Self-Adaptive Systems\u2014Principles, Models, and Techniques, Volume 7740 of Lecture Notes in Computer Science, pp. 152\u2013186. Springer (2013)","DOI":"10.1007\/978-3-642-36249-1_6"},{"key":"1270_CR35","doi-asserted-by":"crossref","unstructured":"Gobillot, N., Lesire, C., Doose, D.: A modeling framework for software architecture specification and validation. In: Brugali, D., Broenink, J.\u00a0F., Kroeger, T., MacDonald, B.\u00a0A. (eds) Simulation, Modeling, and Programming for Autonomous Robots, pp. 303\u2013314. Springer International Publishing (2014)","DOI":"10.1007\/978-3-319-11900-7_26"},{"key":"1270_CR36","volume-title":"Unifying Theories of Programming","author":"CAR Hoare","year":"1998","unstructured":"Hoare, C.A.R., Jifeng, He.: Unifying Theories of Programming. Prentice-Hall, Hoboken (1998)"},{"issue":"6","key":"1270_CR37","doi-asserted-by":"publisher","first-page":"635","DOI":"10.1002\/(SICI)1097-024X(199606)26:6<635::AID-SPE26>3.0.CO;2-P","volume":"26","author":"R Ierusalimschy","year":"1996","unstructured":"Ierusalimschy, R., Figueiredo, L.H., Filho, W.C.: Lua\u2014an extensible extension language. Softw. Pract. Exp. 26(6), 635\u2013652 (1996)","journal-title":"Softw. Pract. Exp."},{"key":"1270_CR38","unstructured":"Jifeng, H.: From CSP to hybrid systems. In: A Classical Mind, pp. 171\u2013189. Prentice-Hall (1994)"},{"issue":"3\/4","key":"1270_CR39","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1145\/2110170.2110185","volume":"45","author":"D Joyner","year":"2012","unstructured":"Joyner, D., \u010cert\u00edk, O., Meurer, A., Granger, B.E.: Open source computer algebra systems: SymPy. ACM Commun. Comput. Algebra 45(3\/4), 225\u2013234 (2012)","journal-title":"ACM Commun. Comput. Algebra"},{"key":"1270_CR40","doi-asserted-by":"crossref","unstructured":"Kelmar, L., Khosla, P.K.: Automatic generation of kinematics for a reconfigurable modular manipulator system. In: IEEE International Conference on Robotics and Automation, vol. 2, pp. 663\u2013668 (1988)","DOI":"10.1109\/ROBOT.1988.12135"},{"key":"1270_CR41","doi-asserted-by":"publisher","DOI":"10.1016\/j.autcon.2021.103720","volume":"127","author":"S Kim","year":"2021","unstructured":"Kim, S., Peavy, M., Huang, P.-C., Kim, K.: Development of BIM-integrated construction robot task planning and simulation system. Autom. Constr. 127, 103720 (2021)","journal-title":"Autom. Constr."},{"key":"1270_CR42","doi-asserted-by":"crossref","unstructured":"Koenig, N., Andrew, H.: Design and use paradigms for gazebo, an open-source multi-robot simulator. In: 2004 IEEE\/RSJ International Conference on Intelligent Robots and Systems, vol.\u00a03, pp. 2149\u20132154. IEEE (2004)","DOI":"10.1109\/IROS.2004.1389727"},{"issue":"10\u201311","key":"1270_CR43","doi-asserted-by":"publisher","first-page":"1326","DOI":"10.1177\/0278364920950795","volume":"39","author":"K Leung","year":"2020","unstructured":"Leung, K., Schmerling, E., Zhang, M., Chen, M., Talbot, J., Gerdes, J.C., Pavone, M.: On infusing reachability-based safety assurance within planning frameworks for human\u2013robot vehicle interactions. Int. J. Robotics Res. 39(10\u201311), 1326\u20131345 (2020)","journal-title":"Int. J. Robotics Res."},{"key":"1270_CR44","doi-asserted-by":"crossref","unstructured":"Liu, J., Lv, J., Quan, Z., Zhan, N., Zhao, H., Zhou, C., Zou, L.: A calculus for hybrid CSP. In: Ueda, K. (ed) Programming Languages and Systems, Volume 6461 of Lecture Notes in Computer Science, pp. 1\u201315. Springer (2010)","DOI":"10.1007\/978-3-642-17164-2_1"},{"key":"1270_CR45","doi-asserted-by":"crossref","unstructured":"Luckcuck, M., Farrell, M., Dennis, L.\u00a0A., Dixon, C., Fisher, M.: Formal specification and verification of autonomous robotic systems: a survey. ACM Comput. Surv. 52(5), (2019)","DOI":"10.1145\/3342355"},{"key":"1270_CR46","doi-asserted-by":"crossref","unstructured":"Lynch, K.\u00a0M., Park, F.\u00a0C.: Modern Robotics: Mechanics, Planning, and Control, 1st edn. Cambridge University Press (2017)","DOI":"10.1017\/9781316661239"},{"key":"1270_CR47","unstructured":"The MathWorks, Inc: Simulink. www.mathworks.com\/products\/simulink"},{"key":"1270_CR48","doi-asserted-by":"crossref","unstructured":"Meister, E., Nosov, E., Levi, P.: Automatic onboard and online modelling of modular and self-reconfigurable robots. In: 6th IEEE Conference on Robotics, Automation and Mechatronics, pp. 91\u201396 (2013)","DOI":"10.1109\/RAM.2013.6758565"},{"key":"1270_CR49","unstructured":"Messner, B., Tilbury, D.: DC Motor Speed: System Modeling (2011). http:\/\/ctms.engin.umich.edu\/CTMS\/index.php?example=MotorSpeed&section=SystemModeling"},{"issue":"1","key":"1270_CR50","first-page":"39","volume":"1","author":"O Michel","year":"2004","unstructured":"Michel, O.: Webots: professional mobile robot simulation. Int. J. Adv. Rob. Syst. 1(1), 39\u201342 (2004)","journal-title":"Int. J. Adv. Rob. Syst."},{"key":"1270_CR51","unstructured":"Miyazawa, A., Cavalcanti, A.\u00a0L.\u00a0C., Ahmadi, S., Post, M., Timmis, J.: RoboSim Physical Modelling: Diagrammatic Physical Robot Models. Technical report, University of York, Department of Computer Science, York, UK (2020). http:\/\/robostar.cs.york.ac.uk\/notations\/"},{"key":"1270_CR52","doi-asserted-by":"crossref","unstructured":"Miyazawa, A., Ribeiro, P., Li, W., Cavalcanti, A.\u00a0L.\u00a0C., Timmis, J.: Automatic property checking of robotic applications. In: IEEE\/RSJ International Conference on Intelligent Robots and Systems, pp. 3869\u20133876 (2017)","DOI":"10.1109\/IROS.2017.8206238"},{"key":"1270_CR53","doi-asserted-by":"crossref","unstructured":"Munive, J.\u00a0H.\u00a0Y., Struth, G., Foster, S.: Differential Hoare logics and refinement calculi for hybrid systems with Isabelle\/HOL. In: 18th International Conference on Relational and Algebraic Methods in Computer Science, volume 12062 of Lecture Notes in Computer Science, pp. 169\u2013186. Springer (2020)","DOI":"10.1007\/978-3-030-43520-2_11"},{"key":"1270_CR54","doi-asserted-by":"crossref","unstructured":"Murray, Y., Sirev\u00e5g, M., Ribeiro, P., Anisi, D.\u00a0A., Mossige, M.: Safety assurance of an industrial robotic control system using hardware\/software co-verification. Sci. Comput. Program. 216, (2022)","DOI":"10.1016\/j.scico.2021.102766"},{"key":"1270_CR55","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle\/HOL: A Proof Assistant for Higher-order Logic. Springer, Berlin (2002)"},{"issue":"1","key":"1270_CR56","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. Robotics 7(1), 75\u201399 (2016)","journal-title":"J. Softw. Eng. Robotics"},{"key":"1270_CR57","unstructured":"OMG: OMG Systems Modeling Language (OMG SysML), Version 1.3 (2012)"},{"key":"1270_CR58","unstructured":"OMG: OMG Unified Modeling Language (2015)"},{"key":"1270_CR59","doi-asserted-by":"crossref","unstructured":"Paredis, C.J.J., Brown, H.B., Khosla, P.K.: A rapidly deployable manipulator system. In: Proceedings of IEEE International Conference on Robotics and Automation, vol. 2, pp. 1434\u20131439 (1996)","DOI":"10.1109\/ROBOT.1996.506907"},{"issue":"6","key":"1270_CR60","doi-asserted-by":"publisher","first-page":"609","DOI":"10.1177\/027836499501400606","volume":"14","author":"FC Park","year":"1995","unstructured":"Park, F.C., Bobrow, J.E., Ploen, S.R.: A lie group formulation of robot dynamics. Int. J. Robotics Res. 14(6), 609\u2013618 (1995)","journal-title":"Int. J. Robotics Res."},{"key":"1270_CR61","doi-asserted-by":"crossref","unstructured":"Rohmer, E., Singh, S.\u00a0P.\u00a0N., Freese, M.: V-REP: a versatile and scalable robot simulation framework. In: IEEE\/RSJ International Conference on Intelligent Robots and Systems, vol.\u00a01, pp. 1321\u20131326. IEEE (2013)","DOI":"10.1109\/IROS.2013.6696520"},{"key":"1270_CR62","doi-asserted-by":"crossref","unstructured":"Roscoe, A.\u00a0W.: Understanding concurrent systems. In: Texts in Computer Science. Springer (2011)","DOI":"10.1007\/978-1-84882-258-0"},{"key":"1270_CR63","unstructured":"Scherer, S., Lerda, F., Clarke, E.\u00a0M.: Model checking of robotic control systems. In: 8th International Symposium on Artificial Intelligence, Robotics and Automation in Space (2005)"},{"key":"1270_CR64","doi-asserted-by":"crossref","unstructured":"Siciliano, B., Sciavicco, L., Villani, L., Oriolo, G.: Robotics: Modelling, Planning and Control. Springer Publishing Company, Incorporated (2008)","DOI":"10.1007\/978-1-84628-642-1"},{"key":"1270_CR65","doi-asserted-by":"crossref","unstructured":"Tola, D., Corke, P.: Understanding urdf: a survey based on user experience (2023)","DOI":"10.1109\/CASE56687.2023.10260660"},{"issue":"1","key":"1270_CR66","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1109\/TRO.2019.2937471","volume":"36","author":"F Vicentini","year":"2020","unstructured":"Vicentini, F., Askarpour, M., Rossi, M.G., Mandrioli, D.: Safety assessment of collaborative robotics through automated formal verification. IEEE Trans. Rob. 36(1), 42\u201361 (2020)","journal-title":"IEEE Trans. Rob."},{"key":"1270_CR67","volume-title":"Using Z\u2014Specification, Refinement, and Proof","author":"JCP Woodcock","year":"1996","unstructured":"Woodcock, J.C.P., Davies, J.: Using Z\u2014Specification, Refinement, and Proof. Prentice-Hall, Hoboken (1996)"},{"key":"1270_CR68","doi-asserted-by":"crossref","unstructured":"Yao, W., Dai, W., Xiao, J., Lu, H., Zheng, Z.: A simulation system based on ROS and Gazebo for RoboCup middle size league. In: IEEE International Conference on Robotics and Biomimetics, pp. 54\u201359 (2015)","DOI":"10.1109\/ROBIO.2015.7414623"},{"key":"1270_CR69","doi-asserted-by":"crossref","unstructured":"\u017d\u00e1kov\u00e1, K.: Maxima\u2014an open alternative for engineering education. In: IEEE Global Engineering Education Conference, pp. 1022\u20131025. IEEE (2011)","DOI":"10.1109\/EDUCON.2011.5773273"}],"updated-by":[{"DOI":"10.1007\/s10270-025-01325-x","type":"correction","label":"Correction","source":"publisher","updated":{"date-parts":[[2025,10,15]],"date-time":"2025-10-15T00:00:00Z","timestamp":1760486400000}}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-025-01270-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-025-01270-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-025-01270-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,15]],"date-time":"2025-10-15T13:29:14Z","timestamp":1760534954000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-025-01270-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,3,12]]},"references-count":69,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2025,10]]}},"alternative-id":["1270"],"URL":"https:\/\/doi.org\/10.1007\/s10270-025-01270-9","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,3,12]]},"assertion":[{"value":"15 November 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 November 2024","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 January 2025","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 March 2025","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 October 2025","order":5,"name":"change_date","label":"Change Date","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Correction","order":6,"name":"change_type","label":"Change Type","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"A Correction to this paper has been published:","order":7,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"https:\/\/doi.org\/10.1007\/s10270-025-01325-x","URL":"https:\/\/doi.org\/10.1007\/s10270-025-01325-x","order":8,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}}]}}