\documentclass{article}
\def\thebibliography#1{\list
  {[\arabic{enumi}]}{\settowidth\labelwidth{[#1]}\leftmargin\labelwidth
    \advance\leftmargin\labelsep
    \usecounter{enumi}}}
\def\newblock{\hskip .11em plus .33em minus .07em}
%%[[to do-- finish adding pointers to online versions. especially tds
%%group ones]]
\makeatletter
 \def\@biblabel#1{\hfill}  % Produces the label for a \bibitem[...]
\makeatother
\input{macros-course}

\begin{document}
\handout{casestudies}{Application Areas and Preliminary
Sources}{February 6, 2001}

In all the application areas described below, the papers listed should
be regarded only as hints.  Students are free (and encouraged) to find
other algorithms in these general areas that are of special interest
to them, and that seem amenable to formal study.

\section{Data management in distributed networks}

This application area involves maintaining data coherently in
distributed networks.
For availability and performance, the data is generally replicated,
which means that protocols are needed to manage consistency among the
replicas.
Interesting properties to study will include
basic coherence properties for the data, fault-tolerance properties,
and performance bounds.

\noindent
A simple ``strong caching'' algorithm was introduced in 6.042, and
shown to implement an ``atomic object''.
%* 6.042 notes, lecture 10

\begin{thebibliography}{100}
\bibitem[Lyn00b]{6042-fall00-lec10}
Nancy Lynch.
\newblock 6.042 lecture notes, Fall 2000.
\newblock Lecture 10. \verb+casestudies/6042-L10.ps.+

\end{thebibliography}
\noindent
The following note presents three basic
replicated data algorithms:  the strong caching algorithm, a majority
voting algorithm, and a version of Lamport's Replicated State Machine
algorithm:
%* Note by Bogdanov, Dean, et al.

\begin{thebibliography}{100}
\bibitem[BDK01]{BogdanovDK}
Andrej Bogdanov, Laura Dean, and Christine Karlovich.
\newblock Distributed memory algorithms coded in ioa: Challenge problems for
  software analysis and synthesis, January 2001.
\newblock Manuscript.\\
 \verb+casestudies/Bogdanov.ps+.

\end{thebibliography}
\noindent
Attiya, et al. present a very asynchronous majority voting algorithm.
This can be extended to allow multiple writers, and to handle general
read/write quorums:
%* Attiya, Bar-Noy, Dolev paper 

\begin{thebibliography}{100}
\bibitem[ABND95]{AttiyaBD95-jacm}
Hagit Attiya, Amotz Bar-Noy, and Danny Dolev.
\newblock Sharing memory robustly in message-passing systems.
\newblock {\em Journal of the ACM}, 42(1):124--142, January 1995.
\newblock \verb+casestudies/p124-attiya.pdf+.

\end{thebibliography}

\noindent
More difficult algorithms involve maintaining coherent data in the
presence of system reconfiguration:  
%* Corel paper (Idit's conference version, PODC)
%* Fekete, Lynch, Shvartsman VS paper
%* De Prisco Dynamic Configurations paper 
%* De Prisco new PODC submission, 2001.
\begin{thebibliography}{100}

\bibitem[KD96]{corel}
I.~Keidar and D.~Dolev.
\newblock Efficient message ordering in dynamic networks.
\newblock In {\em 15th ACM Symposium on Principles of Distributed Computing
  (PODC)}, pages 68--76, May 1996.
\newblock \verb+casestudies/corel-podc96.ps+.

\bibitem[FLS]{FLS99-sub}
Alan Fekete, Nancy Lynch, and Alex Shvartsman.
\newblock Specifying and using a partitionable group communication service.
\newblock {\em ACM Transactions on Computer Systems}. 
\newblock To appear.  \verb+casestudies/TOCS.ps+. 

\bibitem[PFLS99]{DFLS99}
R.~De Prisco, A.~Fekete, N.~Lynch, and A.A. Shvartsman.
\newblock A dynamic primary configuration group communication service.
\newblock In Prasad Jayanti, editor, {\em Distributed Computing {\rm
  Proceedings of DISC'99 - 13th International Symposium on Distributed
  Computing, Bratislava, Slovak Republic, September 1999}}, volume 1693 of {\em
  Lecture Notes in Computer Science}, pages 64--78, Bratislava, Slovak
  Republic, 1999. Springer-Verlag-Heidelberg.
\newblock \verb+casestudies/disc99.ps+.

\bibitem[DL]{DepriscoL-sub}
Roberto DePrisco and Nancy Lynch.
\newblock An algorithm for replicated atomic objects.
\newblock Submitted for publication. \verb+casestudies/deprisco.ps+.

\end{thebibliography}

\noindent
Byzantine failures are considered in:
%* Castro PhD thesis

\begin{thebibliography}{100}
\bibitem[Cas00]{Castro}
Miguel Castro.
\newblock {\em Practical {B}yzantine Fault Tolerance}.
\newblock PhD thesis, Department of Electrical Engineering and Computer
  Science, Massachusetts Institute of Technology, November 2000.

\end{thebibliography}

\section{Reliable network communication}

This application area involves a range of protocols, at different
layers, to implement reliable point-to-point or multicast
communication in unreliable networks.
Some of these protocols provide interesting safety guarantees;
we can also study performance properties, under
a range of assumptions about the behavior of the underlying network
and about the input load.
Since there are so many communication protocols around, students have
a lot of options in choosing subjects to study formally.

\noindent
Simple examples include a send-receive channel and a multicast
channel, as described, for example, in:
%* Distributed algorithms, Ch. 14.

\begin{thebibliography}{100}
\bibitem[Lyn96c]{Lynch-bookchap14}
Nancy Lynch.
\newblock {\em Distributed Algorithms}.
\newblock Morgan Kaufmann Publishers, Inc., San Mateo, CA, March 1996.
\newblock Chapter 14.

\end{thebibliography}

\noindent
Another simple example is a ``totally ordered multicast'' channel that
delivers messages everywhere, in a consistent order, as specified, for
example, in:
%* Fekete, L,S
\begin{thebibliography}{100}


\bibitem[FLS]{FLS99-sub}
Alan Fekete, Nancy Lynch, and Alex Shvartsman.
\newblock Specifying and using a partitionable group communication service.
\newblock {\em ACM Transactions on Computer Systems}. \\
\newblock To appear. \verb+casestudies/TOCS.ps+.
\end{thebibliography}
\noindent
An ``obligatory'' example for formal methods for communication is the
Alternating Bit Protocol, described, e.g., in: 
\begin{thebibliography}{100}
\bibitem[BSW69]{BartlettSW69}
K.A. Bartlett, R.A. Scantlebury, and P.T. Wilkinson.
\newblock A note on reliable full-duplex transmission over half-duplex links.
\newblock {\em Communications of the ACM}, 12(5):260--261, May 1969.

\bibitem[Lyn96d]{Lynch-bookchap22}
Nancy Lynch.
\newblock {\em Distributed Algorithms}.
\newblock Morgan Kaufmann Publishers, Inc., San Mateo, CA, March 1996.
\newblock Chapter 22.

\bibitem[Lam00e]{Lamport-chap13}
Leslie Lamport.
\newblock Specifying concurrent systems with {TLA+}. {P}reliminary draft,
  December 2000.
\newblock Chapter 13.
\end{thebibliography}

\noindent
The connection set-up part of TCP has interesting safety and liveness
properties: 
%* Comer's books
\begin{thebibliography}{100}


\bibitem[Com00]{Comer-volume1}
Douglas~E. Comer.
\newblock {\em Internetworking with {TCP/IP}: Principles, Protocols, and
  Architectures}, volume~1.
\newblock Prentice-Hall, 2000.

\bibitem[CS01]{ComerS-volume3}
Douglas~E. Comer and David~L. Stevens.
\newblock {\em Internetworking with {TCP/IP}: Client-Server Programming and
  Applications}, volume~3.
\newblock Prentice-Hall, 2001.

\bibitem[Lyn96d]{Lynch-bookchap22}
Nancy Lynch.
\newblock {\em Distributed Algorithms}.
\newblock Morgan Kaufmann Publishers, Inc., San Mateo, CA, March 1996.
\newblock Chapter 22.
\end{thebibliography}

\noindent
Protocols that build and maintain spanning trees form an important
part of many communication systems:

\begin{thebibliography}{100}
\bibitem[Luh00]{Luhrs}
Chris Luhrs.
\newblock Distributed spanning tree algorithms coded in {IOA}: Challenge
  problems for software analysis and synthesis methods ver. 1.3, October 2000.
\newblock Manuscript. \verb+casestudies/Luhrs-paper1.3.ps+.

\bibitem[AW00]{Adjie-Winoto}
William Adjie-Winoto.
\newblock A self-configuring resolver architecture for resource discovery and
  routing in device networks.
\newblock Master's thesis, Massachusetts Institute of Technology, May 2000.
\end{thebibliography}
\noindent
Now, focusing on multicast, and progressing from protocols with fewer
guarantees to protocols with more guarantees: \\
IP multicast protocols for routing and group membership are described in:
% Routing:
%* Deering paper on IP multicast...
%% Group membership IGMP, 
%* Overview from 3COM 
\begin{thebibliography}{100}
\bibitem[DC90]{DC90}
Stephen~E. Deering and David~R. Cheriton.
\newblock {Multicast Routing in Datagram Internetworks and Extended LANs}.
\newblock {\em ACM Transactions on Computer Systems (TOCS)}, 8(2):85--110, May
  1990.

\bibitem[Dee89]{IGMPv1}
Stephen~E. Deering.
\newblock {Host Extensions for IP Multicasting}.
\newblock Technical Report (RFC1112), Internet Engineering Task Force (IETF),
  August 1989.
\newblock Obsoletes RFCs 988 and 1054.

\bibitem[Fen97]{IGMPv2}
William~C. Fenner.
\newblock {Internet Group Management Protocol, Version 2}.
\newblock Technical Report (RFC2236), Internet Engineering Task Force (IETF),
  November 1997.
\newblock Updates RFC 1112.

\bibitem[CDF]{IGMPv3}
Brad Cain, Steve Deering, Bill Fenner, Isidor Kouvelas, and Ajit Thyagarajan.
\newblock {Internet Group Management Protocol, Version 3}.
\newblock {Internet-Draft}, Internet Engineering Task Force (IETF), November
  2000.
\newblock Proposed Update to RFC 2236.

\bibitem[SM97]{SM97}
Chuck Semeria and Tom Maufer.
\newblock {Intoduction to IP Multicast Routing}.
\newblock {Internet-Draft (Informational)}, Internet Engineernig Task Force,
  July 1997.
\newblock Also, Technical Memo, Networking Solutions Center, 3Com
  Corporation.

\end{thebibliography}
\noindent
Scalable Reliable Multicast (SRM), Bimodal Multicast, and similar
algorithms try hard to deliver multicast messages, but do not make
absolute guarantees.  It should be interesting to formulate some
claims about what they guarantee.
%* SRM paper (Floyd, et al.) 
%* Birman, Hayden?  Bimodal mcast
%* Papadopoulos (router-assisted)
\begin{thebibliography}{100}

\bibitem[FJM]{FJMLZ97}
Sally Floyd, Van Jacobson, Steve McCanne, Ching-Gung Liu, and Lixia Zhang.
\newblock {A reliable multicast framework for light-weight sessions and
  application level framing}.
\newblock {\em IEEE/ACM Transactions on Networking}, 5(6), December 1997.

\bibitem[BHO]{Birman-etal}
Kenneth Birman, Mark Hayden, Oznur Ozkasap, Zhen Xiao, Mihai Budiu, and Yaron
  Minsky.
\newblock Bimodal multicast.
\newblock {\em ACM Transactions on Computer Systems}, 17(2), May 1999.


\bibitem[PPV98]{PPV98}
Christos Papadopoulos, Guru Parulkar, and George Varghese.
\newblock An error control scheme for large-scale multicast applications.
\newblock In {\em Proc. 17th Annual Joint Conference of the IEEE Computer and
  Communications Societies (IEEE/INFOCOM'98)}, volume~3, pages 1188--1196,
  March 1998.
 
\end{thebibliography}

\noindent
Group communication algorithms guarantee strong (view-oriented)
consistency and reliability conditions; see, e.g.:
%* Corel paper
\begin{thebibliography}{100}

\bibitem[KD96]{corel}
I.~Keidar and D.~Dolev.
\newblock Efficient message ordering in dynamic networks.
\newblock In {\em 15th ACM Symposium on Principles of Distributed Computing
  (PODC)}, pages 68--76, May 1996.
\newblock \verb+casestudies/corel-podc96.ps+.

%* De Prisco DVS 
\bibitem[DFLS98]{DePriscoFLS98-sub}
Roberto DePrisco, Alan Fekete, Nancy Lynch, and Alex Shvartsman.
\newblock A dynamic view-oriented group communication service.
\newblock In {\em Proceedings of the 17th Annual ACM SIGACT-SIGOPS Symposium on
  Principles of Distributed Computing}, pages 227--236, Puerto Vallarta,
  Mexico, June-July 1998.
\newblock Also, technical memo in progress. \verb+casestudies/DVS.ps+. 

\end{thebibliography}
\section{Algorithms and services for mobile communication systems}

Mobile communication leads to a new set of communication algorithms.
Some of these deal with basic communication tasks like locating
participants and routing messages to them:

\begin{thebibliography}{100}


%* Royer, Perkins.  Multicast Operations of the Ad-hoc On-Demand
%Distance Vector Routing Protocol. MOBICOM 1999

\bibitem[RP99]{RoyerPerkins}
Elizabeth~M. Royer and Charles~E. Perkins.
\newblock Multicast operations of the ad-hoc on-demand distance vector routing
  protocol.
\newblock In {\em MOBICOM '99, The Fifth Annual ACM/IEEE International
  Conference on Mobile Computing and Networking}, pages 207--218, Seattle,
  Washington, USA, August 1999.\\
\newblock \verb+casestudies/royerperkins.pdf+.

\bibitem[KK00]{karp00}
Brad Karp and H.~T. Kung.
\newblock {GPSR}: Greedy perimeter stateless routing for wireless networks.
\newblock In {\em Proceedings of the ACM/IEEE Sixth Annual International
  Conference on Mobile Computing and Networking (Mobicom 2000)}, Boston, MA,
  2000.

\bibitem[BMSU99]{bose99}
P.~Bose, P.~Morin, I.~Stojmenovic, and J.~Urrutia.
\newblock Routing with guaranteed delivery in ad hoc wireless networks.
\newblock In {\em Third International Workshop on Discrete Algorithms and
  Methods for Mobile Computing and Communications (DIALM99)}, 1999.

\bibitem[Joh94]{dsr}
David~B. Johnson.
\newblock Routing in ad hoc networks of mobile hosts.
\newblock In {\em IBM Mobile Computing Workshop}, 1994.

\bibitem[BJM99]{dsr-draft}
Josh Broch, David Johnson, and David Maltz.
\newblock The {D}ynamic {S}ource {R}outing protocol for mobile ad hoc networks.
\newblock Internet draft (work in progress), Internet Engineering Task Force
  (IETF), October 1999.
\newblock
  \verb+www.ietf.org/internet-drafts/draft-ietf-manet-dsr-03.txt+.

\bibitem[PB94]{dsdv}
Charles~E. Perkins and Pravin Bhagwat.
\newblock Highly dynamic {D}estination-{S}equenced {D}istance-{V}ector routing
  ({DSDV}) for mobile computers.
\newblock In {\em SIGCOMM'94 - ACM Conference on Communications, Architectures,
  Protocols, and Applications}, pages 234--244, London, England,
  August/September 1994.

\bibitem[PRD99]{aodv}
Charles Perkins, Elizabeth Royer, and Samir~R. Das.
\newblock {A}d hoc {O}n demand {D}istance {V}ector ({AODV}) routing.
\newblock Internet draft (work in progress), October 1999.
\newblock \verb+www.ietf.org/internet-drafts/draft-ietf-manet-aodv-04.txt+.


\bibitem[PC97b]{tora}
Vincent~D. Park and M.~Scott Corson.
\newblock A highly adaptive distributed routing algorithm for mobile wireless
  networks.
\newblock In {\em Proceedings of the Sixteenth IEEE Conference on Computer
  Communications (INFOCOM'97)}, pages 1405--1413, Kobe, Japan, April 1997.


\bibitem[LJC]{mobicom00}
Jinyang Li, John Jannotti, Douglas S. J.~De Couto, David~R. Karger, and Robert
  Morris.
\newblock A scalable location service for geographic ad hoc routing.
\newblock In {\em ACM Mobicom 2000}, Boston, MA, 2000.
\end{thebibliography}
% [[[Doug De Couto will send some other citations.]]]

\noindent
Other problems, such as leader election and resource allocation, can
also be addressed in this new setting:
%* Walter, Welch, Vaidya.  A Mutual Exclusion Algorithm for Ad Hoc
%Mobile Networks.  To appear in a special issue of Telecommunication
%Systems Journal, 2001. (in dial-M workshop in 98).

\begin{thebibliography}{100}

\bibitem[WWV]{WalterWelchVaidya}
Jennifer Walter, Jennifer~L. Welch, and Nitin Vaidya.
\newblock A mutual exclusion algorithm for ad hoc mobile networks.
\newblock To appear in a special issue of {\em Telecommunication Systems
  Journal}, 2001. Also, In {\em Second International Workshop on Discrete
  Algorithms and Methods for Mobile Computing and Communications (DIAL-M
  workshop)}, Dallas, Texas, October, 1998). \verb+casestudies/balt.ps+.

\bibitem[HPS]{Hatzis-etal}
Kostas~P. Hatzis, George~P. Pentaris, Paul~G. Spirakis, Vasilis~T. Tampakas,
  and Richard~B. Tan.
\newblock Fundamental control algorithms in mobile networks.
\newblock In {\em Eleventh Annual ACM Symposium on Parallel Algorithms and
  Architectures (SPAA)}, pages 251--260, Saint-Malo, France, June 1999.

\bibitem[MWV00]{MalpaniWelchVaidya}
Navneet Malpani, Jennifer~L. Welch, and Nitin Vaidya.
\newblock Leader election algorithms for mobile ad hoc networks.
\newblock In {\em Fourth International Workshop on Discrete Algorithms and
  Methods for Mobile Computing and Communications (DIAL-M)}, Boston, MA, August
  2000. \verb+casestudies/dialm00.ps+.

\end{thebibliography}
\noindent
The following deals with group-oriented communication in mobile
networks:
%* Welch, MOBICOM 01 submission
\begin{thebibliography}{100}
\bibitem[MVW]{Mobicom01-sub}
Navneet Malpani, Nitin Vaidya, and Jennifer Welch.
\newblock Distributed token circulation in mobile ad hoc networks.
\newblock Submitted for publication. \verb+casestudies/Mobicom01-sub.ps+.

\noindent
The Oxygen project may also provide some interesting case studies
for design of mobile applications.
\end{thebibliography}
\noindent
An interesting aspect of this case study will be to try to express some
guarantees about what the algorithms do in cases where the
participants are constantly moving, perhaps with some bounds on their
speed.

\section{Automated transportation systems}

\noindent
This case study involves hybrid systems, which combine discrete and
continuous behavior.
Some preliminary hybrid system modeling examples include a simple
delay buffer that just replicates its (discrete and continuous) input,
but time $d$ later;
% [[[Composition, abstraction.]]]
a simple audio control protocol:
\begin{thebibliography}{100}
\bibitem[BPV94]{VaandragerBP94}
Doeko Bosscher, Indra Polak, and Frits Vaandrager.
\newblock Verification of an audio control protocol.
\newblock In H.~Langmaack, W.-P.~de Roever, and J.~Vytopil, editors, {\em
  Proceedings of the Third International School and Symposium on Formal
  Techniques in Real Time and Fault Tolerant Systems. (FTRTFT'94)}, volume 863
  of {\em Lecture Notes in Computer Science}, pages 170--192, L\"{u}beck,
  Germany, September 1994. Springer-Verlag.
\newblock Full version available as Report CS-R9445, CWI, Amsterdam, July 1994.
\end{thebibliography}
and an aircraft altitude switch:
\begin{thebibliography}{100}
\bibitem[Lev]{ASW-leveson}
Nancy~G. Leveson.
\newblock Sample intent specification: Altitude switch.
\newblock Massachusetts Institute of Technology, Safeware Engineering
  Corporation. \verb+casestudies/ASW-leveson.ps+.

\end{thebibliography}

\noindent
In general, the kinds of properties one can prove for hybrid systems
include ``safety'' properties in a real-world sense, time bounds,
and properties saying that values of certain real-valued variables
stay within some limits or track some trajectories.
Automated transportation provides good examples for modeling and analysis.
Some models for simple vehicle maneuvers are given in:

\begin{thebibliography}{100}
\bibitem[WL96]{WeinbergLynch96}
H.~B. Weinberg and Nancy Lynch.
\newblock Correctness of vehicle control systems: A case study.
\newblock In {\em 17th IEEE Real-Time Systems Symposium}, pages 62--72,
  Washington, D. C., December 1996.
\newblock \verb+casestudies/RTSS96.ps+.

\bibitem[LL98a]{LivadasL98-hybrid}
Carolos Livadas and Nancy~A. Lynch.
\newblock Formal verification of safety-critical hybrid systems.
\newblock In S.~Sastry and T.A. Henzinger, editors, {\em Hybrid Systems:
  Computation and Control {\rm (First International Workshop, HSCC'98,
  Berkeley, CA, USA, April, 1998)}}, number 1386 in Lecture Notes in Computer
  Science, pages 253--272. Springer Verlag, 1998.
\newblock \verb+casestudies/HS98.ps+.

\bibitem[DL97]{DolginovaLynch}
Ekaterina Dolginova and Nancy Lynch.
\newblock Safety verification for automated platoon maneuvers: A case study.
\newblock In Oded Maler, editor, {\em Hybrid and Real-Time Systems {\rm
  (International Workshop, HART'97, Grenoble, France, March 1997)}}, volume
  1201 of {\em Lecture Notes in Computer Science}, pages 154--170.
  Springer-Verlag, 1997.
\newblock \verb+casestudies/platoons.ps+.

\bibitem[LL98]{LygerosLynch-hybrid98}
John Lygeros and Nancy Lynch.
\newblock Strings of vehicles: Modeling and safety conditions.
\newblock In S.~Sastry and T.A. Henzinger, editors, {\em Hybrid Systems:
  Computation and Control {\rm (First International Workshop, HSCC'98,
  Berkeley, CA, USA, April, 1998)}}, number 1386 in Lecture Notes in Computer
  Science, pages 273--288. Springer Verlag, 1998.
\newblock \verb+casestudies/strings.ps+.
\end{thebibliography}
\noindent
Some more complicated examples arise in air-traffic management:

\begin{thebibliography}{100}
\bibitem[LL98a]{LivadasL98-hybrid}
Carolos Livadas and Nancy~A. Lynch.
\newblock Formal verification of safety-critical hybrid systems.
\newblock In S.~Sastry and T.A. Henzinger, editors, {\em Hybrid Systems:
  Computation and Control {\rm (First International Workshop, HSCC'98,
  Berkeley, CA, USA, April, 1998)}}, number 1386 in Lecture Notes in Computer
  Science, pages 253--272. Springer Verlag, 1998.
\newblock \verb+casestudies/HS98.ps+.

\bibitem[JC00]{JacksonChapin}
Daniel Jackson and John Chapin.
\newblock Redesigning air-traffic control: A case study in software design.
\newblock {\em IEEE Software}, May/June 2000.
\newblock \verb+sdg.lcs.mit.edu/~dnj/publications.html#6894+.
\end{thebibliography}

\section{Object-oriented programming} 

This case study has a different character from the others.
It isn't mostly about modeling and analyzing a collection of
algorithms.
Rather, the problem is to develop techniques for modeling program
objects and their interactions, in object-oriented programs (think
Java).
The techniques should allow for reasoning about the behavior of the
program, not just about object interfaces.
Specific examples that arise in the course of developing these general
methods can be used as case studies for the math methods and tools of
this course.

\noindent
Traditional forms of data abstraction treat the case of
self-contained concrete objects implementing self-contained abstract
objects.  See, e.g.,
%* Guttag, Liskov book. 
\begin{thebibliography}{100}
\bibitem[LG01]{LiskovGuttag-book}
Barbara Liskov and John Guttag.
\newblock {\em Program Development in {J}ava: Abstraction, Specification, and
  Object-Oriented Design}.
\newblock Addison-Wesley, 2001.

\end{thebibliography}
These two levels, and the connection between them, can be modeled
using state machines.  See, e.g.
%* 6042 notes, lecture 10.

\begin{thebibliography}{100}
\bibitem[Lyn00b]{6042-fall00-lec10}
Nancy Lynch.
\newblock 6.042 lecture notes, Fall 2000.
\newblock Lecture 10. \verb+casestudies/6042-L10.ps+.

\end{thebibliography}



However, the traditional frameworks are not adequate for representing
complications such as: 
objects that are not self-contained, but interact with (or
``contain'') other objects;
mutability/immutability; and data sharing. 

\noindent
For starters, we might consider an abstract ``assemblage'' of finite
sequences (or queues) that share tails.
Since this sharing is visible to programs that use the queues in the
assemblage, it must be represented in any abstract model of the
assemblage.
Such an assemblage can be modeled as a state machine.
A variety of implementations are possible (e.g., using sharing of
representations, or using separate representations with consistency
constraints); these can be modeled and shown to implement the
specification.
Note that this assemblage is different (abstractly) from an assemblage
of queues that don't share tails; different implementations would work
for this kind of abstraction.

\noindent
We might consider containment relations, e.g., between 
``container'' objects and the objects they ``contain''.
% it's probably
% useful to think of this relationship as an interaction via calls and
% returns. 
What does it mean for one container object to implement another?
We need models for mutable and immutable collections of mutable and
immutable objects, and results about which implement which others.
State machines should be able to help.

\noindent
More elaborate patterns of object interactions can be found, for
example, in:

%* Gamma, Helm, Johnson, Vlissides.  Design patterns: Elements of
%Reusable Object-Oriented Software
% observer pattern? others?

\begin{thebibliography}{100}
\bibitem[GHJV94]{GammaHJV}
Erich Gamma, Richard Helm, Ralph Johnson, and Vlissides.
\newblock {\em Design Patterns: Elements of Reusable Object-Oriented Software}.
\newblock Professional Computing. Addison-Wesley, 1994.
\end{thebibliography}
\end{document}







