An inheritance-based technique for building simulation proofs incrementally

ABSTRACT

This paper presents a technique for incrementally constructing safety specifications, abstract algorithm descriptions, and simulation proofs showing that algorithms meet their specifications.The technique for building specifications (and algorithms) allows a child specification (or algorithm) to inherit from its parent by two forms of incremental modification: (a) interface extension, where new forms of interaction are added to the parent's interface, and (b) specialization (subtyping), where new data, restrictions, and effects are added to the parent's behavior description. The combination of interface extension and specialization constitutes a powerful and expressive incremental modification mechanism for describing changes that do not override the behavior of the parent, although it may introduce new behavior.Consider the case when incremental modification is applied to both a parent specification S and a parent algorithm A. A proof that the child algorithm A′ implements the child specification S′ can be built incrementally upon simulation proof that algorithm A implements specification S. The new work required involves reasoning about the modifications, but does not require repetition of the reasoning in the original simulation proof.The paper presents the technique mathematically, in terms of automata. The technique has already been used to model and validate a full-fledged group communication system (see [26]); the methodology and results of that experiment are summarized in this paper.

REFERENCES

• 1: Martin Abadi , Luca Cardelli, A Theory of Objects, Springer-Verlag New York, Inc., Secaucus, NJ, 1996
• 2: Martín Abadi , Leslie Lamport, The existence of refinement mappings, Theoretical Computer Science, v.82 n.2, p.253-284, May 31, 1991 [doi>10.1016/0304-3975(91)90224-P]
• 3: ACM. Commun. ACM 39(4), special issue on Group Communications Systems, April 1996.
• 4: E. Anceaume, B. Charron-Bost, P. Minet, and S. Toueg. On the formal speci cation of group membership services. Comp. Sci. TR 95-1534, Cornell Univ., Aug. 1995.
• 5: Fault Tolerant Video on Demand Services, Proceedings of the 19th IEEE International Conference on Distributed Computing Systems, p.244, May 31-June 04, 1999
• 6: M. Bickford and J. Hickey. An object-oriented approach to verifying group communication systems. http://www.cs.cornell.edu/jyh/papers/cav99 ooioa/.
• 7: K. Birman, R. Friedman, M. Hayden, and I. Rhee. Middleware support for distributed multimedia and collaborative computing. Multimedia Computing and Networking (MMCN98), 1998.
• 8: Timothy A. Budd, An introduction to object-oriented programming (2nd ed.), Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, 1997
• 9: G. V. Chockler. An Adaptive Totally Ordered Multicast Protocol that Tolerates Partitions. Master's thesis, Institute of Computer Science, The Hebrew University of Jerusalem, Jerusalem, Israel, 1997.
• 10: William Cook , Jens Palsberg, A denotational semantics of inheritance and its correctness, Information and Computation, v.114 n.2, p.329-350, Nov. 1, 1994 [doi>10.1006/inco.1994.1090]
• 11: Roberto De Prisco , Alan Fekete , Nancy Lynch , Alex Shvartsman, A dynamic view-oriented group communication service, Proceedings of the seventeenth annual ACM symposium on Principles of distributed computing, p.227-236, June 28-July 02, 1998, Puerto Vallarta, Mexico [doi>10.1145/277697.277739]
• 12: Roberto De Prisco , Alan Fekete , Nancy A. Lynch , Alexander A. Shvartsman, A Dynamic Primary Configuration Group Communication Service, Proceedings of the 13th International Symposium on Distributed Computing, p.64-78, September 27-29, 1999
• 13: W. DeRoever , Kai Engelhardt, Data Refinement: Model-Oriented Proof Methods and Their Comparison, Cambridge University Press, New York, NY, 1999
• 14: Alan Fekete , David Gupta , Victor Luchangco , Nancy Lynch , Alex Shvartsman, Eventually-serializable data services, Theoretical Computer Science, v.220 n.1, p.113-156, June 6, 1999 [doi>10.1016/S0304-3975(98)00239-4]
• 15: Alan Fekete , Nancy Lynch , Alex Shvartsman, Specifying and using a partitionable group communication service, Proceedings of the sixteenth annual ACM symposium on Principles of distributed computing, p.53-62, August 21-24, 1997, Santa Barbara, California, United States [doi>10.1145/259380.259422]
• 16: R. Friedman , A. Vaysburd, Fast Replicated State Machines Over Partitionable Networks, Proceedings of the 16th Symposium on Reliable Distributed Systems (SRDS '97), p.130, October 22-24, 1997
• 17: Stephen J. Garland , Nancy Lynch, Using I/O automata for developing distributed systems, Foundations of component-based systems, Cambridge University Press, New York, NY, 2000
• 18: S. J. Garland, N. A. Lynch, and M. Vaziri. IOA: A Language for Specifying, Programming and Validating Distributed Systems. MIT LCS, Dec. 1997. http://sds.lcs.mit.edu/~garland/ioaLanguage.html.
• 19: Mark Hayden , Robbert vanRenesse, Optimizing Layered Communication Protocols, Cornell University, Ithaca, NY, 1996
• 20: Mats P. E. Heimdahl , Constance L. Heitmeyer, Formal Methods For Developing High Assurance Computer Systems: Working Group Report, Proceedings of the Second IEEE Workshop on Industrial Strength Formal Specification Techniques, p.60, October 20-23, 1998
• 21: C. Heitmeyer and N. Lynch. The generalized railroad crossing: A case study in formal verification of realtime systems. Real Time Systems Symposium, Dec. 1994. Full version: MR-7619, Naval Research Laboratory.
• 22: Constance L. Heitmeyer, On the Need for Practical Formal Methods, Proceedings of the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, p.18-26, September 14-18, 1998
• 23: Andreas V. Hense, Wrapper Semantics of an Object-Oriented Programming Language with State, Proceedings of the International Conference on Theoretical Aspects of Computer Software, p.548-568, September 24-27, 1991
• 24: Jason Hickey , Nancy A. Lynch , Robbert van Renesse, Specifications and Proofs for Ensemble Layers, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.119-133, March 22-28, 1999
• 25: S. Kamin, Inheritance in smalltalk-80: a denotational definition, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.80-87, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73567]
• 26: Idit Keidar , Roger I. Khazan, A Client-Server Approach to Virtually Synchronous Group Multicast: Specifications and Algorithms, Proceedings of the The 20th International Conference on Distributed Computing Systems ( ICDCS 2000), p.344, April 10-13, 2000
• 27: Idit Keidar , Jeremy Sussman , Keith Marzullo , Danny Dolev, A Client-Server Oriented Algorithm for Virtually Synchronous Group Membership in WANs, University of California at San Diego, La Jolla, CA, 1999
• 28: Roger I. Khazan , Alan Fekete , Nancy A. Lynch, Multicast Group Communication as a Base for a Load-Balancing Replicated Data Service, Proceedings of the 12th International Symposium on Distributed Computing, p.258-272, September 24-26, 1998
• 29: B. Lampson. Generalizing Abstraction Functions. MIT, Laboratory for Computer Science, Principles of Computer Systems, Handout 8, 1997. ftp://theory.lcs.mit .edu/pub/classes/6.826/www/6.826-top.html.
• 30: Nancy A. Lynch, Distributed Algorithms, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1996
• 31: N. A. Lynch , A. A. Shvartsman, Robust emulation of shared memory using dynamic quorum-acknowledged broadcasts, Proceedings of the 27th International Symposium on Fault-Tolerant Computing (FTCS '97), p.272, June 25-27, 1997
• 32: N. Lynch and M. Tuttle. An introduction to Input/Output Automata. CWI Quart., 2(3):219{246, '89.
• 33: Uday Reddy, Objects as closures: abstract semantics of object-oriented languages, Proceedings of the 1988 ACM conference on LISP and functional programming, p.289-297, July 25-27, 1988, Snowbird, Utah, United States [doi>10.1145/62678.62721]
• 34: I. Shnaiderman. Implementation of Reliable Datagram Service in the LAN environment. Lab project, The Hebrew University of Jerusalem, January 1999. http://www.cs.huji.ac.il/~transis/publications.html.
• 35: A. P. Sistla, Proving correctness with respect to nondeterministic safety specifications, Information Processing Letters, v.39 n.1, p.45-49, July 12, 1991 [doi>10.1016/0020-0190(91)90061-L]
• 36: Raymie Stata , John V. Guttag, Modular reasoning in the presence of subclassing, Proceedings of the tenth annual conference on Object-oriented programming systems, languages, and applications, p.200-214, October 15-19, 1995, Austin, Texas, United States
• 37: R. Vitenberg, I. Keidar, G. V. Chockler, and D. Dolev. Group Communication Specifications: A Comprehensive Study. TR CS99-31, Institute of Comp. Science, The Hebrew University of Jerusalem, Israel, Sept. 1999.
• 38: D. Yates, N. Lynch, V. Luchangco, and M. Seltzer. I/O automaton model of operating system primitives. Master's thesis, Harvard University and MIT, May 1999.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

  I. Computing Methodologies
  I.6 SIMULATION AND MODELING

General Terms:
Algorithms, Design, Performance, Theory, Verification

Keywords:
interface extension, refinement, simulation, specialization by inheritance, system modeling/verification