{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T15:27:46Z","timestamp":1780327666708,"version":"3.54.1"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T00:00:00Z","timestamp":1775001600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T00:00:00Z","timestamp":1775606400000},"content-version":"vor","delay-in-days":7,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100004913","name":"Universit\u00e0 degli Studi di Palermo","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100004913","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2026,4]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    In automotive engineering, vehicle platooning is a proposed method for improving convoy movements by coordinating them to increase the safety and efficiency of transportation systems. The complexity and stochastic nature of platooning systems provide difficulties for traditional model-checking techniques. However, Statistical Model Checking (SMC) offers a solution by using statistical inference to probabilistically evaluate system features. This paper shows that\n                    <jats:sc>Uppaal<\/jats:sc>\n                    \u00a0SMC offers a robust framework for assessing platooning systems across various operational scenarios, combining statistical analysis and formal verification methodologies. The behaviour of the platoon is modelled stochastically to cover a wide range of driving scenarios and road surfaces. Using SMC, it has been possible to gauge the safety and functionality of the platoon by estimating the probability of several properties.\n                  <\/jats:p>","DOI":"10.1007\/s10009-026-00862-0","type":"journal-article","created":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T11:41:14Z","timestamp":1775648474000},"page":"235-250","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Statistical model checking of a dynamic vehicle platoon"],"prefix":"10.1007","volume":"28","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1604-4465","authenticated-orcid":false,"given":"Cinzia","family":"Bernardeschi","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9943-1975","authenticated-orcid":false,"given":"Adriano","family":"Fagiolini","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1005-7441","authenticated-orcid":false,"given":"Giuseppe","family":"Lettieri","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-4663-6666","authenticated-orcid":false,"given":"Dario","family":"Pagani","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4906-6997","authenticated-orcid":false,"given":"Federico","family":"Rossi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,4,8]]},"reference":[{"issue":"2","key":"862_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. Theor. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"862_CR2","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1109\/IVS.2019.8813793","volume-title":"2019 IEEE Intelligent Vehicles Symposium (IV)","author":"M. Barbier","year":"2019","unstructured":"Barbier, M., Renzaglia, A., Quilbeuf, J., Rummelhard, L., Paigwar, A., Laugier, C., Legay, A., Iba\u00f1ez-Guzm\u00e1n, J., Simonin, O.: Validation of perception and decision-making systems for autonomous driving via statistical model checking. In: 2019 IEEE Intelligent Vehicles Symposium (IV), pp.\u00a0252\u2013259 (2019). https:\/\/doi.org\/10.1109\/IVS.2019.8813793"},{"key":"862_CR3","volume-title":"Conference SIA Simulation Num\u00e9rique","author":"B. Barbot","year":"2017","unstructured":"Barbot, B., B\u00e9rard, B., Duplouy, Y., Haddad, S.: Statistical model-checking for autonomous vehicle safety validation. In: Conference SIA Simulation Num\u00e9rique. Soci\u00e9t\u00e9 des Ing\u00e9nieurs de l\u2019Automobile, Montigny-le-Bretonneux (2017)"},{"key":"862_CR4","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"A Tutorial on Uppaal","author":"G. Behrmann","year":"2004","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A Tutorial on Uppaal, pp.\u00a0200\u2013236. Springer, Berlin (2004). https:\/\/doi.org\/10.1007\/978-3-540-30080-9_7"},{"key":"862_CR5","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/11561163_8","volume-title":"Formal Methods for Components and Objects: Third International Symposium, FMCO 2004","author":"G. Behrmann","year":"2005","unstructured":"Behrmann, G., Larsen, K.G., Rasmussen, J.I.: Priced timed automata: algorithms and applications. In: Formal Methods for Components and Objects: Third International Symposium, FMCO 2004, Leiden, The Netherlands, November 2\u20135, 2004, Revised Lectures 3, pp.\u00a0162\u2013182. Springer, Berlin (2005)"},{"key":"862_CR6","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/978-3-031-75107-3_19","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Rigorous Engineering of Collective Adaptive Systems","author":"C. Bernardeschi","year":"2025","unstructured":"Bernardeschi, C., Lettieri, G., Rossi, F.: Statistical model checking of cooperative autonomous driving systems. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Rigorous Engineering of Collective Adaptive Systems, pp.\u00a0316\u2013332. Springer, Cham (2025)"},{"key":"862_CR7","doi-asserted-by":"publisher","unstructured":"Blochwitz, T., Otter, M., \u00c5kesson, J., Arnold, M., Clauss, C., Elmqvist, H., Friedrich, M., Junghanns, A., Mauss, J., Neumerkel, D., Olsson, H., Viel, A.: Functional mockup interface 2.0: the standard for tool independent exchange of simulation models (2012). https:\/\/doi.org\/10.3384\/ecp12076173","DOI":"10.3384\/ecp12076173"},{"key":"862_CR8","volume-title":"Sml-a High Level Language for the Design and Verification of Finite State Machines","author":"M.C. Browne","year":"1985","unstructured":"Browne, M.C., Clarke, E.M.: Sml-a High Level Language for the Design and Verification of Finite State Machines (1985)"},{"key":"862_CR9","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/BFb0058022","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"E.M. Clarke","year":"1997","unstructured":"Clarke, E.M.: Model checking. In: Ramesh, S., Sivakumar, G. (eds.) Foundations of Software Technology and Theoretical Computer Science, pp.\u00a054\u201356. Springer, Berlin (1997). https:\/\/doi.org\/10.1007\/BFb0058022"},{"key":"862_CR10","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logics of Programs, pp.\u00a052\u201371. Springer, Berlin (1982). https:\/\/doi.org\/10.1007\/BFb0025774"},{"issue":"2","key":"862_CR11","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244\u2013263 (1986). https:\/\/doi.org\/10.1145\/5397.5399","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"862_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-35746-6_1","volume-title":"Model checking and the state explosion problem","author":"E.M. Clarke","year":"2012","unstructured":"Clarke, E.M., Klieber, W., Nov\u00e1\u010dek, M., Zuliani, P.: Model checking and the state explosion problem, pp.\u00a01\u201330. Springer, Berlin (2012). https:\/\/doi.org\/10.1007\/978-3-642-35746-6_1"},{"key":"862_CR13","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-319-67531-2_11","volume-title":"17th International Conference on Runtime Verification (RV)","author":"A. Desai","year":"2017","unstructured":"Desai, A., Dreossi, T., Seshia, S.A.: Combining model checking and runtime verification for safe robotics. In: 17th International Conference on Runtime Verification (RV), pp.\u00a0172\u2013189 (2017)"},{"issue":"5","key":"862_CR14","doi-asserted-by":"publisher","first-page":"582","DOI":"10.1177\/0142331214546522","volume":"37","author":"M. Dousti","year":"2015","unstructured":"Dousti, M., Baslam\u0131sli, S.C., Onder, E.T., Solmaz, S.: Design of a multiple-model switching controller for abs braking dynamics. Trans. Inst. Meas. Control 37(5), 582\u2013595 (2015). https:\/\/doi.org\/10.1177\/0142331214546522","journal-title":"Trans. Inst. Meas. Control"},{"key":"862_CR15","doi-asserted-by":"publisher","first-page":"748","DOI":"10.1007\/978-3-319-48989-6_46","volume-title":"FM 2016: Formal Methods","author":"P. Filipovikj","year":"2016","unstructured":"Filipovikj, P., Mahmud, N., Marinescu, R., Seceleanu, C., Ljungkrantz, O., L\u00f6nn, H.: Simulink to uppaal statistical model checker: analyzing automotive industrial systems. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016: Formal Methods, pp.\u00a0748\u2013756. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48989-6_46"},{"key":"862_CR16","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1109\/LICS.1996.561342","volume-title":"Proceedings 11th Annual IEEE Symposium on Logic in Computer Science","author":"T.A. Henzinger","year":"1996","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, pp.\u00a0278\u2013292. IEEE (1996)"},{"issue":"3","key":"862_CR17","doi-asserted-by":"publisher","first-page":"959","DOI":"10.1109\/TITS.2018.2841967","volume":"20","author":"Z. Huang","year":"2019","unstructured":"Huang, Z., Chu, D., Wu, C., He, Y.: Path planning and cooperative control for automated vehicle platoon using hybrid automata. IEEE Trans. Intell. Transp. Syst. 20(3), 959\u2013974 (2019). https:\/\/doi.org\/10.1109\/TITS.2018.2841967","journal-title":"IEEE Trans. Intell. Transp. Syst."},{"key":"862_CR18","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1016\/j.scico.2017.05.006","volume":"148","author":"M. Kamali","year":"2017","unstructured":"Kamali, M., Dennis, L.A., McAree, O., Fisher, M., Veres, S.M.: Formal verification of autonomous vehicle platooning. Sci. Comput. Program. 148, 88\u2013106 (2017). https:\/\/doi.org\/10.1016\/j.scico.2017.05.006","journal-title":"Sci. Comput. Program."},{"key":"862_CR19","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1145\/2933575.2934574","volume-title":"Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS \u201916","author":"J.P. Katoen","year":"2016","unstructured":"Katoen, J.P.: The probabilistic model checking landscape. In: Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS \u201916, pp.\u00a031\u201345. Association for Computing Machinery, New York (2016). https:\/\/doi.org\/10.1145\/2933575.2934574"},{"key":"862_CR20","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-031-57249-4_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. K\u00f6nig","year":"2024","unstructured":"K\u00f6nig, L., Heinzemann, C., Griggio, A., Klauck, M., Cimatti, A., Henze, F., Tonetta, S., K\u00fcperkoch, S., Fassbender, D., Hanselmann, M.: Towards safe autonomous driving: model checking a behavior planner during development. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp.\u00a044\u201365. Springer, Cham (2024)"},{"key":"862_CR21","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-16612-9_11","volume-title":"Runtime Verification","author":"A. Legay","year":"2010","unstructured":"Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Ro\u015fu, G., Sokolsky, O., Tillmann, N. (eds.) Runtime Verification, pp.\u00a0122\u2013135. Springer, Berlin (2010). https:\/\/doi.org\/10.1007\/978-3-642-16612-9_11"},{"key":"862_CR22","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1109\/IVS.2015.7225700","volume-title":"2015 IEEE Intelligent Vehicles Symposium (IV)","author":"S.E. Li","year":"2015","unstructured":"Li, S.E., Zheng, Y., Li, K., Wang, J.: An overview of vehicular platoon control under the four-component framework. In: 2015 IEEE Intelligent Vehicles Symposium (IV), pp.\u00a0286\u2013291. IEEE (2015)"},{"issue":"4","key":"862_CR23","doi-asserted-by":"publisher","first-page":"1051","DOI":"10.1109\/TITS.2015.2492243","volume":"17","author":"K.Y. Liang","year":"2016","unstructured":"Liang, K.Y., M\u00e5rtensson, J., Johansson, K.H.: Heavy-duty vehicle platoon formation for fuel efficiency. IEEE Trans. Intell. Transp. Syst. 17(4), 1051\u20131061 (2016). https:\/\/doi.org\/10.1109\/TITS.2015.2492243","journal-title":"IEEE Trans. Intell. Transp. Syst."},{"key":"862_CR24","doi-asserted-by":"publisher","first-page":"4327","DOI":"10.1109\/ACC.2002.1025325","volume-title":"Proceedings of the 2002 American Control Conference (IEEE Cat. No. CH37301)","author":"X.Y. Lu","year":"2002","unstructured":"Lu, X.Y., Hedrick, J., Drew, M.: Acc\/cacc-control design, stability and robust performance. In: Proceedings of the 2002 American Control Conference (IEEE Cat. No. CH37301), vol.\u00a06, pp.\u00a04327\u20134332 (2002). https:\/\/doi.org\/10.1109\/ACC.2002.1025325"},{"key":"862_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.trc.2017.04.005","volume":"80","author":"S. Maiti","year":"2017","unstructured":"Maiti, S., Winter, S., Kulik, L.: A conceptualization of vehicle platoons and platoon operations. Transp. Res., Part C, Emerg. Technol. 80, 1\u201319 (2017)","journal-title":"Transp. Res., Part C, Emerg. Technol."},{"key":"862_CR26","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2025.103300","volume":"244","author":"A. Miller","year":"2025","unstructured":"Miller, A., Porr, B., Valkov, I., Fraser, D., Pagojus, D.: Model checking with memoisation for fast overtaking planning. Sci. Comput. Program. 244, 103300 (2025)","journal-title":"Sci. Comput. Program."},{"issue":"3","key":"862_CR27","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1109\/MIE.2019.2916232","volume":"13","author":"M. Novak","year":"2019","unstructured":"Novak, M., Nyman, U.M., Dragicevic, T., Blaabjerg, F.: Statistical model checking for finite-set model predictive control converters: a tutorial on modeling and performance verification. IEEE Ind. Electron. Mag. 13(3), 6\u201315 (2019). https:\/\/doi.org\/10.1109\/MIE.2019.2916232","journal-title":"IEEE Ind. Electron. Mag."},{"key":"862_CR28","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1109\/IV47402.2020.9304821","volume-title":"2020 IEEE Intelligent Vehicles Symposium (IV)","author":"A. Paigwar","year":"2020","unstructured":"Paigwar, A., Baranov, E., Renzaglia, A., Laugier, C., Legay, A.: Probabilistic collision risk estimation for autonomous driving: validation via statistical model checking. In: 2020 IEEE Intelligent Vehicles Symposium (IV), pp.\u00a0737\u2013743 (2020). https:\/\/doi.org\/10.1109\/IV47402.2020.9304821"},{"key":"862_CR29","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.comcom.2023.09.019","volume":"212","author":"M. Palmieri","year":"2023","unstructured":"Palmieri, M., Quadri, C., Fagiolini, A., Bernardeschi, C.: Co-simulated digital twin on the network edge: a vehicle platoon. Comput. Commun. 212, 35\u201347 (2023). https:\/\/doi.org\/10.1016\/j.comcom.2023.09.019","journal-title":"Comput. Commun."},{"key":"862_CR30","series-title":"Mechanical Engineering Series","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4614-1433-9","volume-title":"Vehicle Dynamics and Control","author":"R. Rajamani","year":"2012","unstructured":"Rajamani, R.: Vehicle Dynamics and Control. Mechanical Engineering Series. Springer, Berlin (2012)"},{"key":"862_CR31","volume-title":"Handbook of Automated Reasoning, Vol. I","author":"A. Robinson","year":"2001","unstructured":"Robinson, A., Voronkov, A.: Handbook of Automated Reasoning, Vol. I. Elsevier, MIT Press (2001)"},{"key":"862_CR32","doi-asserted-by":"publisher","first-page":"291","DOI":"10.23919\/ACC.1990.4790743","volume-title":"1990 American Control Conference","author":"S. Sheikholeslam","year":"1990","unstructured":"Sheikholeslam, S., Desoer, C.A.: Longitudinal control of a platoon of vehicles. In: 1990 American Control Conference, pp.\u00a0291\u2013296 (1990). https:\/\/doi.org\/10.23919\/ACC.1990.4790743"},{"key":"862_CR33","doi-asserted-by":"publisher","first-page":"1806","DOI":"10.1109\/ACC.1995.531196","volume-title":"Proceedings of 1995 American Control Conference - ACC\u201995","author":"D. Swaroop","year":"1995","unstructured":"Swaroop, D., Hedrick, J.: String stability of interconnected systems. In: Proceedings of 1995 American Control Conference - ACC\u201995, vol.\u00a03, pp.\u00a01806\u20131810 (1995). https:\/\/doi.org\/10.1109\/ACC.1995.531196"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-026-00862-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-026-00862-0","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-026-00862-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T07:17:23Z","timestamp":1779779843000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-026-00862-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,4]]},"references-count":33,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2026,4]]}},"alternative-id":["862"],"URL":"https:\/\/doi.org\/10.1007\/s10009-026-00862-0","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,4]]},"assertion":[{"value":"5 March 2026","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 April 2026","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}