\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}

\makeatletter
 \def\@biblabel#1{\hfill}  % Produces the label for a \bibitem[...]
\makeatother
\input{macros-course}

\newcommand{\tool}[1]{\noindent [TOOL: #1 ]}

\begin{document}
\handout{readinglist}{Course Outline, Readings, and Tools}{February 6, 2001}

This course will explore the available state-machine-based methods for
modeling and analyzing complex systems and will attempt to determine
what is needed to make them more useful in practice. 
Students will study and learn to use a broad set of modeling
techniques and analysis tools, and will apply them to case studies in
areas such as data management in distributed networks, reliable network
communication, mobile computing, automated transportation, and
object-oriented programming.

The course will be organized according to increasing complexity of
system features to be modeled.
We will start with basic, unstructured, untimed state machines, 
considering first safety properties and then liveness properties.
We will proceed to consider composition, then add complications of
timing, hybrid continuous/discrete behavior, and probability.
At each step, we will study the basic mathematical foundations and
study and use some of the available tools.

% [[[Joanne:  All papers from this handout must be collected for me,
% for the other staff members, and for the students' use. 
%
% First, all papers for which we can get .ps versions should be put
% into 6.897/papers subdirectory, in sub-subdirectories I've set up,
% according to the six sections fo the course (safety, liveness,
% etc.).
% Then all these papers must be pointed to from the course Web pages,
% for downloading.  I think that will mean making extra copies of
% these in a special Web directory.  
% I will need a paper copy of evertying, for my own preparation use.
%
% For those papers for which we can't get .ps files, we'll have to
% make paper copies ourselves for me to bring to class.
% That will be a bit of a pain, but is unavoidable.
% 
% For the first day, I will want to bring copies in any case, of the
% first few papers:
% lecture notes 8, 9 and 10, and the CWI paper, and xeroxes of chapter
% 8 of my book.
%
% The books will need copies on reserve.]]]

\section{Simple Asynchronous Systems, Safety Properties}

\subsection{Mathematical Foundations}
\label{sc-safety-foundations}

\noindent
[3 classes]  Leader: Nancy Lynch

\noindent
The main ideas here are state machines, invariants, labeled state
machines, I/O automata, abstraction functions, and abstraction relations.
These are introduced in:

\begin{thebibliography}{100}

\bibitem[Lyn00a]{6042-fall00}
Nancy Lynch.
\newblock 6.042 lecture notes, Fall 2000.
\newblock \verb+safety/6042-L08..9..10.ps+.



% [[[Joanne:  Copy the .ps files for these into the course
% papers/safety subdirectory, under 6042-lecture8.ps, etc.  
% All papers from Section 1 of this handout for which we can obtain
% .ps versions should be put into that subdirectory.  
% See general instructions above, for making this and other papers
% available.]]]

\bibitem[LT89]{LynchT89}
Nancy~A. Lynch and Mark~R. Tuttle.
\newblock An introduction to input/output automata.
\newblock {\em CWI-Quarterly}, 2(3):219--246, September 1989.
\newblock Centrum voor Wiskunde en Informatica, Amsterdam, The Netherlands.
  Technical Memo MIT/LCS/TM-373, Laboratory for Computer Science,
Massachusetts Institute of Technology, Cambridge, MA 02139, November
1988.    
\verb+safety/CWI89.ps+.

\bibitem[Lyn96a]{Lynch-bookchap8}
Nancy Lynch.
\newblock {\em Distributed Algorithms}.
\newblock Morgan Kaufmann Publishers, Inc., San Mateo, CA, March 1996.
\newblock Chapter 8.
% Joanne put 3 copies of the book on reserve.  Also for day 1,
% make copies of just chapter 8.]]]

\end{thebibliography}

\noindent
Lamport describes a mathematical state-machine model with an
associated logic (TLA).  For now, we will consider the safety aspects of
this work, then return to the liveness aspects later.
\begin{thebibliography}{100}

\bibitem[Lam94]{Lamport91}
Leslie Lamport.
\newblock The temporal logic of actions.
\newblock {\em ACM Transactions on Programming Languages and Systems},
  16(3):872--923, May 1994. 
\newblock \verb+safety/Lamport-tla-toplas.ps+.

\end{thebibliography}

\noindent
Manna and Pnueli describe ``reactive systems''.  Again, we will begin
with safety aspects, returning to liveness later.

\begin{thebibliography}{100}
\bibitem[Pnu77]{Pnueli77}
Amir Pnueli.
\newblock The temporal logic of programs.
\newblock In {\em Proceedings of the 18th Annual Symposium on Foundations of
  Computer Science}, pages 46--57, Providence, Rhode Island, October-November
  1977. IEEE.
%

\bibitem[Pnu81]{Pnueli81}
Amir Pnueli.
\newblock The temporal semantics of concurrent programs.
\newblock {\em Theoretical Computer Science}, 13:45--60, 1981.
%

%\bibitem[MP83]{MannaPnueli-popl83}
%Zohar Manna and Amir Pnueli.
%\newblock How to cook a temporal proof system for your pet language.
%\newblock In {\em Proceedings of the Tenth Annual ACM Symposium on the
%  Principles of Programming Languages (POPL)}, pages 141--154, Austin, Texas,
%  January 1983.
%

\bibitem[MP94]{MannaPnueli-94}
Z.~Manna and A.~Pnueli.
\newblock Temporal verification diagrams.
\newblock In {\em Proceedings of the International Symposium on Theoretical
  Aspects of Computer Software}, volume 789 of {\em Lecture Notes in Computer
  Science}, pages 726--765. Springer-Verlag, April 1994.  
