{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,30]],"date-time":"2024-08-30T11:41:29Z","timestamp":1725018089050},"reference-count":60,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"8","license":[{"start":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T00:00:00Z","timestamp":1659312000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T00:00:00Z","timestamp":1659312000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T00:00:00Z","timestamp":1659312000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"name":"SEADA, Icelandic Research Fund","award":["163205-051"]},{"name":"KKS SACSys Synergy Project"},{"name":"KKS DPAC Project"},{"name":"Malardalen University"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IIEEE Trans. Software Eng."],"published-print":{"date-parts":[[2022,8,1]]},"DOI":"10.1109\/tse.2021.3069192","type":"journal-article","created":{"date-parts":[[2021,3,29]],"date-time":"2021-03-29T21:04:05Z","timestamp":1617051845000},"page":"2732-2747","source":"Crossref","is-referenced-by-count":1,"title":["Magnifier: A Compositional Analysis Approach for Autonomous Traffic Control"],"prefix":"10.1109","volume":"48","author":[{"ORCID":"http:\/\/orcid.org\/0000-0001-9576-2478","authenticated-orcid":false,"given":"Maryam","family":"Bagheri","sequence":"first","affiliation":[{"name":"Department of Computer Engineering, Sharif University of Technology, Tehran, Iran"}]},{"ORCID":"http:\/\/orcid.org\/0000-0001-5478-0987","authenticated-orcid":false,"given":"Marjan","family":"Sirjani","sequence":"additional","affiliation":[{"name":"School of IDT, Mälardalen University, Västerås, Sweden"}]},{"given":"Ehsan","family":"Khamespanah","sequence":"additional","affiliation":[{"name":"School of Electrical and Computer Engineering, University of Tehran, Tehran, Iran"}]},{"ORCID":"http:\/\/orcid.org\/0000-0002-5321-9343","authenticated-orcid":false,"given":"Christel","family":"Baier","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Technical University of Dresden, Dresden, Germany"}]},{"ORCID":"http:\/\/orcid.org\/0000-0002-6803-6750","authenticated-orcid":false,"given":"Ali","family":"Movaghar","sequence":"additional","affiliation":[{"name":"Department of Computer Engineering, Sharif University of Technology, Tehran, Iran"}]}],"member":"263","reference":[{"doi-asserted-by":"publisher","key":"ref1","DOI":"10.1016\/j.jss.2018.05.034"},{"doi-asserted-by":"publisher","key":"ref2","DOI":"10.1007\/978-3-319-08915-7_4"},{"doi-asserted-by":"publisher","key":"ref3","DOI":"10.1007\/978-3-319-57666-4_15"},{"year":"1972","author":"Hewitt","article-title":"Description and theoretical analysis (using schemata) of planner: A language for proving theorems and manipulating models in a robot","key":"ref4"},{"doi-asserted-by":"publisher","key":"ref5","DOI":"10.7551\/mitpress\/1086.001.0001"},{"doi-asserted-by":"publisher","key":"ref6","DOI":"10.1109\/REAL.2003.1253264"},{"doi-asserted-by":"publisher","key":"ref7","DOI":"10.1109\/LICS.1989.39190"},{"volume-title":"System Design, Modeling, and Simulation: Using Ptolemy II","year":"2014","author":"Ptolemaeus","key":"ref8"},{"doi-asserted-by":"publisher","key":"ref9","DOI":"10.1109\/DS-RT47707.2019.8958682"},{"doi-asserted-by":"publisher","key":"ref10","DOI":"10.1007\/978-3-540-88387-6_7"},{"volume-title":"Proc. CEUR Workshop Proc.","author":"Bensalem","first-page":"5","article-title":"Compositional verification of timed systems","key":"ref11"},{"doi-asserted-by":"publisher","key":"ref12","DOI":"10.1016\/j.pmcj.2014.09.009"},{"doi-asserted-by":"publisher","key":"ref13","DOI":"10.1007\/978-3-642-35813-5_1"},{"doi-asserted-by":"publisher","key":"ref14","DOI":"10.1145\/3166227.3166233"},{"volume-title":"North Atlantic Operations and Airspace Manual","year":"2016","key":"ref15"},{"key":"ref16","first-page":"3","article-title":"Sat-based reachability checking for timed automata with discrete data","volume":"79","author":"Zbrzezny","year":"2007","journal-title":"Fundamenta Informaticae"},{"doi-asserted-by":"publisher","key":"ref17","DOI":"10.1007\/3-540-48778-6_18"},{"doi-asserted-by":"publisher","key":"ref18","DOI":"10.1109\/tse.2021.3069192"},{"volume-title":"Dept. Comput. Sci., Aalborg Univ., Aalborg, Denmark","year":"2006","author":"Behrmann","article-title":"A tutorial on uppaal 4.0","key":"ref19"},{"doi-asserted-by":"publisher","key":"ref20","DOI":"10.1109\/MC.2003.1160055"},{"key":"ref21","first-page":"108","article-title":"Timed interfaces","volume-title":"Embedded Software","author":"Henzinger","year":"2002"},{"doi-asserted-by":"publisher","key":"ref22","DOI":"10.47893\/ijcct.2016.1384"},{"doi-asserted-by":"publisher","key":"ref23","DOI":"10.1145\/2000367.2000368"},{"doi-asserted-by":"publisher","key":"ref24","DOI":"10.1109\/CDC.2006.377796"},{"doi-asserted-by":"publisher","key":"ref25","DOI":"10.1016\/j.ress.2015.09.014"},{"doi-asserted-by":"publisher","key":"ref26","DOI":"10.1145\/2461328.2461350"},{"doi-asserted-by":"publisher","key":"ref27","DOI":"10.1109\/TCST.2012.2220773"},{"doi-asserted-by":"publisher","key":"ref28","DOI":"10.1007\/978-3-540-75221-9_6"},{"doi-asserted-by":"publisher","key":"ref29","DOI":"10.1016\/j.scico.2014.04.002"},{"doi-asserted-by":"publisher","key":"ref30","DOI":"10.1016\/j.csi.2011.02.006"},{"doi-asserted-by":"publisher","key":"ref31","DOI":"10.2514\/1.2556"},{"doi-asserted-by":"publisher","key":"ref32","DOI":"10.1007\/978-3-030-02146-7_1"},{"doi-asserted-by":"publisher","key":"ref33","DOI":"10.1145\/1059816.1059823"},{"doi-asserted-by":"publisher","key":"ref34","DOI":"10.1007\/s10703-006-0014-1"},{"doi-asserted-by":"publisher","key":"ref35","DOI":"10.1109\/ROBOT.2004.1302413"},{"doi-asserted-by":"publisher","key":"ref36","DOI":"10.1109\/ECC.2016.7810369"},{"volume-title":"Proc. ACM\/IEEE 8th Int. Conf. Cyber-Phys. Syst. (ICCPS)","author":"Desai","first-page":"239","article-title":"Drona: A framework for safe distributed mobile robotics","key":"ref37"},{"doi-asserted-by":"publisher","key":"ref38","DOI":"10.1016\/j.jss.2012.03.007"},{"doi-asserted-by":"publisher","key":"ref39","DOI":"10.1007\/978-3-030-31517-7_1"},{"issue":"4","key":"ref40","first-page":"385","article-title":"Modeling and verification of reactive systems using Rebeca","volume":"63","author":"Sirjani","year":"2004","journal-title":"Fundamenta Informaticae"},{"doi-asserted-by":"publisher","key":"ref41","DOI":"10.1007\/978-3-642-35632-2_30"},{"doi-asserted-by":"publisher","key":"ref42","DOI":"10.1007\/978-3-642-36249-1_2"},{"doi-asserted-by":"publisher","key":"ref43","DOI":"10.1007\/978-3-642-35813-5_8"},{"doi-asserted-by":"publisher","key":"ref44","DOI":"10.1016\/j.infsof.2017.09.008"},{"doi-asserted-by":"publisher","key":"ref45","DOI":"10.1109\/SEAMS.2017.18"},{"doi-asserted-by":"publisher","key":"ref46","DOI":"10.1007\/978-3-642-36249-1_5"},{"doi-asserted-by":"publisher","key":"ref47","DOI":"10.1145\/2786805.2786853"},{"doi-asserted-by":"publisher","key":"ref48","DOI":"10.1109\/SEAMS.2012.6224401"},{"doi-asserted-by":"publisher","key":"ref49","DOI":"10.1007\/978-3-540-74792-5_5"},{"doi-asserted-by":"publisher","key":"ref50","DOI":"10.1007\/11767954_18"},{"doi-asserted-by":"publisher","key":"ref51","DOI":"10.1016\/j.scico.2014.07.005"},{"doi-asserted-by":"publisher","key":"ref52","DOI":"10.1007\/978-3-319-30734-3_25"},{"doi-asserted-by":"publisher","key":"ref53","DOI":"10.1109\/SEAMS.2009.5069079"},{"doi-asserted-by":"publisher","key":"ref54","DOI":"10.1007\/s10009-012-0237-y"},{"doi-asserted-by":"publisher","key":"ref55","DOI":"10.1007\/978-3-540-73368-3_38"},{"doi-asserted-by":"publisher","key":"ref56","DOI":"10.1007\/978-3-642-36249-1_6"},{"volume-title":"Proc. IEEE\/ACM 13th Int. Symp. Softw. Eng. Adaptive Self-Manag. Syst. (SEAMS)","author":"Borda","first-page":"1","article-title":"Compositional verification of self-adaptive cyber-physical systems","key":"ref57"},{"doi-asserted-by":"publisher","key":"ref58","DOI":"10.1145\/1755952.1755967"},{"year":"2018","author":"Bujtor","article-title":"Modal interface automata: A theory for heterogeneous specification of parallel systems","key":"ref59"},{"doi-asserted-by":"publisher","key":"ref60","DOI":"10.4204\/eptcs.46.1"}],"container-title":["IEEE Transactions on Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/32\/9857502\/09388903.pdf?arnumber=9388903","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,30]],"date-time":"2024-08-30T10:40:47Z","timestamp":1725014447000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9388903\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,1]]},"references-count":60,"journal-issue":{"issue":"8"},"URL":"http:\/\/dx.doi.org\/10.1109\/tse.2021.3069192","relation":{},"ISSN":["0098-5589","1939-3520","2326-3881"],"issn-type":[{"type":"print","value":"0098-5589"},{"type":"electronic","value":"1939-3520"},{"type":"electronic","value":"2326-3881"}],"subject":[],"published":{"date-parts":[[2022,8,1]]}}}
