{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T16:45:15Z","timestamp":1725727515348},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642391750"},{"type":"electronic","value":"9783642391767"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39176-7_14","type":"book-chapter","created":{"date-parts":[[2013,5,30]],"date-time":"2013-05-30T08:58:44Z","timestamp":1369904324000},"page":"209-226","source":"Crossref","is-referenced-by-count":28,"title":["Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms"],"prefix":"10.1007","author":[{"given":"Annu","family":"John","sequence":"first","affiliation":[]},{"given":"Igor","family":"Konnov","sequence":"additional","affiliation":[]},{"given":"Ulrich","family":"Schmid","sequence":"additional","affiliation":[]},{"given":"Helmut","family":"Veith","sequence":"additional","affiliation":[]},{"given":"Josef","family":"Widder","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","unstructured":"Ademaj, A.: Slightly-off-specification failures in the time-triggered architecture. In: High-Level Design Validation and Test Workshop, pp. 7\u201312. IEEE (2002)"},{"key":"14_CR2","unstructured":"Aguilera, M.K., Delporte-Gallet, C., Fauconnier, H., Toueg, S.: Consensus with Byzantine failures and little system synchrony. In: DSN, pp. 147\u2013155 (2006)"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Attiya, H., Welch, J.: Distributed Computing, 2nd edn. John Wiley & Sons (2004)","DOI":"10.1002\/0471478210"},{"issue":"40","key":"14_CR4","doi-asserted-by":"publisher","first-page":"5602","DOI":"10.1016\/j.tcs.2010.09.032","volume":"412","author":"M. Biely","year":"2011","unstructured":"Biely, M., Schmid, U., Weiss, B.: Synchronous consensus under hybrid process and link failures. Theoretical Computer Science\u00a0412(40), 5602\u20135630 (2011)","journal-title":"Theoretical Computer Science"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"Bokor, P., Kinder, J., Serafini, M., Suri, N.: Efficient model checking of fault-tolerant distributed protocols. In: DSN, pp. 73\u201384 (2011)","DOI":"10.1109\/DSN.2011.5958208"},{"issue":"4","key":"14_CR6","doi-asserted-by":"publisher","first-page":"824","DOI":"10.1145\/4221.214134","volume":"32","author":"G. Bracha","year":"1985","unstructured":"Bracha, G., Toueg, S.: Asynchronous consensus and broadcast protocols. J. ACM\u00a032(4), 824\u2013840 (1985)","journal-title":"J. ACM"},{"key":"14_CR7","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1016\/0890-5401(89)90026-6","volume":"81","author":"M.C. Browne","year":"1989","unstructured":"Browne, M.C., Clarke, E.M., Grumberg, O.: Reasoning about networks with many identical finite state processes. Inf. Comput.\u00a081, 13\u201331 (1989)","journal-title":"Inf. Comput."},{"key":"14_CR8","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/j.entcs.2006.11.004","volume":"168","author":"A. Bucchiarone","year":"2007","unstructured":"Bucchiarone, A., Muccini, H., Pelliccione, P.: Architecting fault-tolerant component-based systems: from requirements to testing. Electr. Notes Theor. Comput. Sci.\u00a0168, 77\u201390 (2007)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"2","key":"14_CR9","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1145\/226643.226647","volume":"43","author":"T.D. Chandra","year":"1996","unstructured":"Chandra, T.D., Toueg, S.: Unreliable failure detectors for reliable distributed systems. J. ACM\u00a043(2), 225\u2013267 (1996)","journal-title":"J. ACM"},{"issue":"1","key":"14_CR10","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/s00446-009-0084-6","volume":"22","author":"B. Charron-Bost","year":"2009","unstructured":"Charron-Bost, B., Schiper, A.: The heard-of model: computing in distributed systems with benign faults. Distributed Computing\u00a022(1), 49\u201371 (2009)","journal-title":"Distributed Computing"},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-78800-3_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2008","unstructured":"Clarke, E., Talupur, M., Veith, H.: Proving Ptolemy right: the environment abstraction framework for model checking concurrent systems. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 33\u201347. Springer, Heidelberg (2008)"},{"key":"14_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/978-3-540-28644-8_18","volume-title":"CONCUR 2004 - Concurrency Theory","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Talupur, M., Touili, T., Veith, H.: Verification by network decomposition. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 276\u2013291. Springer, Heidelberg (2004)"},{"issue":"2","key":"14_CR13","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1145\/42282.42283","volume":"35","author":"C. Dwork","year":"1988","unstructured":"Dwork, C., Lynch, N., Stockmeyer, L.: Consensus in the presence of partial synchrony. J. ACM\u00a035(2), 288\u2013323 (1988)","journal-title":"J. ACM"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Emerson, E., Namjoshi, K.: Reasoning about rings. In: POPL, pp. 85\u201394 (1995)","DOI":"10.1145\/199448.199468"},{"key":"14_CR15","unstructured":"Feather, M.S., Fickas, S., Razermera-Mamy, N.A.: Model-checking for validation of a fault protection system. In: HASE, pp. 32\u201341 (2001)"},{"issue":"2","key":"14_CR16","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1145\/3149.214121","volume":"32","author":"M.J. Fischer","year":"1985","unstructured":"Fischer, M.J., Lynch, N.A., Paterson, M.S.: Impossibility of distributed consensus with one faulty process. J. ACM\u00a032(2), 374\u2013382 (1985)","journal-title":"J. ACM"},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-540-78800-3_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Fisman","year":"2008","unstructured":"Fisman, D., Kupferman, O., Lustig, Y.: On verifying fault tolerance of distributed protocols. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 315\u2013331. Springer, Heidelberg (2008)"},{"issue":"6","key":"14_CR18","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/s00446-011-0151-7","volume":"24","author":"M. F\u00fcgger","year":"2012","unstructured":"F\u00fcgger, M., Schmid, U.: Reconciling fault-tolerant distributed computing and systems-on-chip. Distributed Computing\u00a024(6), 323\u2013355 (2012)","journal-title":"Distributed Computing"},{"key":"14_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"535","DOI":"10.1007\/3-540-46419-0_36","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Gnesi","year":"2000","unstructured":"Gnesi, S., Latella, D., Lenzini, G., Abbaneo, C., Amendola, A., Marmo, P.: A formal specification and validation of a critical system in presence of Byzantine errors. In: Graf, S. (ed.) TACAS 2000. LNCS, vol.\u00a01785, pp. 535\u2013549. Springer, Heidelberg (2000)"},{"key":"14_CR20","unstructured":"Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional (2003)"},{"key":"14_CR21","unstructured":"John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Brief announcement: Parameterized model checking of fault-tolerant distributed algorithms by abstraction. In: ACM PODC (to appear, 2013) (long version at arXiv CoRR abs\/1210.3846)"},{"issue":"8","key":"14_CR22","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/361082.361093","volume":"17","author":"L. Lamport","year":"1974","unstructured":"Lamport, L.: A new solution of Dijkstra\u2019s concurrent programming problem. Commun. ACM\u00a017(8), 453\u2013455 (1974)","journal-title":"Commun. ACM"},{"issue":"2","key":"14_CR23","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BF01786227","volume":"1","author":"L. Lamport","year":"1986","unstructured":"Lamport, L.: On interprocess communication. Part I: Basic formalism. Distributed Computing\u00a01(2), 77\u201385 (1986)","journal-title":"Distributed Computing"},{"volume-title":"Distributed Algorithms","year":"1996","author":"N. Lynch","key":"14_CR24","unstructured":"Lynch, N.: Distributed Algorithms. Morgan Kaufman, San Francisco (1996)"},{"key":"14_CR25","unstructured":"Malekpour, M.R., Siminiceanu, R.: Comments on the \u201cByzantine self-stabilizing pulse synchronization\u201d. protocol: Counterexamples. Tech. rep., NASA (February 2006)"},{"issue":"3","key":"14_CR26","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1109\/TDSC.2006.35","volume":"3","author":"J.P. Martin","year":"2006","unstructured":"Martin, J.P., Alvisi, L.: Fast Byzantine consensus. IEEE Trans. Dep. Sec. Comp.\u00a03(3), 202\u2013215 (2006)","journal-title":"IEEE Trans. Dep. Sec. Comp."},{"key":"14_CR27","unstructured":"Most\u00e9faoui, A., Mourgaya, E., Parv\u00e9dy, P.R., Raynal, M.: Evaluating the condition-based approach to solve consensus. In: DSN, pp. 541\u2013550 (2003)"},{"issue":"2","key":"14_CR28","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1145\/322186.322188","volume":"27","author":"M. Pease","year":"1980","unstructured":"Pease, M., Shostak, R., Lamport, L.: Reaching agreement in the presence of faults. J. ACM\u00a027(2), 228\u2013234 (1980)","journal-title":"J. ACM"},{"key":"14_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/3-540-45657-0_9","volume-title":"Computer Aided Verification","author":"A. Pnueli","year":"2002","unstructured":"Pnueli, A., Xu, J., Zuck, L.: Liveness with (0,1,\u221e)- counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 107\u2013122. Springer, Heidelberg (2002)"},{"key":"14_CR30","unstructured":"Powell, D.: Failure mode assumptions and assumption coverage. In: FTCS-22, Boston, MA, USA, pp. 386\u2013395 (1992)"},{"key":"14_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/BFb0028994","volume-title":"STACS 89","author":"N. Santoro","year":"1989","unstructured":"Santoro, N., Widmayer, P.: Time is not a healer. In: Cori, R., Monien, B. (eds.) STACS 1989. LNCS, vol.\u00a0349, pp. 304\u2013313. Springer, Heidelberg (1989)"},{"key":"14_CR32","unstructured":"Schneider, F., Easterbrook, S.M., Callahan, J.R., Holzmann, G.J.: Validating requirements for fault tolerant systems using model checking. In: ICRE, pp. 4\u201313 (1998)"},{"issue":"4","key":"14_CR33","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1145\/98163.98167","volume":"22","author":"F.B. Schneider","year":"1990","unstructured":"Schneider, F.B.: Implementing fault-tolerant services using the state machine approach: A tutorial. ACM Comput. Surv.\u00a022(4), 299\u2013319 (1990)","journal-title":"ACM Comput. Surv."},{"key":"14_CR34","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/BF01667080","volume":"2","author":"T. Srikanth","year":"1987","unstructured":"Srikanth, T., Toueg, S.: Simulating authenticated broadcasts to derive simple fault-tolerant algorithms. Distributed Computing\u00a02, 80\u201394 (1987)","journal-title":"Distributed Computing"},{"key":"14_CR35","doi-asserted-by":"crossref","unstructured":"Steiner, W., Rushby, J.M., Sorea, M., Pfeifer, H.: Model checking a fault-tolerant startup algorithm: From design exploration to exhaustive fault simulation. In: DSN, pp. 189\u2013198 (2004)","DOI":"10.1109\/DSN.2004.1311889"},{"issue":"5-6","key":"14_CR36","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/s00446-010-0123-3","volume":"23","author":"T. Tsuchiya","year":"2011","unstructured":"Tsuchiya, T., Schiper, A.: Verification of consensus algorithms using satisfiability solving. Distributed Computing\u00a023(5-6), 341\u2013358 (2011)","journal-title":"Distributed Computing"},{"issue":"2","key":"14_CR37","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/s00446-007-0026-0","volume":"20","author":"J. Widder","year":"2007","unstructured":"Widder, J., Schmid, U.: Booting clock synchronization in partially synchronous systems with hybrid process and link failures. Distributed Computing\u00a020(2), 115\u2013140 (2007)","journal-title":"Distributed Computing"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39176-7_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T12:57:55Z","timestamp":1557752275000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39176-7_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642391750","9783642391767"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39176-7_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}