\newblock \verb+safety/MannaP-diagrams.ps+.

\bibitem[MP92a]{MannaP92-safety}
Zohar Manna and Amir Pnueli.
\newblock {\em The Temporal Logic of Reactive and Concurrent Systems:
  Specification}.
\newblock Springer-Verlag, New York, 1992.
\newblock The safety parts.
% Joanne:  Put 3 copies on reserve.]]]

\bibitem[MP95]{MannaP95}
Zohar Manna and Amir Pnueli.
\newblock {\em Temporal Verification of Reactive Systems: Safety}.
\newblock Springer-Verlag, New York, 1995.
% Joanne:  3 copies on reserve]]]

\end{thebibliography}

\noindent
Various kinds of simulation relations and abstraction mappings are
described in:
\begin{thebibliography}{100}

\bibitem[LV95]{LV93I}
Nancy Lynch and Frits Vaandrager.
\newblock Forward and backward simulations --- {P}art {I}: Untimed systems.
\newblock {\em Information and Computation}, 121(2):214--233,
September 1995.  
\newblock \verb+safety/IC95.ps+.

\bibitem[dRE98]{deRoeverEngelhardt}
Willem-Paul de~Roever and Kai Engelhardt.
\newblock {\em Data Refinement: Model-Oriented Proof Methods and their
  Comparison}.
\newblock Cambridge University Press, 1998.
%2 copies on reserve]]]

\bibitem[Jen99]{Jensen97}
Henrik~Ejersbo Jensen.
\newblock {\em Abstraction-Based Verification of Distributed Systems}.
\newblock PhD thesis, Department of Computer Science, Institute for Electronic
  Systems, Aalborg University, Aalborg, Denmark, June 1999.
\newblock R-99-5005.
%2 copies on reserve]]]%%also-- online in safety section of papers.

\end{thebibliography}

\noindent
A hierarchical model for describing state machines and a corresponding
visual formalism, appear in:

\begin{thebibliography}{100}

\bibitem[Har87]{Harel-statecharts}
David Harel.
\newblock Statecharts: A visual formalism for complex systems.
\newblock {\em Science of Computer Programming}, 8:231--274, 1987.
%.ps file not available; have hardcopy

\bibitem[Har88]{Harel-cacm88}
D.~Harel.
\newblock On visual formalisms.
\newblock {\em Communications of the ACM}, 31(5):514--530, 1988.
\newblock (Reprinted in {\em Diagrammatic Reasoning} (Chandrasekaran et al.,
  eds), AAAI Press and MIT Press, 1995, pp. 235-271, and in {\em High Integrity
  System Specification and Design} (Bowen and Hinchey, eds.), Springer-Verlag,
  London, 1999, pp. 623-657.)  
%%safety/p514-harel.pdf.  This file will not print the whole paper.

\end{thebibliography}


%%%%%%%%%%%%%%%%%%%%

\subsection{Tools}

\subsubsection{Languages and parsers}

\noindent
The IOA formal language for specifying input/output automata is
described in:
\begin{thebibliography}{100}


\bibitem[GLV00]{GLV-IOA-manual}
Stephen~J. Garland, Nancy~A. Lynch, and Mandana Vaziri.
\newblock I{OA}: A language for specifying, programming and validating
  distributed systems, December 2000.
\newblock User and Reference Manual. \verb+safety/ioaManual.ps+.


\bibitem[GL00]{IOA-leavens}
Stephen~J. Garland and Nancy~A. Lynch.
\newblock {\em Using {I/O} Automata for Developing Distributed Systems},
  chapter~13, pages 285--312.
\newblock Cambridge University Press, USA, 2000.  
\newblock \verb+safety/ioa-leavens.ps+.

\end{thebibliography}

The IOA language has a front end, which parses and checks static
semantics.  It also produces internal Java data structures
representing the various parts of automata, but those aren't yet
hooked up to usable validation tools.  This represents work in
progress.

\tool{IOA front end: parser and checker}\\
Students can find links to the manual plus other information about
IOA and the IOA Toolkit in \\
\verb+http://nms.lcs.mit.edu/~garland/IOA/+.\\
A direct link to the front end checker is 
\verb+http://nms.lcs.mit.edu/~garland/IOA/ioaCheck.tar.gz.+\\

\noindent
The TLA+ language is a formal specification language based on
Lamport's TLA logic.
This language is described in Lamport's new book, of which we have
a draft version:

\begin{thebibliography}{100}

\bibitem[Lam00a]{Lamport-chap1-7}
Leslie Lamport.
\newblock Specifying concurrent systems with {TLA+}.  {P}reliminary
draft, December 2000.
\newblock Chapters 1-7.
\end{thebibliography}

Descriptions written in TLA+ can be checked using the TLA+ parser:\\
\tool{TLA+ parser}
% [[[Rui:  Need instructions for students to access this.  How does
% this work?]]]

\subsubsection{Model checkers}

\noindent
[3 classes]  Leaders:  Nancy Lynch, Daniel Jackson, Paul Attie

\noindent
We will first focus on model-checking for safety properties, and later
on liveness.
An overview of the ideas in various model checkers appears in: 

\begin{thebibliography}{100}

\bibitem[CGP99]{ClarkeGP-99}
E.~M. Clarke, Orna Grumberg, and Doron Peled.
\newblock {\em Model Checking}.
\newblock MIT Press, December 1999.
% Joanne:  Put 3 copies on reserve]]]

\bibitem[CGL96]{CGL-markt}
E.~M. Clarke, O.~Grumberg, and D.~E. Long.
\newblock Model checking.
\newblock In {\em A survey on model checking, abstraction and composition},
  volume 152 of {\em Nato ASI Series F}. Springer-Verlag, 1996.\\
