Abstract
Four kinds of abstraction for the design and analysis of fault–tolerant distributed systems are discussed. These abstractions concern system messages, faults, fault–masking voting, and communication. The abstractions are formalized in higher–order logic, and are intended to facilitate specifying and verifying such systems in higher–order theorem–provers.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Azadmanesh, M.H., Kieckhafer, R.M.: Exploiting omissive faults in synchronous approximate agreement. IEEE Transactions on Computers 49(10), 1031–1042 (2000)
Castro, M., Liskov, B.: Practical Byzantine fault tolerance. In: ACM Proceedings: Operating Systems Design and Implementation (OSDI), February 1999, pp. 173–186 (1999)
Cristian, F.: Understanding fault-tolerant distributed systems. Communications of the ACM 34(2) (February 1991)
Driscoll, K., Hall, B., Sivencrona, H., Zumsteg, P.: Byzantine fault tolerance, from theory to reality. In: Anderson, S., Felici, M., Littlewood, B. (eds.) SAFECOMP 2003. LNCS, vol. 2788, pp. 235–248. Springer, Heidelberg (2003)
Geser, A., Miner, P.: A formal correctness proof of the SPIDER diagnosis protocol. Technical Report 2002-211736, NASA Langley Research Center, Hampton, Virginia (August 2002), Technical Report contains the Track B proceedings from Theorem Proving in Higher Order Logics (TPHOLSs)
NASA LaRC Formal Methods Group. NASA Langley PVS libraries, Available at http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/pvslib.html
Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1991)
SRI International. PVS homepage, Available at http://pvs.csl.sri.com/
SRI International. PVS language reference, version 2.4, Available at http://pvs.csl.sri.com/manuals.html (December 2001)
Johnson, S.D.: Formal methods in embedded design. Computer, 104–106 (Novemeber 2003)
Koopman, P.: Critical Embedded Automotive Networks, vol. 22-4. IEEE Computer Society, Los Alamitos (July/August 2002)
Kopetz, H.: Real-Time Systems. Kluwer Academic Publishers, Dordrecht (1997)
Lamport, Shostak, Pease: The Byzantine generals problem. ACM Transactions on Programming Languages and Systems 4, 382–401 (1982)
Lamport, L.: Composition: A way to make proofs harder. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 402–423. Springer, Heidelberg (1998)
Laprie, J.-C.: Dependability – its attributes, impairments and means. In: Randell, B., Laprie, J.-C., Kopetz, H., Littlewood, B. (eds.) Predictability Dependable Computing Systems. ESPRIT Basic Research Series, pp. 3–24. Springer, Heidelberg (1995)
Lincoln, P., Rushby, J.: The formal verification of an algorithm for interactive consistency under a hybrid fault model. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 292–304. Springer, Heidelberg (1993)
Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann, San Francisco (1996)
Melham, T.F.: Abstraction mechanisms for hardware verification. In: Birtwistle, G., Subrahmanyam, P.A. (eds.) VLSI Specification, Verification, and Synthesis, Boston, pp. 129–157. Kluwer Academic Publishers, Dordrecht (1988)
Melham, T.F.: Higher Order Logic and Hardware Verification. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (1993)
Miner, P., Geser, A., Pike, L., Maddalon, J.: A unified fault-tolerance protocol (in preparation), Available at http://shemesh.larc.nasa.gov/fm/spider/spider_pubs.html (April 2004)
Miner, P.S., Malekpour, M., Torres-Pomales, W.: Conceptual design of a Reliable Optical BUS (ROBUS). In: 21st AIAA/IEEE Digital Avionics Systems Conference DASC, Irvine, CA (October 2002)
Owre, S., Rushby, J., Shankar, N., von Henke, F.: Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering 21(2), 107–125 (1995)
Pfeifer, H.: Formal Analysis of Fault-Tolerant Algorithms in the Time-Triggered Architecture. PhD thesis, Universität Ulm (2003), Available at http://www.informatik.uni-ulm.de/ki/Papers/pfeifer-phd.html
Pike, L., Maddalon, J., Miner, P., Geser, A.: PVS specifications and proofs for fault-tolerant distributed system verification, Available at http://shemesh.larc.nasa.gov/fm/spider/tphols2004/pvs.html (2004)
Rosenlicht, M.: Introduction to Analysis. Dover Publications, Inc. (1968)
Rushby, J.: Formal methods and digital systems validation for airborne systems. Technical Report CR–4551, NASA (December 1993)
Rushby, J.: Systematic formal verification for fault-tolerant time-triggered algorithms. IEEE Transactions on Software Engineering 25(5), 651–660 (1999)
Rushby, J.: A comparison of bus architectures for safety-critical embedded systems. Technical report, Computer Science Laboratory, SRI International, Menlo Park, CA (September 2001), Available at http://www.csl.sri.com/~rushby/abstracts/buscompare
SPIDER homepage, NASA Langley Research Center, Formal Methods Team, Available at http://shemesh.larc.nasa.gov/fm/spider/
Thambidurai, P., Park, Y.-K.: Interactive consistency with multiple failure modes. In: 7th Reliable Distributed Systems Symposium, October 1988, pp. 93–100 (1988)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pike, L., Maddalon, J., Miner, P., Geser, A. (2004). Abstractions for Fault-Tolerant Distributed System Verification. In: Slind, K., Bunker, A., Gopalakrishnan, G. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2004. Lecture Notes in Computer Science, vol 3223. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30142-4_19
Download citation
DOI: https://doi.org/10.1007/978-3-540-30142-4_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23017-5
Online ISBN: 978-3-540-30142-4
eBook Packages: Springer Book Archive