{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,2]],"date-time":"2025-12-02T15:01:22Z","timestamp":1764687682158,"version":"3.28.0"},"reference-count":30,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015,4]]},"DOI":"10.1109\/infocom.2015.7218491","type":"proceedings-article","created":{"date-parts":[[2015,8,24]],"date-time":"2015-08-24T21:33:36Z","timestamp":1440452016000},"page":"1167-1175","source":"Crossref","is-referenced-by-count":4,"title":["VeRV: A temporal and data-concerned verification framework for the vehicle bus systems"],"prefix":"10.1109","author":[{"given":"Shuo","family":"Zhang","sequence":"first","affiliation":[]},{"given":"Fei","family":"He","sequence":"additional","affiliation":[]},{"given":"Ming","family":"Gu","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1109\/NOMS.2010.5488464"},{"journal-title":"The glory of the past","year":"1985","author":"lichtenstein","key":"ref10"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-011-0198-6"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1145\/2000799.2000800"},{"journal-title":"Model checking","year":"1999","author":"clarke","key":"ref13"},{"key":"ref14","first-page":"42","article-title":"Finite-state analysis of the CAN bus protocol","author":"van","year":"2001","journal-title":"Sixth IEEE International Symposium on High Assurance Systems Engineering"},{"key":"ref15","doi-asserted-by":"crossref","first-page":"390","DOI":"10.1007\/3-540-61474-5_86","article-title":"The Murphi verification system","author":"dill","year":"1996","journal-title":"Proceedings of Computer Aided Verification"},{"key":"ref16","first-page":"114","article-title":"Formally specified monitoring of temporal properties","author":"kim","year":"1999","journal-title":"Proceedings of the 11th Euromicro Conference on Real-Time Systems"},{"key":"ref17","first-page":"294","article-title":"Runtime assurance based on formal specifications","author":"lee","year":"1999","journal-title":"Departmental Papers (CIS)"},{"key":"ref18","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1007\/10722468_15","article-title":"Using runtime analysis to guide model checking of java programs","author":"havelund","year":"2000","journal-title":"SPIN Model Checking and Software Verification"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/1795194.1795214"},{"key":"ref28","doi-asserted-by":"crossref","first-page":"71","DOI":"10.3233\/JCS-2002-101-204","article-title":"STATL: An attack language for state-based intrusion detection","volume":"10","author":"eckmann","year":"2002","journal-title":"Journal of Computer Security"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2010.64"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1016\/S1389-1286(99)00112-7"},{"key":"ref3","article-title":"Generic application-level protocol analyzer and its language","author":"borisov","year":"2007","journal-title":"NDSS"},{"article-title":"Portable system tester","year":"0","author":"ltd","key":"ref6"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/1030194.1015489"},{"article-title":"PTS 402: Portable test system","year":"0","author":"systems","key":"ref5"},{"year":"0","key":"ref8","article-title":"TCNalyzer"},{"year":"0","key":"ref7","article-title":"TCN bus tester"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/40.918005"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029846"},{"article-title":"IEC 61375–1, part 1: Train communication network","year":"1999","author":"commission","key":"ref1"},{"key":"ref20","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1145\/2000367.2000368","article-title":"To-ward online hybrid systems model checking of cyber-physical systems' time-bounded short-run behavior","volume":"8","author":"bu","year":"2011","journal-title":"ACM SIGBED Review"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00254-3"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2013.50"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1145\/347057.347563"},{"journal-title":"CSN 1 Specification Version 2 0 Cell & Sys","year":"1998","author":"mouly","key":"ref23"},{"key":"ref26","article-title":"Intrusion detection systems: A survey and taxonomy","author":"axelsson","year":"2000","journal-title":"Technical Report Tech Rep"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/1177080.1177119"}],"event":{"name":"IEEE INFOCOM 2015 - IEEE Conference on Computer Communications","start":{"date-parts":[[2015,4,26]]},"location":"Kowloon, Hong Kong","end":{"date-parts":[[2015,5,1]]}},"container-title":["2015 IEEE Conference on Computer Communications (INFOCOM)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/7172813\/7218353\/07218491.pdf?arnumber=7218491","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,29]],"date-time":"2019-08-29T19:51:12Z","timestamp":1567108272000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7218491\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,4]]},"references-count":30,"URL":"https:\/\/doi.org\/10.1109\/infocom.2015.7218491","relation":{},"subject":[],"published":{"date-parts":[[2015,4]]}}}