\newblock \verb+safety/CGL-markt.ps+.


%\bibitem[CGL94]{ClarkeOL-94}
%E.~M. Clarke, Orna Grumberg, and D.~E. Long.
%\newblock Verification tools for finite-state concurrent systems.
%\newblock In {\em A Decade of Concurrency: Reflections and Perspectives},
%  volume 803 of {\em Lecture Notes in Computer
%Science}. Springer-Verlag, 1994.  
%\newblock \verb+safety/CGL-tools.ps+.

\end{thebibliography}

\noindent
Symbolic model checking is discussed in:

\begin{thebibliography}{100}

\bibitem[McM92]{SMV-McMillan}
K.L. McMillan.
\newblock {\em Symbolic Model Checking: an Approach to the State Explosion
  Problem}.
\newblock PhD thesis, Carnegie Mellon University, 1992.
\newblock CMU-CS-92-131.
% 2 copies on reserve]]]
\end{thebibliography}

\tool{SMV}
\verb+http://sra.itc.it/tools/nusmv/+
% [[[Needs to be downloaded, and instructions given to students to
% obtain it.]]]

\noindent
Some selected basic model-checking papers are:

\begin{thebibliography}{100}

\bibitem[CES86]{ClarkeES86}
E.~M. Clarke, E.~A. Emerson, and A.~P. Sistla.
\newblock Automatic verification of finite-state concurrent systems using
  temporal-logic specifications.
\newblock {\em ACM Transactions on Programming Languages and Systems},
  8(2):244--263, 1986.
\newblock
\verb+http://theory.lcs.mit.edu/classes/6.897/papers/safety/p244-Clarke.pdf+.

\bibitem[ES]{EmersonSistla-journal}
E.~Allen Emerson and A.~Prasad Sistla.
\newblock Symmetry and model checking.
\newblock {\em Formal Methods in System Design}, 9(1/2):105-130,
1996.  
\newblock \verb+safety/EmersonS-symmetry.ps+.

\bibitem[EOD94]{ClarkeGL-toplas}
E. M. Clarke, O. Grumberg, and D. E. Long.
\newblock Model checking and abstraction.
\newblock {\em ACM Transactions on Programming Languages and Systems
(TOPLAS)}, 16(5):1512--, September 1994. 
\newblock \verb+safety/CGL-abstraction.ps+.

\end{thebibliography}   

\noindent
The SPIN model checker is described in:

\begin{thebibliography}{100}
\bibitem[Hol91]{SPIN-Holzmann}
Gerard~J. Holzmann.
\newblock {\em Design and Validation of Computer Protocols}.
\newblock Prentice Hall Software Series, New Jersey, 1991.
\end{thebibliography}
% 3 copies on reserve.  Also, I need a copy for me.]]]

\tool{SPIN}
% [[[Needs download instructions.]]]
% [[[Rui:  Needs to be downloaded, and instructions given to students to
% obtain it.]]]

\noindent
The TLC model-checker is described in:
\begin{thebibliography}{100}
\bibitem[Lam00b]{Lamport-chap12-13}
Leslie Lamport.
\newblock Specifying concurrent systems with {TLA+} preliminary draft, December
  2000.
\newblock Chapters 12-13.
\end{thebibliography}

\noindent
\tool{TLC}
% [[[Rui:  Needs to be downloaded, and instructions given to students to
% obtain it.]]]

\subsubsection{Invariant discovery tools}

[1 class]  Leader:  Michael Ernst

The notion of dynamic detection of likely invariants, and the Daikon tool
for doing so, is described in:

%* Ernst, M., Cockrell, Griswold, Notkin.
%Dynamically discovering likely program invariants to support program
%evolution.
%IEEE TOSE Feb. 2001

\begin{thebibliography}{100}
\bibitem[ECGN01]{ErnstCGN2001}
Michael~D. Ernst, Jake Cockrell, William~G. Griswold, and David Notkin.
\newblock Dynamically discovering likely program invariants to support program
  evolution.
\newblock {\em IEEE Transactions on Software Engineering}, 27(2):1--25,
February 2001. 
\newblock \verb+safety/Ernst-invariants-tse.pdf+.

\end{thebibliography}
\tool{Daikon}

\subsubsection{Theorem provers}

\noindent
[3 classes]  Leader:  Steve Garland

An overview of interactive theorem-proving ideas and tools will be
given, with some discussion of the particular theorem prover LP and
high-level pointers to other theorem provers like PVS and Isabelle.
Some sources for overview material:

%* Handbook for Theoretical Computer Science, Volume II.
%Chapter 6, on term rewriting systems;
%Chapter 13, on algebraic specification;
%Chapters 14-16, on logics for proving things about programs.

\begin{thebibliography}{100}
\bibitem[han90]{handbook-tcs}
Handbook of theoretical computer science: Volume b, formal models and
  semantics, 1990.
\newblock Chapter 6, on term rewriting systems; Chapter 13, on algebraic
  specification; Chapters 14-16, on logics for proving things about programs.

%* Larch Prover paper 


\bibitem[GG]{GarlGut-LP-online}
Stephen~J. Garland and John~V. Guttag.
\newblock L{P}, the {L}arch {P}rover.\\
\newblock \verb+www.sds.lcs.mit.edu/~garland/LP/overview.html.+.



%%[[Nancy-Steve suggested Rushby spin99 and Shankar concur00. do you
%%want to add them? I put the refs in coursebib.bib.]]


