{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,29]],"date-time":"2024-10-29T21:23:29Z","timestamp":1730237009961,"version":"3.28.0"},"reference-count":12,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007,3]]},"DOI":"10.1109\/iccta.2007.4","type":"proceedings-article","created":{"date-parts":[[2007,4,19]],"date-time":"2007-04-19T20:38:58Z","timestamp":1177015138000},"page":"77-81","source":"Crossref","is-referenced-by-count":11,"title":["A Finite State Analysis of Time-Triggered CAN (TTCAN) Protocol Using Spin"],"prefix":"10.1109","author":[{"given":"Indranil","family":"Saha","sequence":"first","affiliation":[]},{"given":"Suman","family":"Roy","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"3","article-title":"Modeling and verification of a fault-tolerant real-time startup protocol using calendar automata","author":"dutertre","year":"2004","journal-title":"Proc FORMATS\/FTRTFT"},{"key":"2","first-page":"423","article-title":"Integrating real time into spin: A prototype implementation","author":"bos?anac?ki","year":"1998","journal-title":"Proceedings of the FORTE\/PSTV XVIII conference"},{"journal-title":"Can system engineering - from theory to practical applications","year":"1997","author":"lawrenz","key":"10"},{"key":"1","first-page":"307","article-title":"Discrete-time promela and spin","volume":"1486","author":"bos?anac?ki","year":"1998","journal-title":"LNCS"},{"year":"0","key":"7"},{"journal-title":"The SPIN Model Checker Primer and Reference Manual","year":"2003","author":"holtzman","key":"6"},{"key":"5","first-page":"694","article-title":"Fast ltl to bu?chi automata translation","volume":"2076","author":"gastin","year":"0","journal-title":"LNCS"},{"key":"4","article-title":"Time triggered communication on can (timetriggered can-ttcan)","author":"fu?hrer","year":"0","journal-title":"Robert Bosch GmbH"},{"key":"9","article-title":"Verifying real-time properties of can bus by timed automata","author":"krakora","year":"2004","journal-title":"Proceedings of FISITA"},{"key":"8","article-title":"Timed automata approach to can verification","author":"krakora","year":"2004","journal-title":"Proceedings of 11th IFAC Symposium on Information Control Problems in Manufacturing"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1109\/ICNICONSMCL.2006.150"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1109\/HASE.2001.966806"}],"event":{"name":"2007 International Conference on Computing: Theory and Applications (ICCTA'07)","start":{"date-parts":[[2007,3,5]]},"location":"Kolkata, India","end":{"date-parts":[[2007,3,7]]}},"container-title":["2007 International Conference on Computing: Theory and Applications (ICCTA'07)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/4127325\/4127326\/04127346.pdf?arnumber=4127346","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,3,15]],"date-time":"2017-03-15T22:38:39Z","timestamp":1489617519000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/4127346\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,3]]},"references-count":12,"URL":"https:\/\/doi.org\/10.1109\/iccta.2007.4","relation":{},"subject":[],"published":{"date-parts":[[2007,3]]}}}