{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T14:05:02Z","timestamp":1730297102713,"version":"3.28.0"},"reference-count":20,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018,10]]},"DOI":"10.1109\/smartworld.2018.00086","type":"proceedings-article","created":{"date-parts":[[2018,12,6]],"date-time":"2018-12-06T19:38:21Z","timestamp":1544125101000},"page":"308-315","source":"Crossref","is-referenced-by-count":0,"title":["Executable Micro-Architecture Modeling and Automatic Verification of EtherCAT"],"prefix":"10.1109","author":[{"given":"Shun","family":"Wang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaojuan","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yong","family":"Guan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rui","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jie","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_20"},{"key":"ref11","first-page":"113","volume":"43","author":"li","year":"2016","journal-title":"xmas-based formal verification of spacewire credit logic Computer Science"},{"key":"ref12","first-page":"1","author":"van","year":"2014","journal-title":"Inference of channel types in micro-architectural models of on-chip communication networks in International Conference on Very Large Scale Integration"},{"key":"ref13","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3188-0","author":"kaufmann","year":"2000","journal-title":"Computer-Aided reasoning ACL2 case studies Kluwer Academic Publishers"},{"key":"ref14","first-page":"127","author":"borrione","year":"2007","journal-title":"A generic model for formally verifying noc communication architectures A case study in International Symposium on Networks-On-Chip"},{"journal-title":"Symbolic Simulation An ACL2 Approach Springer Berlin Heidelberg","year":"1998","author":"moore","key":"ref15"},{"key":"ref16","first-page":"147","volume":"40","author":"chatterjee","year":"2012","journal-title":"Automatic generation of inductive invariants from high-level microarchitectural models of communication fabrics Formal Methods in System Design"},{"key":"ref17","first-page":"1419","author":"burns","year":"2015","journal-title":"Gals synthesis and verification for xmas models"},{"key":"ref18","first-page":"79","volume":"29","author":"shan","year":"2007","journal-title":"Ethercat-industrial ethernet fieldbus and its driver design Manufacturing automation"},{"journal-title":"EtherCAT Technology Group","year":"0","key":"ref19"},{"key":"ref4","first-page":"42","author":"chatterjee","year":"2010","journal-title":"Quick formal modeling of communication fabrics to enable verification"},{"key":"ref3","first-page":"1","author":"melnykov","year":"2011","journal-title":"Biped robot “rotto” Design simulation experiments"},{"key":"ref6","first-page":"214","author":"gotmanov","year":"2011","journal-title":"Verifying deadlock-freedom of communication fabrics in Verification Model Checking and Abstract Interpretation - International Conference VMCAI 2011"},{"key":"ref5","first-page":"223","author":"verbeek","year":"2011","journal-title":"Hunting deadlocks efficiently in microarchitec-tural models of communication fabrics"},{"journal-title":"A formalisation of xmas Eprint Arxiv (Proc ACL2 2013)","year":"0","author":"gastel","key":"ref8"},{"key":"ref7","first-page":"792","author":"das","year":"2017","journal-title":"xmas based accurate modeling and progress verification of nocs in International Symposium on VLSI Design and Test"},{"journal-title":"Walking robot anton design simulation experiments","year":"2015","author":"konyev","key":"ref2"},{"key":"ref1","first-page":"1238","volume":"34","author":"liu","year":"2013","journal-title":"Research of robot control bus scheme based on ethercat Computer engineering and design"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1145\/2071356.2071357"},{"key":"ref20","first-page":"905","author":"ray","year":"2012","journal-title":"Scalable progress verification in credit-based flow-control systems"}],"event":{"name":"2018 IEEE SmartWorld, Ubiquitous Intelligence & Computing, Advanced & Trusted Computing, Scalable Computing & Communications, Cloud & Big Data Computing, Internet of People and Smart City Innovation (SmartWorld\/SCALCOM\/UIC\/ATC\/CBDCom\/IOP\/SCI)","start":{"date-parts":[[2018,10,8]]},"location":"Guangzhou, China","end":{"date-parts":[[2018,10,12]]}},"container-title":["2018 IEEE SmartWorld, Ubiquitous Intelligence & Computing, Advanced & Trusted Computing, Scalable Computing & Communications, Cloud & Big Data Computing, Internet of People and Smart City Innovation (SmartWorld\/SCALCOM\/UIC\/ATC\/CBDCom\/IOP\/SCI)"],"original-title":[],"link":[{"URL":"https:\/\/2.zoppoz.workers.dev:443\/http\/xplorestaging.ieee.org\/ielx7\/8533596\/8559978\/08560064.pdf?arnumber=8560064","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,26]],"date-time":"2022-01-26T21:48:24Z","timestamp":1643233704000},"score":1,"resource":{"primary":{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/ieeexplore.ieee.org\/document\/8560064\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10]]},"references-count":20,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1109\/smartworld.2018.00086","relation":{},"subject":[],"published":{"date-parts":[[2018,10]]}}}