\bibitem[ORRetal]{ORR+96}
S.~Owre, S.~Rajan, J.M. Rushby, N.~Shankar, and M.~Srivas.
\newblock P{VS}: Combining specification, proof checking, and model checking.
\newblock In {\em CAV '96}, volume 1102 of {\em Lecture Notes in Computer
  Science}, pages 411--414. Springer Verlag, 1996.
\newblock \verb+safety/pvs-cav96.ps.gz+. 

\bibitem[SOR93]{ShankarOR-pvs}
N.~Shankar, Sam Owre, and John Rushby.
\newblock The {PVS} proof checker: {A} reference manual.
\newblock Technical report, Computer Science Lab, SRI Intl., Menlo Park, CA,
  1993. Also see the Language Reference, System Guide, and Prover
Guide all available from \verb+pvs.csl.sri.com/manuals.html+.


%Joanne:  Add note to this citation (in coursebib.bib and repaste)
%Also see the Language Reference, System Guide, and Prover Guide, all
%available from \verb+ pvs.csl.sri.com/manuals.html+.]]][[done]]

\bibitem[Pau94]{Paulson-springer-94}
L.~C. Paulson.
\newblock {\em Isabelle: A Generic Theorem-Prover}.
\newblock LNCS 828. Springer-Verlag, 1994.\\
\newblock \verb+www.cl.cam.ac.uk/Research/HVG/Isabelle.+

\end{thebibliography}


\noindent
We will learn one theorem prover:  MIT's own Larch Prover:

\tool{Larch Prover}

\verb+http://www.sds.lcs.mit.edu/~garland/LP/overview.html+


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Simple Asynchronous Systems, Liveness Properties}

\noindent
[2 classes]  Leaders:  Nancy Lynch, Paul Attie

\subsection{Foundations}

\noindent
Simple termination properties are described in:
\begin{thebibliography}{100}
\bibitem[Lyn00]{6042-fall00}
Nancy Lynch.
\newblock 6.042 lecture notes, Fall 2000.
\newblock Lectures 8, 9, 10. 
\newblock \verb+safety/6042-L08..9..10.ps+.

\end{thebibliography}

\noindent
Basic definitions of safety vs. liveness appear in:
\begin{thebibliography}{100}
\bibitem[AS85]{AlpernSchneider-ipl}
Bowen Alpern and Fred~B. Schneider.
\newblock Defining liveness.
\newblock {\em Information Processing Letters}, 21(4):181--185, October 1985.
%hardcopy only

\bibitem[AS87]{AlpernSchneider-dc}
Bowen Alpern and Fred~B. Schneider.
\newblock Recognizing safety and liveness.
\newblock {\em Distributed Computing}, 2(3):117--126, 1987.
\end{thebibliography}

\noindent
A treatment of fairness for I/O automata appears in:
\begin{thebibliography}{100}
\bibitem[Lyn96a]{Lynch-bookchap8}
Nancy Lynch.
\newblock {\em Distributed Algorithms}.
\newblock Morgan Kaufmann Publishers, Inc., San Mateo, CA, March 1996.
\newblock Chapter 8.
\end{thebibliography}

\noindent
The following gives an overview of temporal logics, which are used to
prove liveness properties:
\begin{thebibliography}{100}
\bibitem[Eme90]{Emerson90}
E.~A. Emerson.
\newblock Temporal and modal logic.
\newblock In J.~van Leeuwen, editor, {\em Handbook of Theoretical Computer
  Science: Volume B, Formal Models and Semantics}, pages 995--1072. North
  Holland Pub. Co./MIT Press, 1990.
\newblock Chapter 16.
\end{thebibliography}
% Joanne:  For the Handbook, put 3 copies on reserve.  (The whole
% handbook)]]]

The work by Manna and Pnueli, listed in Section \ref{sc-safety-foundations}, 
describes liveness features in temporal logics.
We will revisit this here, and will also consider: 
\begin{thebibliography}{100}
\bibitem[Lam00d]{Lamport-chap8}
Leslie Lamport.
\newblock Specifying concurrent systems with {TLA+}.  {P}reliminary
draft, December 2000.
\newblock Chapter 8.

\bibitem[CM88]{ChandyM88}
K.~Mani Chandy and Jayadev Misra.
\newblock {\em Parallel Program Design: A Foundation}.
\newblock Addison-Wesley Publishing Co., Reading, MA, 1988.
% Joanne:  2 copies on reserve]]]

