{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,20]],"date-time":"2025-08-20T13:09:55Z","timestamp":1755695395689,"version":"3.40.3"},"publisher-location":"Singapore","reference-count":27,"publisher":"Springer Nature Singapore","isbn-type":[{"type":"print","value":"9789819756742"},{"type":"electronic","value":"9789819756759"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-981-97-5675-9_2","type":"book-chapter","created":{"date-parts":[[2024,8,1]],"date-time":"2024-08-01T01:10:40Z","timestamp":1722474640000},"page":"15-26","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Formal Verification of Path Planning Safety and Reachability in Unmanned Surface Vehicles"],"prefix":"10.1007","author":[{"given":"Yu","family":"Lu","sequence":"first","affiliation":[]},{"given":"Pan","family":"Sun","sequence":"additional","affiliation":[]},{"given":"Shijie","family":"Shi","sequence":"additional","affiliation":[]},{"given":"Meng","family":"Li","sequence":"additional","affiliation":[]},{"given":"Huilin","family":"Ge","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,8,1]]},"reference":[{"issue":"2","key":"2_CR1","doi-asserted-by":"publisher","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_CR2","doi-asserted-by":"publisher","DOI":"10.1016\/j.eswa.2023.123113","volume":"245","author":"G Alwhishi","year":"2024","unstructured":"Alwhishi, G., Bentahar, J., Elwhishi, A., et al.: Mv-checker: a software tool for multi-valued model checking intelligent applications with trust and commitment. Expert Syst. Appl. 245, 123113 (2024)","journal-title":"Expert Syst. Appl."},{"key":"2_CR3","doi-asserted-by":"publisher","DOI":"10.1016\/j.inffus.2023.102048","volume":"102","author":"G Alwhishi","year":"2024","unstructured":"Alwhishi, G., Bentahar, J., Elwhishi, A., et al.: Multi-valued model checking iot and intelligent systems with commitment protocols in multi-source data environments. Inf. Fusion 102, 102048 (2024)","journal-title":"Inf. Fusion"},{"issue":"2","key":"2_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3542945","volume":"32","author":"H Araujo","year":"2023","unstructured":"Araujo, H., Mousavi, M.R., Varshosaz, M.: Testing, validation, and verification of robotic and autonomous systems: a systematic review. ACM Trans. Softw. Eng. Methodol. 32(2), 1\u201361 (2023)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"issue":"6","key":"2_CR5","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C Baier","year":"2003","unstructured":"Baier, C., Haverkort, B., Hermanns, J.P., et al.: Model-checking algorithms for continuous-time markov chains. IEEE Trans. Softw. Eng. 29(6), 524\u2013541 (2003)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on UPPAAL. In: Formal Methods for the Design of Real-Time Systems, pp. 200\u2013236 (2004)","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Behrmann, G., Larsen, K.G., Rasmussen, J.I.: Priced Timed automata: algorithms and applications. In: Formal Methods for Components and Objects, vol. 3657, pp. 162\u2013182 (2005)","DOI":"10.1007\/11561163_8"},{"issue":"2","key":"2_CR8","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/s10703-007-0035-4","volume":"31","author":"P Bouyer","year":"2007","unstructured":"Bouyer, P., Brihaye, T., Bruy\u00e8re, V., et al.: On the optimal reachability problem of weighted timed automata. Formal Meth. Syst. Des. 31(2), 135\u2013175 (2007)","journal-title":"Formal Meth. Syst. Des."},{"key":"2_CR9","doi-asserted-by":"publisher","first-page":"105139","DOI":"10.1016\/j.ssci.2020.105139","volume":"136","author":"D Dghaym","year":"2021","unstructured":"Dghaym, D., Hoang, T.S., Turnock, M.B., et al.: An stpa-based formal composition framework for trustworthy autonomous maritime systems. Saf. Sci. 136, 105139 (2021)","journal-title":"Saf. Sci."},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Gu, R., Marinescu, R., Seceleanu, C., Lundqvist, K.: Towards a Two-layer framework for verifying autonomous vehicles. In: NASA Formal Methods, pp. 186\u2013203 (2019)","DOI":"10.1007\/978-3-030-20652-9_12"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Hoffmann, R., Ireland, M., Miller, A., et al.: Autonomous agent behaviour modelled in PRISM \u2013 a case study. In: Model Checking Software, vol. 9641, pp. 104\u2013110 (2016)","DOI":"10.1007\/978-3-319-32582-8_7"},{"key":"2_CR12","unstructured":"Ireland, M.L., Hoffmann, R., Miller, A., et al.: A continuous-time model of an autonomous aerial vehicle to inform and validate formal verification methods. arXiv preprint arXiv:1609.00177 (2016)"},{"issue":"4","key":"2_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3393666","volume":"25","author":"RL Jana","year":"2020","unstructured":"Jana, R.L., Dey, S., Dasgupta, P.: A hierarchical HVAC control scheme for energy-aware smart building automation. TODAES 25(4), 1\u201333 (2020)","journal-title":"TODAES"},{"key":"2_CR14","doi-asserted-by":"publisher","DOI":"10.1016\/j.apor.2022.103125","volume":"122","author":"E Krell","year":"2022","unstructured":"Krell, E., King, S.A., Carrillo, L.R.G.: Autonomous surface vehicle energy-efficient and reward-based path planning using particle swarm optimization and visibility graphs. Appl. Ocean Res. 122, 103125 (2022)","journal-title":"Appl. Ocean Res."},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Larsen, K., Behrmann, G., Brinksma, E., et al.: As cheap as possible: efficient cost-optimal reachability for priced timed automata. In: CAV 2001, pp. 493\u2013505 (2001)","DOI":"10.1007\/3-540-44585-4_47"},{"issue":"2\u20133","key":"2_CR16","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1016\/j.tcs.2007.09.021","volume":"390","author":"KG Larsen","year":"2008","unstructured":"Larsen, K.G., Rasmussen, J.I.: Optimal reachability for multi-priced timed automata. Theoret. Comput. Sci. 390(2\u20133), 197\u2013213 (2008)","journal-title":"Theoret. Comput. Sci."},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Liu, H., Cheng, R., Yang, T., Wang, J.: Modeling and verifying the communication and control of a fleet of collaborative autonomous underwater vehicles. In: IECON (2017)","DOI":"10.1109\/IECON.2017.8216540"},{"key":"2_CR18","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1016\/j.oceaneng.2015.01.008","volume":"97","author":"Y Liu","year":"2015","unstructured":"Liu, Y., Bucknall, R.: Path planning algorithm for unmanned surface vehicle formations in a practical maritime environment. Ocean Eng. 97, 126\u2013144 (2015)","journal-title":"Ocean Eng."},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Lu, Y., Niu, H., Savvaris, A., Tsourdos, A.: Verifying collision avoidance behaviours for unmanned surface vehicles using probabilistic model checking. In: CAMS 2016 (2016)","DOI":"10.1016\/j.ifacol.2016.10.332"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Molnar, L., Veres, S.M.: System verification of autonomous underwater vehicles by model checking. In: OCEANS 2009-EUROPE, pp. 1\u201310 (2009)","DOI":"10.1109\/OCEANSE.2009.5278284"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"Niu, H., Ji, Z., Savvaris, A., Tsourdos, A., Carrasco, J.: Model checking for decision making system of long endurance unmanned surface vehicle. In: SII, pp. 256\u2013262 (2021)","DOI":"10.1109\/IEEECONF49454.2021.9382677"},{"issue":"23","key":"2_CR22","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/j.ifacol.2016.10.331","volume":"49","author":"H Niu","year":"2016","unstructured":"Niu, H., Lu, Y., Savvaris, A., Tsourdos, A.: Efficient path planning algorithms for unmanned surface vehicle. IFAC-PapersOnLine 49(23), 121\u2013126 (2016)","journal-title":"IFAC-PapersOnLine"},{"key":"2_CR23","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1016\/j.oceaneng.2018.01.025","volume":"161","author":"H Niu","year":"2018","unstructured":"Niu, H., Lu, Y., Savvaris, A., Tsourdos, A.: An energy-efficient path planning algorithm for unmanned surface vehicles. Ocean Eng. 161, 308\u2013321 (2018)","journal-title":"Ocean Eng."},{"key":"2_CR24","doi-asserted-by":"publisher","DOI":"10.1016\/j.oceaneng.2022.111010","volume":"251","author":"\u00dc \u00d6zt\u00fcrk","year":"2022","unstructured":"\u00d6zt\u00fcrk, \u00dc., Akda\u011f, M., Ayabakan, T.: A review of path planning algorithms in maritime autonomous surface ships: navigation safety perspective. Ocean Eng. 251, 111010 (2022)","journal-title":"Ocean Eng."},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"Saberi, A.K., Groote, J.F., Keshishzadeh, S.: Analysis of path planning algorithms: a formal verification-based approach. In: ECAL 2013, pp. 232\u2013239 (2013)","DOI":"10.7551\/978-0-262-31709-2-ch035"},{"key":"2_CR26","doi-asserted-by":"publisher","DOI":"10.1016\/j.knosys.2023.110355","volume":"264","author":"X Wang","year":"2023","unstructured":"Wang, X., Liu, J., Nugent, C., et al.: Mobile agent path planning under uncertain environment using reinforcement learning and probabilistic model checking. Knowl.-Based Syst. 264, 110355 (2023)","journal-title":"Knowl.-Based Syst."},{"issue":"5","key":"2_CR27","first-page":"258","volume":"11","author":"M Webster","year":"2014","unstructured":"Webster, M., Cameron, N., Fisher, M., et al.: Generating certification evidence for autonomous unmanned aircraft using model checking and simulation. J. Aeros. Inf. Syst. 11(5), 258\u2013279 (2014)","journal-title":"J. Aeros. Inf. Syst."}],"container-title":["Lecture Notes in Computer Science","Advanced Intelligent Computing Technology and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-97-5675-9_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,1]],"date-time":"2024-08-01T01:11:16Z","timestamp":1722474676000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-97-5675-9_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9789819756742","9789819756759"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-981-97-5675-9_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"1 August 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICIC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Computing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tianjin","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":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 August 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 August 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"icic2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.ic-icc.cn\/2024\/index.htm","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}