{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,1]],"date-time":"2025-02-01T05:24:03Z","timestamp":1738387443692,"version":"3.35.0"},"publisher-location":"Boston, MA","reference-count":19,"publisher":"Springer US","isbn-type":[{"type":"print","value":"9780387096605"},{"type":"electronic","value":"9780387096612"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-0-387-09661-2_6","type":"book-chapter","created":{"date-parts":[[2008,8,19]],"date-time":"2008-08-19T13:40:02Z","timestamp":1219153202000},"page":"57-67","source":"Crossref","is-referenced-by-count":4,"title":["Formal Correctness of an Automotive Bus Controller Implementation at Gate-Level"],"prefix":"10.1007","author":[{"given":"Eyad","family":"Alkassar","sequence":"first","affiliation":[]},{"given":"Peter","family":"B\u00f6hm","sequence":"additional","affiliation":[]},{"given":"Steffen","family":"Knapp","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"Berry, G., Kishinevsky, M., Singh, S.: System level design and verification using a synchronous language. In: ICCAD, pp. 433\u2013440 (2003)","DOI":"10.1109\/ICCAD.2003.159720"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Bevier, W., Young, W.: The proof of correctness of a fault-tolerant circuit design. In: Second IFIP Conference on Dependable Computing For Critical Applications, pp. 107\u2013114 (1991)","DOI":"10.1007\/978-3-7091-9198-9_12"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Beyer, S., B\u00f6hm, P., Gerke, M., Hillebrand, M., In der Rieden, T., Knapp, S., Leinenbach, D., Paul, W.J.: Towards the formal verification of lower system layers in automotive systems. In: ICCD \u201905, pp. 317\u2013324. IEEE Computer Society (2005)","DOI":"10.1109\/ICCD.2005.110"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Brown, G.M., Pike, L.: Easy parameterized verification of biphase mark and 8N1 protocols. In: TACAS\u201906, LNCS, vol. 3920, pp. 58\u201372. Springer (2006)","DOI":"10.1007\/11691372_4"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Marco Pistore, M.R., Sebastiani, R., Tacchella, A.: NuSMV 2: An open source tool for symbolic model checking. In: CAV \u201902, pp. 359\u2013364. Springer-Verlag (2002)","DOI":"10.1007\/3-540-45657-0_29"},{"issue":"2","key":"6_CR6","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1016\/S0167-6423(99)00010-6","volume":"35","author":"C. Ferdinand","year":"1999","unstructured":"Ferdinand, C., Martin, F., Wilhelm, R., Alt, M.: Cache Behavior Prediction by Abstract Interpretation. Sci. Comput. Program. 35(2), 163\u2013189 (1999)","journal-title":"Sci. Comput. Program."},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Hillebrand, M., In der Rieden, T., Paul, W.: Dealing with I\/O devices in the context of pervasive system verification. In: ICCD \u201905, pp. 309\u2013316. IEEE Computer Society (2005)","DOI":"10.1109\/ICCD.2005.42"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Knapp, S., Paul,W.: RealisticWorst Case Execution Time Analysis in the Context of Pervasive System Verification. In: Program Analysis and Compilation, LNCS, vol. 4444, pp. 53\u201381 (2007)","DOI":"10.1007\/978-3-540-71322-7_3"},{"issue":"1","key":"6_CR9","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1145\/2455.2457","volume":"32","author":"L. Lamport","year":"1985","unstructured":"Lamport, L., Melliar-Smith, P.M.: Synchronizing clocks in the presence of faults. J. ACM 32(1), 52\u201378 (1985)","journal-title":"J. ACM"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Miner, P.S., Johnson, S.D.: Verification of an optimized fault-tolerant clock synchronization circuit. In: Designing Correct Circuits. Springer (1996)","DOI":"10.14236\/ewic\/DCC1996.9"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Pfeifer, H., Schwier, D., von Henke, F.W.: Formal verification for time-triggered clock synchronization. In: DCCA-7, vol. 12, pp. 207\u2013226. IEEE Computer Society, San Jose, CA (1999)","DOI":"10.1109\/DCFTS.1999.814297"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"Pike, L.: Modeling Time-Triggered Protocols and Verifying Their Real-Time Schedules. In: FMCAD\u201907, pp. 231\u2013238 (2007)","DOI":"10.1109\/FAMCAD.2007.10"},{"issue":"5","key":"6_CR14","doi-asserted-by":"publisher","first-page":"651","DOI":"10.1109\/32.815324","volume":"25","author":"J. Rushby","year":"1999","unstructured":"Rushby, J.: Systematic formal verification for fault-tolerant time-triggered algorithms. IEEE Transactions on Software Engineering 25(5), 651\u2013660 (1999)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"Rushby, J.: An overview of formal verification for the time-triggered architecture. In: FTRTFT\u201902, LNCS, vol. 2469, pp. 83\u2013105. Springer-Verlag, Oldenburg, Germany (2002)","DOI":"10.1007\/3-540-45739-9_7"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Schmaltz, J.: A Formal Model of Clock Domain Crossing and Automated Verification of Time-Triggered Hardware. In: FMCAD\u201907, pp. 223\u2013230. IEEE\/ACM, Austin, TX, USA (2007)","DOI":"10.1109\/FAMCAD.2007.22"},{"key":"6_CR17","first-page":"217","volume-title":"Mechanical verification of a generalized protocol for byzantine fault tolerant clock synchronization. In: FTRTFT\u201992, vol. 571","author":"N. Shankar","year":"1992","unstructured":"Shankar, N.: Mechanical verification of a generalized protocol for byzantine fault tolerant clock synchronization. In: FTRTFT\u201992, vol. 571, pp. 217\u2013236. Springer, Netherlands (1992)"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Tverdyshev, S., Alkassar, E.: Efficient bit-level model reductions for automated hardware verification. In: TIME 2008, to appear. IEEE Computer Society Press (2008)","DOI":"10.1109\/TIME.2008.11"},{"key":"6_CR19","unstructured":"Zhang, B.: On the Formal Verification of the FlexRay Communication Protocol. Automatic Verification of Critical Systems (AVoCS\u201906) pp. 184\u2013189 (2006)"}],"container-title":["IFIP \u2013 The International Federation for Information Processing","Distributed Embedded Systems: Design, Middleware and Resources"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-0-387-09661-2_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,31]],"date-time":"2025-01-31T15:38:42Z","timestamp":1738337922000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-0-387-09661-2_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9780387096605","9780387096612"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-0-387-09661-2_6","relation":{},"ISSN":["1571-5736"],"issn-type":[{"type":"print","value":"1571-5736"}],"subject":[]}}