%* Emerson, Chin Laung Lai, Model checking under generalized fairness
%  constraints.UT TR.  [[Per Emerson: the journal paper reporting this
%  results is: ]E. A. Emerson and C.-L. Lei,
%``Modalities for Model Checking: Branching Time Logic Strikes Back'',
%{\it Science of Computer Programming}, vol.\ 8, vol. 8, pp. 275-306, 1987.

\bibitem[EL84]{EmersonLei}
E.~Allen Emerson and Chin~Laung Lei.
\newblock Modalities for model checking: Branching time logic strikes back.
\newblock {\em Science of Computer Programming}, 8:275--306, 1987.
\newblock Earlier version Technical Report CS-TR-84-20, Department of Computer
  Science, University of Texas, 1984.

%* Vardi, M.  Alternating Automata:  Checking Truth and Validity for
 % Temporal Logics Buchi automata, Vardi paper

\bibitem[Var97]{Vardi}
Moshe Vardi.
\newblock Alternating automata: Checking truth and validity for temporal
  logics.
\newblock In William McCune, editor, {\em Automated Deduction-CADE-14 (14th
  International Conference on Automated Deduction, Townsville, North
  Queensland, Australia, July, 1997)}, volume 1249 of {\em Lecture Notes in
  Computer Science}. Springer Verlag, 1997.
\newblock \verb+liveness/cade97.ps+.

%* Attie, P.  PODC 99 paper.
\bibitem[Att99]{Attie-podc99}
Paul~C. Attie.
\newblock Liveness-preserving simulation relations.
\newblock In {\em ACM Symposium on the Principles of Distributed Computing
  (PODC)}, Atlanta, Georgia, May 1999.
\newblock \verb+liveness/Attie-podc99+.


\end{thebibliography}
%\noindent
%The following describes a method for proving liveness properties using
%certain kinds of ``lattice'' diagrams:
%\begin{thebibliography}{100}
%\bibitem[MBSU98]{MBSU-amast}
%Zohar Manna, Anca Browne, Henny~B. Sipma, and Tomas~E. Uribe.
%\newblock Visual abstractions for temporal verification.
%\newblock In {\em AMAST'98}, volume 1548 of {\em Lecture Notes in Computer
%  Science}, pages 28--41. Springer-Verlag, 1998.
%\end{thebibliography}

\subsection{Tools}

\noindent
Most model-checking tools can be used to prove liveness properties:\\
\tool{SMV}\\
\tool{SPIN}\\
\tool{TLC}\\

\noindent
The following thesis describes a tool, built upon Isabelle, for verifying
safety and liveness properties of I/O automata:
\begin{thebibliography}{100}
\bibitem[M\"98]{Mueller-phd}
Olaf M\"uller.
\newblock {\em A Verification Environment for I/O Automata Based on Formalized
  Meta-Theory}.
\newblock PhD thesis, Technische Universitat Munchen, 1998.\\
\newblock \verb+liveness/OM-PhD.ps+.
\end{thebibliography}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Asynchronous Systems with Composition}

\noindent
[4 classes]  Leaders:  Nancy Lynch, Daniel Jackson, Paul Attie

\subsection{Foundations}

\noindent
Composition for I/O automata is described in:
\begin{thebibliography}{100}
\bibitem[LT89]{LynchT89}
Nancy~A. Lynch and Mark~R. Tuttle.
\newblock An introduction to input/output automata.
\newblock {\em CWI-Quarterly}, 2(3):219--246, September 1989.
\newblock Centrum voor Wiskunde en Informatica, Amsterdam, The Netherlands.
  Technical Memo MIT/LCS/TM-373, Laboratory for Computer Science, Massachusetts
  Institute of Technology, Cambridge, MA 02139, November 1988.
\verb+safety/CWI89.ps+.

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

\bibitem[SGSAL98]{GLSS93-jour}
Roberto Segala, Rainer Gawlick, J{\o}rgen S{\o}gaard-Andersen, and Nancy Lynch.
\newblock Liveness in timed and untimed systems.
\newblock {\em Information and Computation}, 141(2):119--171, March
1998. 
\newblock \verb+composition/GLSS-liveness.ps+.
\end{thebibliography}

\noindent
Work on composition using shared variables appears in: 
\begin{thebibliography}{100}
\bibitem[AL93]{AbadiLamport-compose}
Martin Abadi and Leslie Lamport.
\newblock Composing specifications.
\newblock {\em ACM Transactions on Programming Languages and Systems},
  15(1):73--132, January 1993.
\newblock Also appeared as SRC Research Report 66. \\
\verb+composition/src66-acm.ps+.

\bibitem{AbadiLamport-conjoin}
Martin Abadi and Leslie Lamport.
\newblock Conjoining Specifications.
\newblock {\em Toplas}, 17(3):507-534, May, 1995. 
\newblock \verb+composition/src118.ps.Z.+


\bibitem[Lam98]{Lamport-harder}
Leslie Lamport.
\newblock Composition: A way to make proofs harder.
\newblock In Willem-Paul de~Roever, Hans Langmaack, and Amir Pnueli, editors,
  {\em Compositionality: The Significant Difference (Proceedings of the
  COMPOS'97 Symposium)}, volume 1536 of {\em Lecture Notes in Computer
  Science}, pages 402--423, 1998.\\
\verb+composition/lamport-proofs-harder.pdf+.

\bibitem[Lam00c]{Lamport-chap10}
Leslie Lamport.
\newblock Specifying concurrent systems with {TLA+}. {P}reliminary
draft, December 2000.
\newblock Chapter 10.

\bibitem[AH99]{AlurHenzinger-reactive}
R.~Alur and T.~A. Henzinger.
\newblock Reactive modules.
\newblock {\em Formal Methods in System Design}, 15(1):7--48, 1999.
\newblock Earlier version in {\em Proceedings of the 11th IEEE Symposium on
  Logic in Computer Science}, pp. 207-218, 1996. \verb+composition/Lics96T.ps+.

%journal version same as proceedings per Rajeev]]
\end{thebibliography}

\noindent
Work on the ``assume-guarantee'' approach to compositional reasoning
appears in:
%* Jones, Cliff.  Specification and design of (parallel) programs.
%IFIP 83. 
%[[[Joanne:  Needs full citation.  But first check with Daniel that
%this is the correct paper---might not be.]]][[emailed Daniel 1/29/01]]

\noindent
An example of building state machines from other state machines using
methods arising from object ``inheritance'' is described in:
\begin{thebibliography}{100}
\bibitem[KKLS00]{KKLS}
Idit Keidar, Roger Khazan, Nancy Lynch, and Alex Shvartsman.
\newblock An inheritance-based technique for building simulation proofs
  incrementally.
\newblock In {\em 22nd International Conference on Software Engineering
  (ICSE)}, pages 478--487, Limerick, Ireland, June 2000.
