{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,16]],"date-time":"2026-02-16T19:31:51Z","timestamp":1771270311635,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642203978","type":"print"},{"value":"9783642203985","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-20398-5_27","type":"book-chapter","created":{"date-parts":[[2011,4,6]],"date-time":"2011-04-06T15:29:49Z","timestamp":1302103789000},"page":"375-390","source":"Crossref","is-referenced-by-count":20,"title":["Automated Formal Verification of the TTEthernet Synchronization Quality"],"prefix":"10.1007","author":[{"given":"Wilfried","family":"Steiner","sequence":"first","affiliation":[]},{"given":"Bruno","family":"Dutertre","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"27_CR1","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1109\/JPROC.2002.805821","volume":"91","author":"H. Kopetz","year":"2003","unstructured":"Kopetz, H., Bauer, G.: The Time-Triggered Architecture. Proceedings of the IEEE\u00a091(1), 112\u2013126 (2003)","journal-title":"Proceedings of the IEEE"},{"key":"27_CR2","unstructured":"Howard, C.E.: Orion avionics employ COTS technologies. In: Avionics Intelligence (June 2009)"},{"issue":"2-3","key":"27_CR3","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1016\/S0019-9958(84)80033-9","volume":"62","author":"J. Lundelius","year":"1984","unstructured":"Lundelius, J., Lynch, N.: An upper and lower bound for clock synchronization. Information and Control\u00a062(2-3), 190\u2013204 (1984)","journal-title":"Information and Control"},{"key":"27_CR4","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/800222.806737","volume-title":"PODC 1984: Proceedings of the Third Annual ACM Symposium on Principles of Distributed Computing","author":"L. Lamport","year":"1984","unstructured":"Lamport, L., Melliar-Smith, P.M.: Byzantine clock synchronization. In: PODC 1984: Proceedings of the Third Annual ACM Symposium on Principles of Distributed Computing, pp. 68\u201374. ACM, New York (1984)"},{"key":"27_CR5","unstructured":"Kopetz, H.: TTP\/C Protocol \u2013 Version 1.0. Vienna, Austria: TTTech Computertechnik AG (July 2002), \n                    \n                      http:\/\/www.ttagroup.org"},{"key":"27_CR6","unstructured":"Schneider, F.B.: Understanding protocols for byzantine clock synchronization. Cornell University, Ithaca, NY, USA, Tech. Rep. TR87\u2013859 (1987)"},{"key":"27_CR7","unstructured":"Rushby, J., von Henke, F.: Formal verification of the interactive convergence clock synchronization algorithm. Computer Science Laboratory, SRI International, Menlo Park, CA, Tech. Rep. SRI-CSL-89-3R, (February 1989), \n                    \n                      http:\/\/www.csl.sri.com\/papers\/csl-89-3\/\n                    \n                    \n                   (revised online August 1991)"},{"key":"27_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/3-540-55092-5_12","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"N. Shankar","year":"1992","unstructured":"Shankar, N.: Mechanical verification of a generalized protocol for byzantine fault-tolerant clock synchronization. In: Vytopil, J. (ed.) FTRTFT 1992. LNCS, vol.\u00a0571, pp. 217\u2013236. Springer, Heidelberg (1992)"},{"key":"27_CR9","unstructured":"Miner, P.S.: Verification of fault-tolerant clock synchronization systems. NASA, NASA Technical Paper 2249 (1993), \n                    \n                      http:\/\/ntrs.nasa.gov"},{"key":"27_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/BFb0055353","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"D. Schwier","year":"1998","unstructured":"Schwier, D., von Henke, F.: Mechanical verification of clock synchronization algorithms. In: Ravn, A.P., Rischel, H. (eds.) FTRTFT 1998. LNCS, vol.\u00a01486, pp. 262\u2013271. Springer, Heidelberg (1998)"},{"key":"27_CR11","unstructured":"Pfeifer, H., Schwier, D., von Henke, F.: Formal verification for time-triggered clock synchronization. In: Weinstock, C.B., Rushby, J. (eds.) Dependable Computing for Critical Applications, vol.\u00a07, pp. 206\u2013226 (January 1999)"},{"key":"27_CR12","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/s00165-007-0027-6","volume":"19","author":"D. Barsotti","year":"2007","unstructured":"Barsotti, D., Nieto, L., Tiu, A.: Verification of clock synchronization algorithms: experiments on a combination of deductive tools. Formal Aspects of Computing\u00a019, 321\u2013341 (2007)","journal-title":"Formal Aspects of Computing"},{"key":"27_CR13","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1109\/FAMCAD.2007.10","volume-title":"Proceedings of Formal Methods in Computer Aided Design (FMCAD 2007)","author":"L. Pike","year":"2007","unstructured":"Pike, L.: Modeling time-triggered protocols and verifying their real-time schedules. In: Proceedings of Formal Methods in Computer Aided Design (FMCAD 2007), pp. 231\u2013238. IEEE, Los Alamitos (2007)"},{"key":"27_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-642-15898-8_10","volume-title":"Formal Methods for Industrial Critical Systems","author":"W. Steiner","year":"2010","unstructured":"Steiner, W., Dutertre, B.: SMT-Based formal verification of a TTEthernet synchronization function. In: Kowalewski, S., Roveri, M. (eds.) FMICS 2010. LNCS, vol.\u00a06371, pp. 148\u2013163. Springer, Heidelberg (2010)"},{"key":"27_CR15","doi-asserted-by":"crossref","unstructured":"Malekpour, M.R.: Model checking a byzantine-fault-tolerant self-stabilizing protocol for distributed clock synchronization systems. NASA, Tech. Rep. NASA\/TM-2007-215083 (2007)","DOI":"10.1109\/AERO.2008.4526337"},{"key":"27_CR16","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"L. Moura de","year":"2004","unstructured":"de Moura, L., Owre, S., Rue\u00df, H., Rushby, J., Shankar, N., Sorea, M., Tiwari, A.: Tool presentation: SAL2. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114. Springer, Heidelberg (2004)"},{"key":"27_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/978-3-540-45069-6_2","volume-title":"Computer Aided Verification","author":"L. Moura de","year":"2003","unstructured":"de Moura, L., Rue\u00df, H., Sorea, M.: Bounded model checking and induction: From refutation to verification. In: Voronkov, A. (ed.) CAV 2003. LNCS, vol.\u00a02725, pp. 14\u201326. Springer, Heidelberg (2003)"},{"key":"27_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-540-30206-3_15","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"B. Dutertre","year":"2004","unstructured":"Dutertre, B., Sorea, M.: Modeling and verification of a fault-tolerant real-time startup protocol using calendar automata. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol.\u00a03253, pp. 199\u2013214. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-20398-5_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T14:36:36Z","timestamp":1558535796000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-20398-5_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642203978","9783642203985"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-20398-5_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}