{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T01:18:58Z","timestamp":1773883138478,"version":"3.50.1"},"reference-count":100,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"3","license":[{"start":{"date-parts":[[2026,3,1]],"date-time":"2026-03-01T00:00:00Z","timestamp":1772323200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IIEEE Trans. Software Eng."],"published-print":{"date-parts":[[2026,3]]},"DOI":"10.1109\/tse.2026.3654819","type":"journal-article","created":{"date-parts":[[2026,1,16]],"date-time":"2026-01-16T20:49:53Z","timestamp":1768596593000},"page":"889-907","source":"Crossref","is-referenced-by-count":0,"title":["Safety Analysis of Over-the-Air Updates for CPS: A Contract-Driven Approach"],"prefix":"10.1109","volume":"52","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-7152-1389","authenticated-orcid":false,"given":"Nunzio Marco","family":"Bisceglia","sequence":"first","affiliation":[{"name":"University of Bergamo, Bergamo, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-0655-8335","authenticated-orcid":false,"given":"Aurora Francesca","family":"Zanenga","sequence":"additional","affiliation":[{"name":"University of Bergamo, Bergamo, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6526-2544","authenticated-orcid":false,"given":"Mehrnoosh","family":"Askarpour","sequence":"additional","affiliation":[{"name":"General Motors Canada, McMaster University, Hamilton, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-5348-2240","authenticated-orcid":false,"given":"Sahar","family":"Kokaly","sequence":"additional","affiliation":[{"name":"General Motors Canada, McMaster University, Hamilton, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8501-7447","authenticated-orcid":false,"given":"S.","family":"Ramesh","sequence":"additional","affiliation":[{"name":"General Motors, Warren, MI, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6301-3517","authenticated-orcid":false,"given":"Marsha","family":"Chechik","sequence":"additional","affiliation":[{"name":"University of Toronto, Toronto, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5303-8481","authenticated-orcid":false,"given":"Claudio","family":"Menghi","sequence":"additional","affiliation":[{"name":"University of Bergamo, Bergamo, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63588-0"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2011.2160929"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1631\/FITEE.2000311"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1016\/j.future.2016.06.034"},{"key":"ref5","article-title":"A Tesla driver is charged in a crash involving Autopilot that killed 2 people","year":"2022"},{"key":"ref6","article-title":"How terrible software design decisions led to Uber\u2019s deadly 2018 crash","year":"2024"},{"key":"ref7","year":"2011","journal-title":"26262: Road Vehicles-Functional Safety"},{"key":"ref8","volume-title":"Making Embedded Systems: Design Patterns for Great Software","author":"White","year":"2011"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-59897-6"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/3652620.3687815"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-68606-1_9"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1002\/0471739421"},{"key":"ref13","volume-title":"The Safety Critical Systems Handbook: A Straightforward Guide to Functional Safety: IEC 61508 (2010 Edition), IEC 61511 (2015 Edition) and Related Guidance","author":"Smith","year":"2020"},{"key":"ref14","first-page":"384","article-title":"Analysis of safety and security challenges and opportunities related to cyber-physical systems","volume-title":"Process Saf. Environ. Protection","volume":"173","author":"El-Kady","year":"2023"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2014.06.011"},{"issue":"3","key":"ref16","first-page":"217","article-title":"Taming Dr. Frankenstein: Contract-based design for cyber-physical systems","volume-title":"Eur. J. Control","volume":"18","author":"Sangiovanni-Vincentelli","year":"2012"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11936-6_7"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41591-8_26"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2013.2295764"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2015.2453253"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE48619.2023.00030"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30942-8_7"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1145\/3372020.3391557"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1145\/3372020.3391557"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2010.98"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2009.5070544"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1109\/ECBS.2000.839871"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/MEMOCODE51338.2020.9315065"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-89247-0_3"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1109\/FormaliSE58978.2023.00011"},{"key":"ref31","article-title":"Correct-by-construction design of contextual robotic missions using contracts","author":"Mallozzi","year":"2023"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1145\/3704736"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28872-2_18"},{"key":"ref34","article-title":"System composer: Design, analyze, and simulate system and software architectures","year":"2023"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2025.3530820"},{"key":"ref36","article-title":"Use a requirements table block to create formal requirements","year":"2023"},{"key":"ref37","article-title":"Mathworks","year":"2024"},{"key":"ref38","volume-title":"MATLAB and Simulink In-Depth: Model-based Design with Simulink and Stateflow, User Interface, Scripting, Simulation, Visualization and Debugging (English Edition)","author":"Patankar","year":"2022"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1109\/DASC50938.2020.9256753"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.2514\/6.2024-1856"},{"key":"ref41","article-title":"Planning software architecture and modeling patterns for ISO 26262 compliance","author":"Gro\u00df","year":"2020"},{"key":"ref42","article-title":"Identify inconsistent and incomplete formal requirement sets","volume-title":"MathWorks","year":"2024"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1109\/RE48521.2020.00040"},{"key":"ref44","article-title":"Battery warm-up methodologies at subzero temperatures for automotive applications: Recent advances and perspectives","volume-title":"Prog. Energy Combust. Sci.","volume":"77","author":"Hu","year":"2020"},{"key":"ref45","article-title":"Formal requirements elicitation with FRET","volume-title":"Proc. Int. Working Conf. Requirements Eng., Found. Softw. Qual. (REFSQ)","author":"Giannakopoulou","year":"2020"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1145\/3338906.3338920"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE43902.2021.00082"},{"key":"ref49","article-title":"Theano","year":"2023"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1145\/3696630.3728599"},{"key":"ref51","article-title":"antlr","year":"2023"},{"key":"ref52","article-title":"Z3 An efficient SMT solver","year":"2020"},{"key":"ref53","article-title":"CoCoSim: An automated analysis framework for simulink\/stateflow","volume-title":"Proc. Model Based Space Syst. Softw. Eng.-Eur. Space Agency Workshop (MBSE)","author":"Bourbouh","year":"2020"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(02)00374-0"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2021.3101818"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1145\/3368089.3409737"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1145\/3338906.3340444"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1109\/ase.2013.6693137"},{"key":"ref59","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1988.5119"},{"key":"ref60","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2002.1114984"},{"key":"ref61","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48683-6_25"},{"key":"ref62","doi-asserted-by":"publisher","DOI":"10.1145\/990010.990011"},{"key":"ref63","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_32"},{"key":"ref64","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35861-6_11"},{"key":"ref65","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-019-00484-1"},{"key":"ref66","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89363-1_10"},{"key":"ref67","article-title":"Partial behavioural models for requirements and early design","volume-title":"Proc. MMOSS","volume":"6351","author":"Chechik","year":"2006"},{"key":"ref68","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-47813-2_21"},{"key":"ref69","doi-asserted-by":"publisher","DOI":"10.1145\/503502.503503"},{"key":"ref70","volume-title":"Concurrency Verification: Introduction to Compositional and Non-Compositional Methods","volume":"54","author":"de Roever","year":"2001"},{"key":"ref71","doi-asserted-by":"publisher","DOI":"10.1145\/69575.69577"},{"key":"ref72","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008739929481"},{"key":"ref73","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"ref74","doi-asserted-by":"publisher","DOI":"10.1145\/261640.261641"},{"key":"ref75","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.06.022"},{"key":"ref76","doi-asserted-by":"publisher","DOI":"10.1145\/197320.197383"},{"key":"ref77","doi-asserted-by":"publisher","DOI":"10.1109\/TSMCA.2010.2093884"},{"key":"ref78","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-008-0053-x"},{"key":"ref79","doi-asserted-by":"publisher","DOI":"10.1145\/291252.288305"},{"key":"ref80","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75293"},{"key":"ref81","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679387"},{"key":"ref82","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_49"},{"key":"ref83","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2007.21"},{"key":"ref84","doi-asserted-by":"publisher","DOI":"10.1145\/1882291.1882305"},{"key":"ref85","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491414"},{"key":"ref86","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-015-9586-5_6"},{"key":"ref87","article-title":"$\\omega$\u03c9-regular expression synthesis from transition-based B\u00fcchi automata","author":"Pert","year":"2024"},{"key":"ref88","doi-asserted-by":"publisher","DOI":"10.1145\/2430536.2430543"},{"key":"ref89","doi-asserted-by":"publisher","DOI":"10.1145\/1882291.1882305"},{"key":"ref90","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985823"},{"key":"ref91","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.202.5"},{"key":"ref92","doi-asserted-by":"publisher","DOI":"10.1109\/WODES.2006.382401"},{"key":"ref93","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2004.1317443"},{"key":"ref94","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2011.5970509"},{"key":"ref95","doi-asserted-by":"publisher","DOI":"10.1109\/cdc.2016.7798996"},{"key":"ref96","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_14"},{"key":"ref97","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32759-9_33"},{"key":"ref98","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2008.107"},{"key":"ref99","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2001.919093"},{"key":"ref100","article-title":"Experimental results. FOSELAB, University of Bergamo","year":"2025"}],"container-title":["IEEE Transactions on Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/32\/11440029\/11357543.pdf?arnumber=11357543","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T19:38:39Z","timestamp":1773862719000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/11357543\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,3]]},"references-count":100,"journal-issue":{"issue":"3"},"URL":"https:\/\/doi.org\/10.1109\/tse.2026.3654819","relation":{},"ISSN":["0098-5589","1939-3520","2326-3881"],"issn-type":[{"value":"0098-5589","type":"print"},{"value":"1939-3520","type":"electronic"},{"value":"2326-3881","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,3]]}}}