\newblock \verb+composition/icse00.ps+.
\end{thebibliography}

\noindent
Process algebras, which admit parallel composition and many other
kinds of combination operators, are described in:
\begin{thebibliography}{100}
\bibitem[Hoa85]{Hoare85}
C.~A.~R. Hoare.
\newblock {\em Communicating Sequential Processes}.
\newblock Prentice-Hall International, United Kingdom, 1985.
% 2 copies on reserve]]]

\bibitem[Mil99a]{Milner99-basic}
Robin Milner.
\newblock {\em Communicating and mobile systems: the Pi-Calculus}.
\newblock Cambridge University Press, United Kingdom, 1999.
\newblock Part I.
%3 copies on reserve]]]
\end{thebibliography}

\noindent
Dynamic systems, which include dynamic creation of state machines
(which then get composed with the previously-existing state machines)
are discussed in:
\begin{thebibliography}{100}

\bibitem[Mil99b]{Milner99-pi}
Robin Milner.
\newblock {\em Communicating and mobile systems: the Pi-Calculus}.
\newblock Cambridge University Press, United Kingdom, 1999.
\newblock Part II.

\bibitem[AtLy]{AttieLynch}
Paul Attie and Nancy Lynch.
\newblock Dynamic Input/Ouput Automata: A Formal Model for Dynamic Computation.
\newblock Manuscript.
\newblock \verb+composition/DIOA.ps+.

\bibitem[AtLy]{AttieLynch-tr}
Paul Attie and Nancy Lynch.
\newblock Dynamic Input/Output Automata: a Formal Model for Dynamic
Systems.  
\newblock Technical Report, College of Computer Science, Northeastern
University, January 2001. 
\newblock \verb+composition/Attie-dsioa-tr.ps+.

\end{thebibliography}

\subsection{Tools}

\noindent
Compositional model-checking is described in: 
\begin{thebibliography}{100}
\bibitem[CGP99?]{ClarkeGP-99-chap13}
E.~M. Clarke, Orna Grumberg, and Doron Peled.
\newblock {\em Model Checking}.
\newblock MIT Press, December 1999.
\newblock Chapter 13.
%%reserved

\bibitem[GL94]{GrumbergLong-94}
O.~Grumberg and D.~E. Long.
\newblock Model checking and modular verification.
\newblock {\em ACM Transactions on Programming Languages and Systems (TOPLAS)},
  16(3):843--871, May 1994.  
\newblock \verb+papers/composition/Gl-modular.ps+.

\end{thebibliography}

\noindent
The following tool handles reactive modules: 
\tool{Mocha} \verb+http://www.cis.upenn.edu/~mocha/+

\noindent
Relational models provide ways of describing complex state structure.
Some background on models of this kind appears in:

\begin{thebibliography}{100}
%*Ian Hayes. Specification Case Studies. Second Edition, Prentice Hall, 1993.
\bibitem[Hay93]{Hayes-book}
Ian Hayes.
\newblock {\em Specification Case Studies}.
\newblock Prentice Hall, 1993.
\newblock Second Edition.

%* Jim Woodcock and Jim Davies. Using Z: Specification, Refinement, and Proof.
%Prentice Hall, 1996.
\bibitem[WD96]{WoodcockDavies-book}
Jim Woodcock and Jim Davies.
\newblock {\em Using {Z}: Specification, Refinement, and Proof}.
\newblock Prentice Hall, 1996.


%* Martin Fowler. Analysis Patterns: Reusable Object Models. Addison Wesley,
%1997.
\bibitem[Fow97]{Fowler-book}
Martin Fowler.
\newblock {\em Analysis Patterns: Reusable Object Models}.
\newblock Addison Wesley, 1997.

%* Daniel Jackson. Alloy: A Lightweight Object Modelling Notation. Technical
%Report MIT-LCS-TR-797, MIT Lab for Computer Science, February 2000. To
%appear, ACM Transactions on Software Engineering and Methodology. Available
%at: http://sdg.lcs.mit.edu/~dnj/publications.

\bibitem[Jac00a]{Jackson00-tr}
Daniel Jackson.
\newblock Alloy: A lightweight object modelling notation.
\newblock Technical Report MIT-LCS-TR-797, MIT Lab for Computer Science,
  February 2000.
\newblock To appear in {\em ACM Transactions on Software Engineering and
  Methodology}. \verb+composition/alloy-journal.pdf+.
\end{thebibliography}

The Alloy analyzer is described in:
%* Daniel Jackson. Automating First-order Relational Logic. Prof. ACM Conf. on
%Foundations of Software Engineering, San Diego, CA, November 2000.
\begin{thebibliography}{100}
\bibitem[Jac00b]{Jackson00-proc}
Daniel Jackson.
\newblock Automating first-order relational logic.
\newblock In {\em Proceedings of the ACM Conference on Foundations of Software
  Engineering}, San Diego, CA, November 2000.\\
\verb+composition/alloy-fse00.pdf+.

\end{thebibliography}

\tool{The Alloy analyzer} \\
\verb+http://sdg.lcs.mit.edu/alloy+

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Timed Systems}

\noindent
[4 classes]  Leader:  Nancy Lynch

\subsection{Foundations}

\noindent
The first batch of sources deals with the timed I/O automaton model:
\begin{thebibliography}{100}
\bibitem[Lyn96b]{Lynch-bookchap23}
Nancy Lynch.
\newblock {\em Distributed Algorithms}.
\newblock Morgan Kaufmann Publishers, Inc., San Mateo, CA, March 1996.
\newblock Chapter 23.

