{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T00:07:54Z","timestamp":1725926874271},"reference-count":27,"publisher":"Institute of Electronics, Information and Communications Engineers (IEICE)","issue":"10","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEICE Trans. Inf. & Syst."],"published-print":{"date-parts":[[2021,10,1]]},"DOI":"10.1587\/transinf.2020fop0002","type":"journal-article","created":{"date-parts":[[2021,9,30]],"date-time":"2021-09-30T22:40:59Z","timestamp":1633041659000},"page":"1515-1532","source":"Crossref","is-referenced-by-count":2,"title":["Formal Modeling and Verification of Concurrent FSMs: Case Study on Event-Based Cooperative Transport Robots"],"prefix":"10.1587","volume":"E104.D","author":[{"given":"Yoshinao","family":"ISOBE","sequence":"first","affiliation":[{"name":"National Institute of Advanced Industrial Science and Technology"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nobuhiko","family":"MIYAMOTO","sequence":"additional","affiliation":[{"name":"National Institute of Advanced Industrial Science and Technology"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Noriaki","family":"ANDO","sequence":"additional","affiliation":[{"name":"National Institute of Advanced Industrial Science and Technology"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yutaka","family":"OIWA","sequence":"additional","affiliation":[{"name":"National Institute of Advanced Industrial Science and Technology"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"532","reference":[{"key":"1","doi-asserted-by":"crossref","unstructured":"[1] M. Luckcuck, M. Farrell, L. Dennis, C. Dixon, and M. Fisher, \u201cFormal Specification and Verification of Autonomous Robotic Systems: A Survey,\u201d arXiv:1807.00048, 2019.","DOI":"10.1007\/978-3-030-34968-4_33"},{"key":"2","doi-asserted-by":"publisher","unstructured":"[2] C.A.R. Hoare, \u201cCommunicating sequential processes,\u201d Communications of the ACM, vol.21, no.8, pp.666-677, 1978. 10.1145\/359576.359585","DOI":"10.1145\/359576.359585"},{"key":"3","unstructured":"[3] A.W. Roscoe, The Theory and Practice of Concurrency, Prentice Hall, 1998."},{"key":"4","doi-asserted-by":"crossref","unstructured":"[4] A.W. Roscoe, \u201cUnderstanding Concurrent Systems,\u201d Springer, 2010. 10.1007\/978-1-84882-258-0","DOI":"10.1007\/978-1-84882-258-0"},{"key":"5","unstructured":"[5] University of Oxford, \u201cFDR4-The CSP Refinement Checker.\u201d https:\/\/www.cs.ox.ac.uk\/projects\/fdr\/"},{"key":"6","unstructured":"[6] RT Corporation, \u201cRaspberry Pi Mouse,\u201d https:\/\/www.rt-net.jp\/products\/raspimouse3"},{"key":"7","unstructured":"[7] \u201cThe RTC for Raspberry Pi Mouse,\u201d https:\/\/github.com\/rsdlab\/RaspberryPiMouseRTC"},{"key":"8","doi-asserted-by":"crossref","unstructured":"[8] N. Ando, T. Suehiro, K. Kitagaki, T. Kotoku, and W.-K. Yoon, \u201cRT-Middleware: Distributed Component Middleware for RT (Robot Technology),\u201d 2005 IEEE\/RSJ International Conference on Intelligent Robots and Systems (IROS2005), pp.3555-3560, 2005. 10.1109\/iros.2005.1545521","DOI":"10.1109\/IROS.2005.1545521"},{"key":"9","unstructured":"[9] AIST, \u201cOpenRTM-aist official website,\u201d https:\/\/openrtm.org\/"},{"key":"10","unstructured":"[10] AIST, \u201cOpenRTM-aist with FSM4RTC in Python,\u201d https:\/\/github.com\/OpenRTM\/OpenRTM-aist-Python"},{"key":"11","unstructured":"[11] N. Ando, \u201cAbout the standard \u201cFSM4RTC\u201d for state machine components and data ports,\u201d SICE SI2016, pp.2584-2587, 2016."},{"key":"12","unstructured":"[12] OMG available specification, \u201cRobot Technology Component Specification Version 1.1,\u201d formal\/2012-09-01. https:\/\/www.omg.org\/spec\/RTC\/"},{"key":"13","unstructured":"[13] OMG available specification, \u201cFinite State Machine Component For RTC Version 1.0,\u201d formal\/2016-04-01. https:\/\/www.omg.org\/spec\/FSM4RTC\/"},{"key":"14","doi-asserted-by":"crossref","unstructured":"[14] L. Chaimowicz, M.F.M. Campos, and V. Kumar, \u201cHybrid systems modeling of cooperative robots,\u201d Proceedings IEEE International Conference on Robotics and Automation 2003, vol.3, pp.4086-4091, 2003. 10.1109\/robot.2003.1242225","DOI":"10.1109\/ROBOT.2003.1242225"},{"key":"15","unstructured":"[15] S. Schneider, \u201cConcurrent and Real-time systems.\u201d Wiley, 2000."},{"key":"16","unstructured":"[16] Y. Isobe, \u201cWebpage on Formal Modeling and Verification of Cooperative Transport Robots,\u201d https:\/\/staff.aist.go.jp\/y-isobe\/csp-cooprobo\/"},{"key":"17","unstructured":"[17] AIST, \u201cThe system development tools for OpenRTM-aist,\u201d https:\/\/github.com\/OpenRTM\/OpenRTP-aist"},{"key":"18","doi-asserted-by":"publisher","unstructured":"[18] A. Miyazawa, P. Ribeiro, W. Li, A. Cavalcanti, J. Timmis, and J. Woodcock, \u201cRoboChart: modelling and verification of the functional behaviour of robotic applications,\u201d Software & Systems Modeling, volume 18, Springer, pp.3097-3149, 2019. 10.1007\/s10270-018-00710-z","DOI":"10.1007\/s10270-018-00710-z"},{"key":"19","unstructured":"[19] University of York, \u201cRoboTool: RoboChart Tool,\u201d https:\/\/www.cs.york.ac.uk\/robostar\/robotool\/"},{"key":"20","unstructured":"[20] P. Ribeiro, W. Li, A.L.C. Cavalcanti, and A. Sampaio, \u201cTransport: a case study of RoboTool,\u201d https:\/\/www.cs.york.ac.uk\/robostar\/case_studies\/transport\/transport.html"},{"key":"21","doi-asserted-by":"crossref","unstructured":"[21] E. Gjondrekaj, M. Loreti, R. Pugliese, F. Tiezzi, C. Pinciroli, M. Brambilla, M. Birattari, and M. Dorigo, \u201cTowards a Formal Verification Methodology for Collective Robotic Systems,\u201d International Conference on Formal Engineering Methods (ICFEM), pp.54-70, LNCS 7635, Springer, 2012. 10.1007\/978-3-642-34281-3_7","DOI":"10.1007\/978-3-642-34281-3_7"},{"key":"22","unstructured":"[22] National University of Singapre, \u201cPAT: Process Analysis Toolkit,\u201d http:\/\/www.comp.nus.edu.sg\/~pat\/"},{"key":"23","doi-asserted-by":"crossref","unstructured":"[23] T. Nipkow, L.C. Paulson, and M. Wenzel, \u201cIsabelle\/HOL-A Proof Assistant for Higher-Order Logic,\u201d LNCS 2283, Springer, 2002.","DOI":"10.1007\/3-540-45949-9"},{"key":"24","unstructured":"[24] University of Cambridge and Technische Universit\u00e4t M\u00fcnchen, \u201cIsabelle: A Generic Theorem Prover,\u201d https:\/\/isabelle.in.tum.de\/"},{"key":"25","doi-asserted-by":"crossref","unstructured":"[25] S. Foster, J. Baxter, A. Cavalcanti, A. Miyazawa, and J. Woodcock, \u201cAutomating Verification of State Machines with Reactive Designs and Isabelle\/UTP,\u201d International Conference on Formal Aspects of Component Software (FACS), LNCS 11222, Springer, pp.137-155, 2018. 10.1007\/978-3-030-02146-7_7","DOI":"10.1007\/978-3-030-02146-7_7"},{"key":"26","doi-asserted-by":"crossref","unstructured":"[26] Y. Isobe and M. Roggenbach, \u201cA Generic Theorem Prover of CSP Refinement,\u201d International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS 3440, Springer, pp.108-123, 2005. 10.1007\/978-3-540-31980-1_8","DOI":"10.1007\/978-3-540-31980-1_8"},{"key":"27","unstructured":"[27] Y. Isobe and M. Roggenbach, \u201cWebpage on CSP-Prover,\u201d https:\/\/staff.aist.go.jp\/y-isobe\/CSP-Prover\/CSP-Prover.html"}],"container-title":["IEICE Transactions on Information and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E104.D\/10\/E104.D_2020FOP0002\/_pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T03:28:00Z","timestamp":1725852480000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.jstage.jst.go.jp\/article\/transinf\/E104.D\/10\/E104.D_2020FOP0002\/_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,1]]},"references-count":27,"journal-issue":{"issue":"10","published-print":{"date-parts":[[2021]]}},"URL":"https:\/\/doi.org\/10.1587\/transinf.2020fop0002","relation":{},"ISSN":["0916-8532","1745-1361"],"issn-type":[{"type":"print","value":"0916-8532"},{"type":"electronic","value":"1745-1361"}],"subject":[],"published":{"date-parts":[[2021,10,1]]},"article-number":"2020FOP0002"}}