{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:58:34Z","timestamp":1776333514751,"version":"3.51.2"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319929699","type":"print"},{"value":"9783319929705","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-92970-5_14","type":"book-chapter","created":{"date-parts":[[2018,5,29]],"date-time":"2018-05-29T12:54:12Z","timestamp":1527598452000},"page":"223-238","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Formal Verification of Platoon Control Strategies"],"prefix":"10.1007","author":[{"given":"Adnan","family":"Rashid","sequence":"first","affiliation":[]},{"given":"Umair","family":"Siddique","sequence":"additional","affiliation":[]},{"given":"Osman","family":"Hasan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,5,30]]},"reference":[{"key":"14_CR1","unstructured":"http:\/\/www.driverless-future.com\/?page_id=384 (2018)"},{"key":"14_CR2","unstructured":"https:\/\/www.technologyreview.com\/s\/602196\/2021-may-be-the-year-of-the-fully-autonomous-car\/ (2018)"},{"key":"14_CR3","unstructured":"https:\/\/phys.org\/news\/2017-09-self-driving-cars-road-toll.html (2018)"},{"issue":"001","key":"14_CR4","first-page":"1","volume":"3","author":"Z Changfu","year":"2006","unstructured":"Changfu, Z., Kai, L.: Development of the drive-by-wire technology. Automobile Technol. 3(001), 1\u20135 (2006)","journal-title":"Automobile Technol."},{"issue":"4","key":"14_CR5","doi-asserted-by":"crossref","first-page":"429","DOI":"10.1109\/TITS.2006.884615","volume":"7","author":"B Arem Van","year":"2006","unstructured":"Van Arem, B., Van Driel, C.J.G., Visser, R.: The impact of cooperative adaptive cruise control on traffic-flow characteristics. Trans. Intell. Transp. Syst. 7(4), 429\u2013436 (2006)","journal-title":"Trans. Intell. Transp. Syst."},{"key":"14_CR6","unstructured":"Kawazoe, H., Shimakage, M., Sadano, O., Sato, S.: Lane Keeping Assistance System and Method for Automotive Vehicle, US Patent 6,493,619, 10 December 2002"},{"issue":"1","key":"14_CR7","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1109\/TITS.2011.2179936","volume":"13","author":"P Fernandes","year":"2012","unstructured":"Fernandes, P., Nunes, U.: Platooning with IVC-enabled autonomous vehicles: strategies to mitigate communication delays, improve safety and traffic flow. Trans. Intell. Transp. Syst. 13(1), 91\u2013106 (2012)","journal-title":"Trans. Intell. Transp. Syst."},{"issue":"1","key":"14_CR8","doi-asserted-by":"crossref","first-page":"74","DOI":"10.1109\/MCOM.2006.1580935","volume":"44","author":"S Biswas","year":"2006","unstructured":"Biswas, S., Tatchikou, R., Dion, F.: Vehicle-to-vehicle wireless communication protocols for enhancing highway traffic safety. Commun. Mag. 44(1), 74\u201382 (2006)","journal-title":"Commun. Mag."},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Yi, J., Alvarez, L., Horowitz, R., Canudas De Wit, C.: Adaptive emergency braking control using a dynamic tire\/road Friction Model. In: Decision and Control, vol. 1, pp. 456\u2013461. IEEE (2000)","DOI":"10.1109\/CDC.2000.912806"},{"issue":"5","key":"14_CR10","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1080\/00423119808969457","volume":"30","author":"J Eyre","year":"1998","unstructured":"Eyre, J., Yanakiev, D., Kanellakopoulos, I.: A simplified framework for string stability analysis of automated vehicles. Veh. Syst. Dyn. 30(5), 375\u2013405 (1998)","journal-title":"Veh. Syst. Dyn."},{"issue":"9","key":"14_CR11","doi-asserted-by":"crossref","first-page":"2100","DOI":"10.1109\/TAC.2009.2026934","volume":"54","author":"P Barooah","year":"2009","unstructured":"Barooah, P., Mehta, P.G., Hespanha, J.P.: Mistuning-based control design to improve closed-loop stability margin of vehicular platoons. Trans. Autom. Control 54(9), 2100\u20132113 (2009)","journal-title":"Trans. Autom. Control"},{"key":"14_CR12","doi-asserted-by":"crossref","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)","journal-title":"Sci. Comput. Program."},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"Dolginova, E.: Safety Verification for Automated Vehicle Maneuvers. Ph.D thesis, Massachusetts Institute of Technology (1998)","DOI":"10.1007\/BFb0014723"},{"key":"14_CR14","unstructured":"Wongpiromsarn, T., Murray, R.M.: Formal verification of an autonomous vehicle system. In: Conference on Decision and Control (2008)"},{"key":"14_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/978-3-642-31137-6_32","volume-title":"Computational Science and Its Applications \u2013 ICCSA 2012","author":"A Mashkoor","year":"2012","unstructured":"Mashkoor, A., Hasan, O.: Formal probabilistic analysis of cyber-physical transportation systems. In: Murgante, B., Gervasi, O., Misra, S., Nedjah, N., Rocha, A.M.A.C., Taniar, D., Apduhan, B.O. (eds.) ICCSA 2012. LNCS, vol. 7335, pp. 419\u2013434. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31137-6_32"},{"key":"14_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"Formal Methods in Computer-Aided Design","author":"J Harrison","year":"1996","unstructured":"Harrison, J.: HOL light: a tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 265\u2013269. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/BFb0031814"},{"key":"14_CR17","unstructured":"Kumar, R.: Self-compilation and Self-verification. Technical report, University of Cambridge, Computer Laboratory (2016)"},{"issue":"2","key":"14_CR18","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/s10817-012-9250-9","volume":"50","author":"J Harrison","year":"2013","unstructured":"Harrison, J.: The HOL light theory of euclidean space. J. Autom. Reasoning 50(2), 173\u2013190 (2013)","journal-title":"J. Autom. Reasoning"},{"key":"14_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"744","DOI":"10.1007\/978-3-642-45221-5_50","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"SH Taqdees","year":"2013","unstructured":"Taqdees, S.H., Hasan, O.: Formalization of laplace transform using the multivariable calculus theory of HOL-Light. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 744\u2013758. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-45221-5_50"},{"key":"14_CR20","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-319-62075-6_22","volume-title":"Intelligent Computer Mathematics","author":"A Rashid","year":"2017","unstructured":"Rashid, A., Hasan, O.: Formalization of transform methods using HOL Light. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds.) CICM 2017. LNCS (LNAI), vol. 10383, pp. 319\u2013332. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-62075-6_22"},{"key":"14_CR21","unstructured":"Rashid, A.: Formal Verification of Platoon Control Strategies (2018). http:\/\/save.seecs.nust.edu.pk\/projects\/fvpcs\/"},{"key":"14_CR22","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511576430","volume-title":"Handbook of Practical Logic and Automated Reasoning","author":"J Harrison","year":"2009","unstructured":"Harrison, J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, Cambridge (2009)"},{"key":"14_CR23","unstructured":"A History of OCaml (2015). http:\/\/ocaml.org\/learn\/history.html"},{"issue":"4","key":"14_CR24","first-page":"14:1","volume":"20","author":"A Bauer","year":"2011","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. Trans. Softw. Eng. Methodol. 20(4), 14:1\u201314:64 (2011)","journal-title":"Trans. Softw. Eng. Methodol."},{"key":"14_CR25","doi-asserted-by":"crossref","unstructured":"Havelund, K., Rosu, G.: Monitoring programs using rewriting. In: Automated Software Engineering, pp. 135\u2013143 (2001)","DOI":"10.1109\/ASE.2001.989799"},{"key":"14_CR26","unstructured":"Dunn, D.D.: Attacker-induced Traffic Flow Instability in a Stream of Automated Vehicles. Utah State University (2015)"},{"key":"14_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/978-3-319-08970-6_31","volume-title":"Interactive Theorem Proving","author":"U Siddique","year":"2014","unstructured":"Siddique, U., Mahmoud, M.Y., Tahar, S.: On the formalization of Z-Transform in HOL. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 483\u2013498. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08970-6_31"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-92970-5_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:38:47Z","timestamp":1751661527000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-92970-5_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319929699","9783319929705"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-92970-5_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}