\bibitem[LV96]{LV95II-jour}
Nancy Lynch and Frits Vaandrager.
\newblock Forward and backward simulations --- {P}art {II}: Timing-based
  systems.
\newblock {\em Information and Computation}, 128(1):1--25, July 1996.
\newblock \verb+timed/IC96.ps+.

\bibitem[SGSAL98]{GLSS93-jour}
Roberto Segala, Rainer Gawlick, J{\o}rgen S{\o}gaard-Andersen, and Nancy Lynch.
\newblock Liveness in timed and untimed systems.
\newblock {\em Information and Computation}, 141(2):119--171, March
1998. 
\verb+composition/GLSS-liveness.ps+.
\end{thebibliography}

\noindent
Timed automata (without the inputs and outputs) are described in:
\begin{thebibliography}{100}
\bibitem[AD94]{AlurD94}
Rajeev Alur and David~L. Dill.
\newblock A theory of timed automata.
\newblock {\em Theoretical Computer Science}, 126(2):183--235, April 1994.
\newblock A preliminary version appears in {\em Proceedings of 17th ICALP, LNCS
  443, under the title Automata for modeling real-time systems, pages 322-335,
  1990}. \verb+timed/Icalp90.ps+.


\bibitem[Alu]{Alur-nato}
Rajeev Alur.
\newblock Timed automata.
\newblock NATO summer school, 1998. \verb+timed/Nato97.ps+.

\end{thebibliography}

\noindent
TLA also has ways of dealing with timing.  These are discussed in: 
\begin{thebibliography}{100}
\bibitem[Lam00d]{Lamport-chap9}
Leslie Lamport.
\newblock Specifying concurrent systems with {TLA+}. {P}reliminary
draft, December 2000.
\newblock Chapter 9.
\end{thebibliography}

\noindent
Composition of timed systems
\begin{thebibliography}{100}
\bibitem[AH97]{AlurH-97}
Rajeev Alur and Thomas~A. Henzinger.
\newblock Modularity for timed and hybrid systems.
\newblock In {\em Proceedings of Ninth International Conference on Concurrency
  Theory}, volume 1243 of {\em Lecture Notes in Computer Science}, 1997.
\newblock \verb+timed/Concur97.ps+.


\end{thebibliography}

\noindent
We may also briefly visit basic notions of performance modeling/analysis in
timed state machine settings.
%  Conditional performance analysis

\subsection{Tools}

\noindent
Uppaal is a nice tool for analyzing timed automata; lots of examples
have been worked out: \\ 
\tool{Uppaal}
See http://www.docs.uu.se/docs/rtmv/uppaal/

\noindent
Other work on analyzing timed automata:
\begin{thebibliography}{100}
\bibitem[Yov98]{Yovine}
S. Yovine.
\newblock Model checking timed automata.
\newblock In G. Rozenberg and F. Vaandrager, editors {\em Lectures on Embedded
Systems}, volume 1494 of {\em Lecture Notes in Computer Science},
October 1998.
\newblock \verb+timed/Yovine98.ps.gz.+
\end{thebibliography}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Hybrid Systems}

[4 classes]  Leader:  Nancy Lynch

\subsection{Foundations}

\noindent
The following all give general modeling frameworks for hybrid systems:

