{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T09:10:01Z","timestamp":1746177001655,"version":"3.40.4"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319054155"},{"type":"electronic","value":"9783319054162"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-05416-2_4","type":"book-chapter","created":{"date-parts":[[2014,4,5]],"date-time":"2014-04-05T05:41:09Z","timestamp":1396676469000},"page":"36-53","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["An UPPAAL Framework for Model Checking Automotive Systems with FlexRay Protocol"],"prefix":"10.1007","author":[{"given":"Xiaoyun","family":"Guo","sequence":"first","affiliation":[]},{"given":"Hsin-Hung","family":"Lin","sequence":"additional","affiliation":[]},{"given":"Kenro","family":"Yatake","sequence":"additional","affiliation":[]},{"given":"Toshiaki","family":"Aoki","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,4,6]]},"reference":[{"unstructured":"Altran Technologies: FlexRay Specifications Version 3.0.1 (2010)","key":"4_CR1"},{"issue":"4","key":"4_CR2","doi-asserted-by":"publisher","first-page":"921","DOI":"10.1109\/TASE.2010.2050199","volume":"7","author":"H Bel Mokadem","year":"2010","unstructured":"Bel Mokadem, H., Berard, B., Gourcuff, V., De Smet, O., Roussel, J.-M.: Verification of a timed multitask system with UPPAAL. IEEE Trans. Autom. Sci. Eng. 7(4), 921\u2013932 (2010)","journal-title":"IEEE Trans. Autom. Sci. Eng."},{"key":"4_CR3","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/BFb0020949","volume-title":"Hybrid Systems III","author":"J Bengtsson","year":"1996","unstructured":"Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: UPPAAL - a tool suite for automatic verification of real-time systems. Hybrid Systems III. LNCS, vol. 1066, pp. 232\u2013243. Springer, Heidelberg (1996)"},{"doi-asserted-by":"crossref","unstructured":"B\u00f8gholm, T., Kragh-Hansen, H., Olsen, P., Thomsen, B., Larsen, K.G.: Model-based schedulability analysis of safety critical hard real-time java programs. In: Proceedings of the 6th International Workshop on Java Technologies for Real-Time and Embedded Systems (JTRES\u201908), pp. 106\u2013114 (2008)","key":"4_CR4","DOI":"10.1145\/1434790.1434807"},{"key":"4_CR5","series-title":"Computational Analysis, Synthesis, and Design of Dynamic Systems","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1201\/9781420067859-c4","volume-title":"Model-Based Design for Embedded Systems","author":"A David","year":"2009","unstructured":"David, A., Rasmussen, J.I., Larsen, K.G., Skou, A.: Model-based framework for schedulability analysis using Uppaal 4.1. Model-Based Design for Embedded Systems. Computational Analysis, Synthesis, and Design of Dynamic Systems, pp. 93\u2013119. CRC Press, Boca Raton (2009)"},{"key":"4_CR6","series-title":"LNCS","first-page":"132","volume-title":"FMICS 2010","author":"M Gerke","year":"2010","unstructured":"Gerke, M., Ehlers, R., Finkbeiner, B., Peter, H.-J.: Model checking the FlexRay physical layer protocol. In: Kowalewski, S., Roveri, M. (eds.) FMICS 2010. LNCS, vol. 6371, pp. 132\u2013147. Springer, Heidelberg (2010)"},{"doi-asserted-by":"crossref","unstructured":"Giusto, P., Ferrari, A., Lavagno, L., Brunel, J.Y., Fourgeau, E., Sangiovanni-Vincentelli, A.: Automotive virtual integration platforms: why\u2019s, what\u2019s, and how\u2019s. In: IEEE International Conference on Computer Design: VLSI in Computers and Processors, pp. 370\u2013378 (2002)","key":"4_CR7","DOI":"10.1109\/ICCD.2002.1106796"},{"doi-asserted-by":"crossref","unstructured":"Hagiescu, A., Bordoloi, U.D., Chakraborty, S., Sampath, P., Ganesan, P.V.V., Ramesh, S.: Performance analysis of FlexRay-based ECU networks. In: DAC\u201907, pp. 284\u2013289 (2007)","key":"4_CR8","DOI":"10.1145\/1278480.1278554"},{"key":"4_CR9","series-title":"LNCS","first-page":"77","volume-title":"FORTEST","author":"A Hessel","year":"2008","unstructured":"Hessel, A., Larsen, K.G., Mikucionis, M., Nielsen, B., Pettersson, P., Skou, A.: Testing real-time systems using UPPAAL. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) FORTEST. LNCS, vol. 4949, pp. 77\u2013117. Springer, Heidelberg (2008)"},{"unstructured":"Hiraoka, T., Eto, S., Nishihara, O., Kumamoto, H.: Fault tolerant design for X-by-wire vehicle. In: SICE\u201904 Annual Conference, vol. 3, pp. 1940\u20131945 (2004)","key":"4_CR10"},{"doi-asserted-by":"crossref","unstructured":"Jung, K.H., Song, M.G., Lee, D.I., Jin, S.H.: Priority-based scheduling of dynamic segment in FlexRay network. In: International Conference on Control, Automation and Systems (ICCAS\u201908), pp. 1036\u20131041 (2008)","key":"4_CR11","DOI":"10.1109\/ICCAS.2008.4694307"},{"issue":"3","key":"4_CR12","doi-asserted-by":"crossref","first-page":"461","DOI":"10.2478\/v10178-010-0039-z","volume":"17","author":"J Malinsk\u00fd","year":"2010","unstructured":"Malinsk\u00fd, J., Nov\u00e1k, J.: Verification of FlexRay start-up mechanism by timed automata. Metrol. Measur. Syst. 17(3), 461\u2013480 (2010)","journal-title":"Metrol. Measur. Syst."},{"issue":"6","key":"4_CR13","doi-asserted-by":"publisher","first-page":"1204","DOI":"10.1109\/JPROC.2005.849725","volume":"93","author":"N Navet","year":"2005","unstructured":"Navet, N., Song, Y., Simonot-Lion, F., Wilwert, C.: Trends in automotive communication systems. Proc. IEEE 93(6), 1204\u20131223 (2005)","journal-title":"Proc. IEEE"},{"unstructured":"Qtronic GmbH, Germany: Virtual integration and test of automotive ECUs. In: Automotive Testing Expo North America, ASAM Open Technology Forum (2011)","key":"4_CR14"},{"issue":"3","key":"4_CR15","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1109\/MM.2003.1209462","volume":"23","author":"A Sangiovanni-Vincentelli","year":"2003","unstructured":"Sangiovanni-Vincentelli, A.: Electronic-system design in the automobile industry. IEEE Micro 23(3), 8\u201318 (2003)","journal-title":"IEEE Micro"},{"doi-asserted-by":"crossref","unstructured":"Tanasa, B., Bordoloi, U., Kosuch, S., Eles, P., Peng, Z.: Schedulability analysis for the dynamic segment of FlexRay: a generalization to slot multiplexing. In: IEEE 18th Real-Time and Embedded Technology and Applications Symposium (RTAS\u201912), pp. 185\u2013194 (2012)","key":"4_CR16","DOI":"10.1109\/RTAS.2012.10"},{"doi-asserted-by":"crossref","unstructured":"Zeng, H., Ghosal, A., Di Natale, M.: Timing analysis and optimization of FlexRay dynamic segment. In: IEEE 10th International Conference on Computer and Information Technology (CIT\u201910), pp. 1932\u20131939 (2010)","key":"4_CR17","DOI":"10.1109\/CIT.2010.329"},{"unstructured":"UPPAAL models used in this paper: https:\/\/github.com\/h-lin\/FTSCS2013","key":"4_CR18"}],"container-title":["Communications in Computer and Information Science","Formal Techniques for Safety-Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-05416-2_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T08:46:55Z","timestamp":1746175615000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-05416-2_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319054155","9783319054162"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-05416-2_4","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"6 April 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}