{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:20:25Z","timestamp":1725456025702},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540566625"},{"type":"electronic","value":"9783540476238"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/bfb0024663","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T05:09:15Z","timestamp":1132722555000},"page":"482-500","source":"Crossref","is-referenced-by-count":7,"title":["Formal verification for fault-tolerant architectures: Some lessons learned"],"prefix":"10.1007","author":[{"given":"Sam","family":"Owre","sequence":"first","affiliation":[]},{"given":"John","family":"Rushby","sequence":"additional","affiliation":[]},{"given":"Natarajan","family":"Shankar","sequence":"additional","affiliation":[]},{"given":"Friedrich","family":"von Henke","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"30_CR1","first-page":"243","volume-title":"Dependable Computing for Critical Applications\u20142, volume 6 of Dependable Computing and Fault-Tolerant Systems","author":"W. R. Bevier","year":"1991","unstructured":"W. R. Bevier and W. D. Young. The design and proof of correctness of a fault-tolerant circuit. In Meyer and Schlichting [13], pages 243\u2013260."},{"key":"30_CR2","unstructured":"R. S. Boyer and J S. Moore. Integrating decision procedures into heuristic theorem provers: A case study with linear arithmetic. In Machine Intelligence, volume 11. Oxford University Press, 1986."},{"key":"30_CR3","unstructured":"J. H. Cheng and C. B. Jones. On the usability of logics which handle partial functions. In Carroll Morgan and J. C. P. Woodcock, editors, Proceedings of the Third Refinement Workshop, pages 51\u201369. Springer-Verlag Workshops in Computing, 1990."},{"key":"30_CR4","doi-asserted-by":"crossref","unstructured":"Ben L. Di Vito and Ricky W. Butler. Formal techniques for synchronized fault-tolerant systems. In 3rd IFIP Working Conference on Dependable Computing for Critical Applications, pages 85\u201397, Mondello, Sicily, Italy, September 1992.","DOI":"10.1007\/978-3-7091-4009-3_7"},{"key":"30_CR5","first-page":"279","volume-title":"Dependable Computing for Critical Applications\u20142, volume 6 of Dependable Computing and Fault-Tolerant Systems","author":"B. L. Vito Di","year":"1991","unstructured":"Ben L. Di Vito, Ricky W. Butler, and James L. Caldwell. High level design proof of a reliable computing platform. In Meyer and Schlichting [13], pages 279\u2013306."},{"key":"30_CR6","unstructured":"System Design and Analysis. Federal Aviation Administration, June 21, 1988. Advisory Circular 25.1309-1A."},{"issue":"1","key":"30_CR7","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1145\/2455.2457","volume":"32","author":"L. Lamport","year":"1985","unstructured":"L. Lamport and P. M. Melliar-Smith. Synchronizing clocks in the presence of faults. Journal of the ACM, 32(1):52\u201378, January 1985.","journal-title":"Journal of the ACM"},{"issue":"3","key":"30_CR8","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1145\/357172.357176","volume":"4","author":"L. Lamport","year":"1982","unstructured":"Leslie Lamport, Robert Shostak, and Marshall Pease. The Byzantine generals problem. ACM Transactions on Programming Languages and Systems, 4(3):382\u2013401, July 1982.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"30_CR9","volume-title":"Technical report","author":"P. Lincoln","year":"1993","unstructured":"Patrick Lincoln and John Rushby. Formal verification of algorithm for interactive consistency under a hybrid fault model. Technical report, Computer Science Laboratory, SRI International, Menlo Park, CA, February 1993."},{"key":"30_CR10","volume-title":"Technical report","author":"E. Liu","year":"1993","unstructured":"Erwin Liu and John Rushby. Formal verification of a clock synchronization support circuit. Technical report, Computer Science Laboratory, SRI International, Menlo Park, CA, 1993. Forthcoming."},{"key":"30_CR11","volume-title":"NASA Technical Paper 2857","author":"D. A. Mackall","year":"1988","unstructured":"Dale A. Mackall. Development and flight test experiences with a flight-crucial digital control system. NASA Technical Paper 2857, NASA Ames Research Center, Dryden Flight Research Facility, Edwards, CA, 1988."},{"key":"30_CR12","first-page":"41","volume-title":"Proc. VerkShop III","author":"P. M. Melliar-Smith","year":"1985","unstructured":"P. Michael Melliar-Smith and John Rushby. The Enhanced HDM system for specification and verification. In Proc. VerkShop III, pages 41\u201343, Watsonville, CA, February 1985. Published as ACM Software Engineering Notes, Vol. 10, No. 4, Aug. 85."},{"volume-title":"Dependable Computing for Critical Applications\u20142, volume 6 of Dependable Computing and Fault-Tolerant Systems","year":"1991","key":"30_CR13","unstructured":"J. F. Meyer and R. D. Schlichting, editors. Dependable Computing for Critical Applications\u20142, volume 6 of Dependable Computing and Fault-Tolerant Systems, Tucson, AZ, February 1991. Springer-Verlag, Wien, Austria."},{"key":"30_CR14","volume-title":"NASA Technical Memorandum 107568","author":"P. S. Miner","year":"1992","unstructured":"Paul S. Miner. A verified design of a fault-tolerant clock synchronization circuit: Preliminary investigations. NASA Technical Memorandum 107568, NASA Langley Research Center, Hampton, VA, March 1992."},{"key":"30_CR15","series-title":"volume 607 of Lecture Notes in Artificial Intelligence","first-page":"748","volume-title":"11th International Conference on Automated Deduction (CADE)","author":"S. Owre","year":"1992","unstructured":"S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In Deepak Kapur, editor, 11th International Conference on Automated Deduction (CADE), volume 607 of Lecture Notes in Artificial Intelligence, pages 748\u2013752, Saratoga, NY, 1992. Springer Verlag."},{"key":"30_CR16","volume-title":"NASA Technical Paper 2857","author":"D. L. Palumbo","year":"1992","unstructured":"Daniel L. Palumbo and R. Lynn Graham. Experimental validation of clock synchronization algorithms. NASA Technical Paper 2857, NASA Langley Research Center, Hampton, VA, July 1992."},{"key":"30_CR17","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1007\/3-540-55092-5_13","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 571 of Lecture Notes in Computer Science","author":"J. Rushby","year":"1992","unstructured":"John Rushby. Formal specification and verification of a fault-masking and transientrecovery model for digital flight-control systems. In Vytopil [26],. pages 237\u2013257."},{"key":"30_CR18","volume-title":"Technical Report SRI-CSL-92-1","author":"J. Rushby","year":"1992","unstructured":"John Rushby. Formal verification of an Oral Messages algorithm for interactive consistency. Technical Report SRI-CSL-92-1, Computer Science Laboratory, SRI International, Menlo Park, CA, July 1992. Also available as NASA Contractor Report 189704, October 1992."},{"key":"30_CR19","first-page":"1","volume-title":"SIGSOFT '91: Software for Critical Systems","author":"J. Rushby","year":"1993","unstructured":"John Rushby and Friedrich von Henke. Formal verification of algorithms for critical systems. In SIGSOFT '91: Software for Critical Systems, pages 1\u201315, New Orleans, LA, December 1991. Expanded version to appear in IEEE Transactions on Software Engineering, 1993."},{"key":"30_CR20","volume-title":"Technical Report SRI-CSL-91-2","author":"J. Rushby","year":"1991","unstructured":"John Rushby, Friedrich von Henke, and Sam Owre. An introduction to formal specification and verification using Ehdm. Technical Report SRI-CSL-91-2, Computer Science Laboratory, SRI International, Menlo Park, CA, February 1991."},{"key":"30_CR21","volume-title":"Technical Report 87-859","author":"F. B. Schneider","year":"1987","unstructured":"Fred B. Schneider. Understanding protocols for Byzantine clock synchronization. Technical Report 87-859, Department of Computer Science, Cornell University, Ithaca, NY, August 1987."},{"key":"30_CR22","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1007\/3-540-55092-5_12","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 571 of Lecture Notes in Computer Science","author":"N. Shankar","year":"1992","unstructured":"Natarajan Shankar. Mechanical verification of a generalized protocol for Byzantine fault-tolerant clock synchronization. In Vytopil [26],. pages 217\u2013236."},{"issue":"1","key":"30_CR23","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R. E. Shostak","year":"1984","unstructured":"Robert E. Shostak. Deciding combinations of theories. Journal of the ACM, 31(1):1\u201312, January 1984.","journal-title":"Journal of the ACM"},{"key":"30_CR24","volume-title":"Contractor Report 4381","author":"M. Srivas","year":"1991","unstructured":"Mandayam Srivas and Mark Bickford. Verification of the FtCayuga fault-tolerant microprocessor system, volume 1: A case-study in theorem prover-based verification. Contractor Report 4381, NASA Langley Research Center, Hampton, VA, July 1991."},{"key":"30_CR25","first-page":"93","volume-title":"Interactive consistency with multiple failure modes","author":"P. Thambidurai","year":"1988","unstructured":"Philip Thambidurai and You-Keun Park. Interactive consistency with multiple failure modes. In 7th Symposium on Reliable Distributed Systems, pages 93\u2013100, Columbus, OH, October 1988. IEEE Computer Society."},{"volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 571 of Lecture Notes in Computer Science","year":"1992","key":"30_CR26","unstructured":"J. Vytopil, editor. Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 571 of Lecture Notes in Computer Science, Nijmegen, The Netherlands, January 1992. Springer Verlag."},{"issue":"1","key":"30_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(88)90043-0","volume":"77","author":"J. L. Welch","year":"1988","unstructured":"J. Lundelius Welch and N. Lynch. A new fault-tolerant algorithm for clock synchronization. Information and Computation, 77(1):1\u201336, April 1988.","journal-title":"Information and Computation"},{"issue":"10","key":"30_CR28","doi-asserted-by":"crossref","first-page":"1240","DOI":"10.1109\/PROC.1978.11114","volume":"66","author":"J. H. Wensley","year":"1978","unstructured":"John H. Wensley et al. SIFT: Design and analysis of a fault-tolerant computer for aircraft control. Proceedings of the IEEE, 66(10):1240\u20131255, October 1978.","journal-title":"Proceedings of the IEEE"},{"key":"30_CR29","volume-title":"NASA Contractor Report 189649","author":"W. D. Young","year":"1992","unstructured":"William D. Young. Verifying the Interactive Convergence clock-synchronization algorithm using the Boyer-Moore prover. NASA Contractor Report 189649, NASA Langley Research Center, Hampton, VA, April 1992."}],"container-title":["Lecture Notes in Computer Science","FME '93: Industrial-Strength Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0024663","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T00:53:03Z","timestamp":1586566383000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0024663"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540566625","9783540476238"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/bfb0024663","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}