\begin{thebibliography}{100}
\bibitem[LSV]{LynchSV00}
Nancy Lynch, Roberto Segala, and Frits Vaandraager.
\newblock Hybrid {I/O} automata revisited.
\newblock {\em Hybrid Systems: Computation and Control: Fourth International
  Workshop (HSCC'01)}, Lecture Notes in Computer Science, Roma, Italy, March
  2001. Springer-Verlag.
\newblock  \verb+hybrid/HIOA.ps+.


\bibitem[MMP92]{MalerMP91}
Oded Maler, Zohar Manna, and Amir Pnueli.
\newblock From timed to hybrid systems.
\newblock In J.~W. de~Bakker, C.~Huizing, and G.~Rozenberg, editors, {\em
  Real-Time: Theory in Practice (REX Workshop, Mook, The Netherlands, June
  1991)}, volume 600 of {\em Lecture Notes in Computer Science}, pages
  447--484. Springer-Verlag, 1992.
\newblock \verb+hybrid/hybrid-rex.ps+.



\bibitem[ACH]{AlurEtAl95}
R.~Alur, C.~Courcoubetis, N.~Halbwachs, T.~A. Henzinger, P.~H. Ho, X.~Nicollin,
  A.~Olivero, J.~Sifakis, and S.~Yovine.
\newblock The algorithmic analysis of hybrid systems.
\newblock {\em Theoretical Computer Science}, 138(1):3--34, 1995.  
\newblock \verb+hybrid/Des94.ps+.


\bibitem[AHH96]{RTSS93j}
R.~Alur, T.~A. Henzinger, and P.~H. Ho.
\newblock Automatic symbolic verification of embedded systems.
\newblock {\em IEEE Transactions on Software Engineering}, 22(3):181--201,
  1996.
\newblock \verb+hybrid/Rtss.ps+.


\bibitem[AH97]{AlurH-97}
Rajeev Alur and Thomas~A. Henzinger.
\newblock Modularity for timed and hybrid systems.
\newblock In {\em Proceedings of Ninth International Conference on Concurrency
  Theory}, volume 1243 of {\em Lecture Notes in Computer Science},
1997.  
\newblock \verb+timed/Concur97.ps+.



\bibitem[MS98]{MannaSipma}
Zohar Manna and Henny Sipma.
\newblock Deductive verification of hybrid systems using {ST}e{P}.
\newblock In {\em Hybrid Systems: Computation and Control}, volume 1386 of {\em
  Lecture Notes in Computer Science}. Springer-Verlag, 1998.
\newblock \verb+hybrid/sipma-hscc98.ps+.

\bibitem[KMP98]{KMP98}
Yonit Kesten, Zohar Manna and Amir Pnueli. 
\newblock Verification of Clocked and Hybrid Systems. 
\newblock In {\em Embedded Systems}, volume 1494 of {\em Lecture Notes in Computer Science}, Springer-Verlag, 1998. \\
\newblock \verb+hybrid/paper-clocked98.ps+.

\bibitem[KMP96]{KMP96}
Yonit Kesten, Zohar Manna and Amir Pnueli. 
\newblock Verifying Clocked Transition Systems. 
\newblock In {\em Hybrid Systems III}, vol. 1066 of {\em Lecture Notes in
Computer Science}, pages 13-40, Springer-Verlag, 1996. 
\newblock \verb+hybrid/pap-clocks96hybrid3.ps+. 

\end{thebibliography}

\noindent
This work has a control-theory flavor.  The second paper identifies some
continuous methods that can be used with hybrid I/O automata.
\begin{thebibliography}{100}
\bibitem[Bra95]{Branicky}
Michael~S. Branicky.
\newblock {\em Studies in Hybrid Systems: Modeling, Analysis, and Control}.
\newblock PhD thesis, Department of Electrical Engineering and Computer
  Science, Massachusetts Institute of Technology, Cambridge, MA, June
1995.  

\bibitem[BDL97]{BranickyDL96}
Michael~S. Branicky, Ekaterina Dolginova, and Nancy Lynch.
\newblock A toolbox for proving and maintaining hybrid specifications.
\newblock In P.~Antsaklis, W.~Kohn, A.~Nerode, and S.~Sastry, editors, {\em
  Hybrid Systems IV (Fourth International Conference on Hybrid Systems, Ithaca,
  NY, October 1996)}, volume 1273 of {\em Lecture Notes in Computer Science},
  pages 18--30. Springer Verlag, 1997.  
\newblock \verb+hybrid/BDL-toolbox.ps+.

\end{thebibliography}



\subsection{Tools}

\noindent
The HyTech tool is the best-known tool for modeling and analyzing
hybrid systems:

\begin{thebibliography}{100}
\bibitem[HHWT97]{HenzingerHoToi}
Thomas~A. Henzinger, Pei-Hsin Ho, and Howard Wong-Toi.
\newblock Hy{T}ech: a model checker for hybrid systems.
\newblock {\em Software Tools for Technology Transfer}, 1:110--122, 1997.\\
\newblock \verb+hybrid/hytech.ps+. 

\bibitem[Hen96]{Henzinger-lics96}
Thomas~A. Henzinger.
\newblock The theory of hybrid automata.
\newblock In {\em Proceedings of the 11th Annual IEEE Symposium on Logic in
  Computer Science (LICS 1996)}, pages 278--292, 1996.\\
\newblock \verb+hybrid/the_theory_of_hybrid_automata.ps+. 

\bibitem[HKPV98]{HenzingerKPV-jcss}
Thomas~A. Henzinger, Peter~W. Kopke, Anuj Puri, and Pravin Varaiya.
\newblock What's decidable about hybrid automata?
\newblock {\em Journal of Computer and System Sciences}, 57:94--124, 1998.\\
\newblock \verb+hybrid/whats_decidable_about_hybrid_automata.ps+.
\end{thebibliography}

\tool{Hytech}
\verb+http://www-cad.eecs.berkeley.edu/~tah/HyTech/+

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Probabilistic Systems}

\noindent
[2 classes]  Leader:  Nancy Lynch

\subsection{Foundations}

\noindent
A basic model for randomized distributed algorithms and systems
appears in: 


\begin{thebibliography}{100}

\bibitem[PSL00]{PSL98-jour}
Anna Pogosyants, Roberto Segala, and Nancy Lynch.
\newblock Verification of the randomized consensus algorithm of {A}spnes and
  {H}erlihy: a case study.
\newblock {\em Distributed Computing}, 13(3):155-186, July
2000. 
\newblock \verb+probability/PSL98-cgi.ps+.


\bibitem[Seg]{Segala-schools}
Roberto Segala.
\newblock Verification of randomized distributed algorithms.
\newblock Manuscript.

\bibitem[Seg95]{Segala95}
Roberto Segala.
\newblock {\em Modeling and Verification of Randomized Distributed Real-Time
  Systems}.
\newblock PhD thesis, Department of Electrical Engineering and Computer
  Science, Massachusetts Institute of Technology, May 1995.
\newblock Also, MIT/LCS/TR-676.  \verb+probability/TR-676.tar.gz.+
\end{thebibliography}

\noindent
An interesting open question is to define a basic mathematical model
that accommodates both hybrid and probabilistic behavior.
I don't know of any references on this topic.
This seems like a great basic research question.

\subsection{Tools}

\noindent
We don't plan to use any particular tools for modeling and analyzing
probabilistic systems.
The following sample reference describes a tool for probabilistic
performance analysis, based on a probabilistic Petri net model.

\begin{thebibliography}{100}
\bibitem[CMT89]{Trivedietal-spnp}
G.~Ciardo, J.~K. Muppala, and K.~S. Trivedi.
\newblock S{PNP}: Stochastic petri net package.
\newblock In {\em Proc. of 3rd International Workshop on Petri Nets and
  Performance Models}, pages 142--150, Kyoto, Japan, December, 1989.
\newblock \verb+probability/1989SPNP.ps+.

\end{thebibliography}

\end{document}








