{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,15]],"date-time":"2025-04-15T04:58:08Z","timestamp":1744693088394,"version":"3.37.3"},"reference-count":31,"publisher":"World Scientific Pub Co Pte Ltd","issue":"10","funder":[{"name":"China HGJ Project","award":["2017ZX01038102-002"],"award-info":[{"award-number":["2017ZX01038102-002"]}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61532019"],"award-info":[{"award-number":["61532019"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61472140"],"award-info":[{"award-number":["61472140"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J CIRCUIT SYST COMP"],"published-print":{"date-parts":[[2019,9]]},"abstract":"<jats:p> The time-triggered CAN (TTCAN) protocol has been widely used in the automotive industry to fulfil the safety and real-time requirements of the application. As an extension of the standard CAN protocol, the TTCAN protocol aims to guarantee a safe and deterministic communication by introducing time-triggered messages with respect to a global synchronized time, which are scheduled in independent transmission windows within the system matrix. However, the new features bring more difficulties in designing and verifying the reliable applications in the TTCAN network. In this paper, we first present a formal probabilistic model of the TTCAN protocol with a consideration of its novel features. A TTCAN system consisting of three parts, i.e., a system matrix, an arbitration and some nodes, is modeled as discrete Markov chains model. Furthermore, five probabilistic properties are described and verified in the probabilistic model checker tool PRISM.\u00a0Our work gives a quantitative analysis method for the given requirements, which facilitates the designers to a formal understanding of TTCAN protocol. <\/jats:p>","DOI":"10.1142\/s0218126619501779","type":"journal-article","created":{"date-parts":[[2018,10,23]],"date-time":"2018-10-23T23:06:32Z","timestamp":1540335992000},"page":"1950177","source":"Crossref","is-referenced-by-count":2,"title":["Formal Modeling and Verifying the TTCAN Protocol from a Probabilistic Perspective"],"prefix":"10.1142","volume":"28","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9114-5955","authenticated-orcid":false,"given":"Xin","family":"Li","sequence":"first","affiliation":[{"name":"Soft\/Hardware Co-Design Engineering Research Center, East China Normal University, Shanghai 200062, P. R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0358-0691","authenticated-orcid":false,"given":"Jian","family":"Guo","sequence":"additional","affiliation":[{"name":"Soft\/Hardware Co-Design Engineering Research Center, East China Normal University, Shanghai 200062, P. R. China"},{"name":"National Trusted Embedded Software, Engineering Technology Research Center, East China Normal University, Shanghai 200062, P. R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yongxin","family":"Zhao","sequence":"additional","affiliation":[{"name":"Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, P. R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaoran","family":"Zhu","sequence":"additional","affiliation":[{"name":"Soft\/Hardware Co-Design Engineering Research Center, East China Normal University, Shanghai 200062, P. R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"219","published-online":{"date-parts":[[2019,9,26]]},"reference":[{"key":"S0218126619501779BIB001","first-page":"5","volume-title":"14th Int. VDI Congress Electronic Systems for Vehicles","author":"F\u00fcrst S.","year":"2009"},{"key":"S0218126619501779BIB002","doi-asserted-by":"publisher","DOI":"10.1049\/cce:19990304"},{"key":"S0218126619501779BIB003","doi-asserted-by":"publisher","DOI":"10.1109\/ICSTCC.2016.7790660"},{"volume-title":"ISO11898: Road Vehicles \u2014 Controller Area Network (CAN) \u2014 Part 4: Time-Triggered Communication","year":"2004","author":"ISO","key":"S0218126619501779BIB004"},{"key":"S0218126619501779BIB005","doi-asserted-by":"publisher","DOI":"10.1016\/S0141-9331(01)00148-X"},{"key":"S0218126619501779BIB006","doi-asserted-by":"publisher","DOI":"10.1109\/HASE.2001.966806"},{"key":"S0218126619501779BIB007","first-page":"F2004F442","volume-title":"In FISITA 2004 \u2014 World Automotive Congress","author":"Krakora J.","year":"2004"},{"key":"S0218126619501779BIB008","doi-asserted-by":"publisher","DOI":"10.1016\/S1474-6670(17)36111-6"},{"key":"S0218126619501779BIB009","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2014.12.004"},{"key":"S0218126619501779BIB010","doi-asserted-by":"publisher","DOI":"10.1142\/S0218126616501371"},{"key":"S0218126619501779BIB011","doi-asserted-by":"publisher","DOI":"10.1142\/S0218126613400318"},{"key":"S0218126619501779BIB012","doi-asserted-by":"publisher","DOI":"10.1109\/ICNICONSMCL.2006.150"},{"key":"S0218126619501779BIB013","first-page":"125","volume-title":"Third Int. Conf. Quantitative Evaluation of Systems, 2006. QEST 2006","author":"Behrmann G.","year":"2006"},{"key":"S0218126619501779BIB014","doi-asserted-by":"publisher","DOI":"10.1109\/ICCTA.2007.4"},{"key":"S0218126619501779BIB015","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2007.27"},{"key":"S0218126619501779BIB016","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2014.8"},{"key":"S0218126619501779BIB018","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.04.012"},{"key":"S0218126619501779BIB019","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_8"},{"key":"S0218126619501779BIB020","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45605-8_11"},{"key":"S0218126619501779BIB021","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"key":"S0218126619501779BIB022","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786853"},{"key":"S0218126619501779BIB023","doi-asserted-by":"publisher","DOI":"10.1142\/S0218126615500917"},{"key":"S0218126619501779BIB024","doi-asserted-by":"publisher","DOI":"10.1142\/S021812661850086X"},{"volume-title":"Principles of Model Checking","year":"2008","author":"Baier C.","key":"S0218126619501779BIB025"},{"key":"S0218126619501779BIB026","doi-asserted-by":"publisher","DOI":"10.1145\/2744769.2744906"},{"key":"S0218126619501779BIB027","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934574"},{"key":"S0218126619501779BIB028","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"S0218126619501779BIB029","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46029-2_13"},{"key":"S0218126619501779BIB030","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2014.2327389"},{"key":"S0218126619501779BIB031","first-page":"710","volume-title":"Proc. of 4th FET2001, IFAC Conf. on Fieldbus System and their Application","author":"Fonseca J.","year":"2002"},{"key":"S0218126619501779BIB032","doi-asserted-by":"publisher","DOI":"10.1287\/opre.26.1.127"}],"container-title":["Journal of Circuits, Systems and Computers"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0218126619501779","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,26]],"date-time":"2019-09-26T03:12:24Z","timestamp":1569467544000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0218126619501779"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,9]]},"references-count":31,"journal-issue":{"issue":"10","published-print":{"date-parts":[[2019,9]]}},"alternative-id":["10.1142\/S0218126619501779"],"URL":"https:\/\/doi.org\/10.1142\/s0218126619501779","relation":{},"ISSN":["0218-1266","1793-6454"],"issn-type":[{"type":"print","value":"0218-1266"},{"type":"electronic","value":"1793-6454"}],"subject":[],"published":{"date-parts":[[2019,9]]}}}