{\rtf1\mac\deff2 {\fonttbl{\f0\fswiss Chicago;}{\f2\froman New York;}{\f3\fswiss Geneva;}{\f4\fmodern Monaco;}{\f12\fnil Z;}{\f13\fnil Zapf Dingbats;}{\f16\fnil Palatino;}{\f18\fnil Zapf Chancery;}{\f20\froman Times;}{\f21\fswiss Helvetica;}
{\f22\fmodern Courier;}{\f23\ftech Symbol;}{\f1263\fnil Palatino-Math;}{\f1302\fnil Helvetica-Math;}{\f2000\fnil Arial Narrow;}{\f2001\fnil Arial;}{\f2002\fnil Book Antiqua;}{\f2003\fnil Bookman Old Style;}{\f2004\fnil Century Gothic;}
{\f2005\fnil Courier New;}{\f2006\fnil Monotype Corsiva;}{\f2007\fnil Monotype Sorts;}{\f2008\fnil Century Schoolbook;}{\f2010\fnil Times New Roman;}{\f2011\fnil Wingdings;}{\f2515\fnil MT Extra;}{\f13473\fnil ClassicalGaramondBT-Math;}}
{\colortbl\red0\green0\blue0;\red0\green0\blue255;\red0\green255\blue255;\red0\green255\blue0;\red255\green0\blue255;\red255\green0\blue0;\red255\green255\blue0;\red255\green255\blue255;}{\stylesheet{\s242\qj\sb120 \f20\fs20 \sbasedon0\snext0 
page number;}{\s243\qj\sb120\tqc\tx4320\tqr\tx8640 \f20\fs20 \sbasedon0\snext243 footer;}{\s253\qj\sb180\keepn\tx480 \b\f20\fs20 \sbasedon254\snext0 heading 3;}{\s254\qj\sb180\keepn\tx480 \b\f20\fs20 \sbasedon255\snext0 heading 2;}{\s255\qj\sb360\tx480 
\b\f20 \sbasedon0\snext0 heading 1;}{\qj\sb120 \f20\fs20 \sbasedon222\snext0 Normal;}{\s2\qc\sb260\sa200 \b\f20\fs28 \sbasedon0\snext2 Title;}{\s3\qj\sb120\brdrt\brsp120\brdrdb \tqc\tx4320\tqr\tx8640 \f20\fs20 \sbasedon0\snext2 TopHeader;}{
\s4\qj\sb40\sa360\brdrb\brsp120\brdrdb \tqc\tx4140\tqr\tx8640 \f20\fs20 \sbasedon0\snext4 BottomHeader;}{\s5\qj\li240\sb120\tx480 \f20\fs20 \sbasedon0\snext5 Item;}{\s6\qj\fi-480\li480\sb120 \f20\fs20 \sbasedon0\snext6 HangIndent;}{
\s7\qj\fi-980\li980\sb120\tx980 \f20\fs20 \sbasedon0\snext7 Ref;}{\s8\qj\fi240 \f20\fs20 \sbasedon0\snext8 Indent;}{\s9\sb40\sa20\tx360\tx1260\tx2880\tx5400\tx7200 \f20\fs20 \sbasedon0\snext9 Syllabus;}{\s10\sb120 \f20\fs20 \sbasedon0\snext10 NoJustify;}{
\s11\li360\ri360\sb40\sa40\tx360\tx720\tx1800\tx2880\tx5400\tx7200 \v\f20\fs18 \sbasedon9\snext11 Syllabus Notes;}{\s12\qj\fi-360\li720\ri360\sb80 \f20\fs20 \sbasedon0\snext12 itemize;}}{\info{\title Course Info}{\subject Models of SW Systems}{\author 
David Garlan & Jeannette Wing}{\*\verscomm 1.3 RTF}}\widowctrl\ftnbj \sectd \sbknone\linemod0\linex0\cols1\endnhere \pard\plain \s3\qj\sb120\brdrt\brsp120\brdrdb \tqc\tx4320\tqr\tx8640 \f20\fs20 CMU MSE 15-671\tab Models of Software Systems\tab Fall 1995
\par 
\pard\plain \s2\qc\sb260\sa200 \b\f20\fs28 Course Information\par 
\pard\plain \s4\qj\sb40\sa360\brdrb\brsp120\brdrdb \tqc\tx4320\tqr\tx8640 \f20\fs20 Garlan & Wing\tab Handout 1\tab August 28, 1995\par 
\pard\plain \s255\qj\sb360\tx480 \b\f20 Instructors\par 
\pard\plain \sb120\tx2880\tx4800\tqr\tx8640 \f20\fs20 David Garlan\tab Jeannette Wing\line garlan@cs.cmu.edu\tab wing@cs.cmu.edu\line WeH 8020 (x8-5056)\tab WeH 8219 (x8-3068)\line Office: Fri 9:30-10:30\tab Office: Wed 12:00-1:00\line 
Moose: Fri 10:15-10:30\tab Moose: Wed: 1:45-1:00\par 
\pard\plain \s255\qj\sb360\tx480 \b\f20 Teaching Assistant\par 
\pard\plain \sb120 \f20\fs20 James Ivers\line jivers@cs.cmu.edu\line WeH 4615  (x8-5842)\line Office: Tue 4:00-5:00\line Moose: Tue 4:45-5:00\par 
\pard\plain \s255\qj\sb360\tx480 \b\f20 Secretary\par 
\pard\plain \s10\sb120 \f20\fs20 Cary Lund\line cary@cs.cmu.edu\line WeH: 8106 (x8-3853)\par 
\pard\plain \qj\sb120 \f20\fs20 \par 
\pard\plain \s255\qj\sb360\tx480 \b\f20 Objectives\par 
\pard\plain \qj\sb120 \f20\fs20 
Scientific foundations for software engineering depend on the use of precise, abstract models and logics for characterizing and reasoning about properties of software systems. There are a number of basic models and logics that over time have proven to be p
articularly import
ant and pervasive in the study of software systems. This course is concerned with that body of knowledge. It considers many of the standard models for representing sequential and concurrent systems, such as state machines, algebras and traces. It shows how
 different logics can be used to specify properties of software systems, such as functional correctness, deadlock freedom, and internal consistency. Concepts such as composition mechanisms, abstraction relations, invariants, non-determinism, inductive and 
denotational descriptions are recurrent themes throughout the course. \par 
\pard \qj\sb120 
By the end of the course you should be able to understand the strengths and weaknesses of certain models and logics, including state machines, algebraic and trace models, and temporal logics. You should be able to apply this understanding to select and des
cribe abstract formal models for certain classes of systems. Further, you should be able to reason formally about the elementary properties of modeled systems.\par 
\pard \qj\sb120\tqr\tx8640 {\fs14 \par 
\par 
\par 
\par 
\par 
}\pard \qr\sb120\tqr\tx8640 {\fs14 Version 1.2 of 8/15/95\par 
}\pard\plain \s255\qj\sb360\tx480 \b\f20 \page Organization\par 
\pard\plain \s6\qj\fi-480\li480\sb120 \f20\fs20 {\b Lectures}. Class will meet Monday & Wednesday,  10:30-11:50 am, in WeH 3420.\par 
\pard \s6\qj\fi-480\li480\sb120 {\b Computing}
. Some of the assignments may make use of tools that are part of the SCS software engineering environment. You will need an account on an SCS SunOS machine to use these tools. If you are an MSE student you will already have such an account. Other students 
should see the instructor after the first class to get an application form. There are a set of documents that describe the MSE tool facilities.\par 
\pard \s6\qj\fi-480\li480\sb120 {\b On-line materials. }Most of our course materials will be available electronically via the Web. To access this material point your favorite web browser to \par 
\pard \s6\qj\fi-480\li480\sb120 \tab \tab URL: http://www.cs.cmu.edu/afs/cs/academic/class/15671-f95/www/\par 
\pard \s6\qj\fi-480\li480\sb120 \tab There is also a class afs directory: /afs/cs/academic/class/15671-f95. It will contain various templates and documents that can be helpful in completing your homework.\par 
\pard \s6\qj\fi-480\li480\sb120 {\b Communication}. We have set up four mechanisms for out-of-class interaction.\par 
\pard \s6\qj\fi-480\li480\sb120 \tab 1.{\b  The Moose Lounge: } This is a virtual lounge for the MSE program. It is a \ldblquote place\rdblquote 
 that you can wander into electronically and partake of the discussion, or simply eavesdrop on what is going on. One of places you can visit inside the Moose is the Models Room
. While you are free to hang around the Moose at any time, each of the instructors has set aside a time when they will be in the Models Room for discussion or to answer questions. You can visit the Moose off the course home page
, where you will also find instructions on how to participate in Moose conversations. \par 
\pard \s6\qj\fi-480\li480\sb120 \tab 2. {\b The Course Bulletin Board. }We will use {\b cmu.cs.class.cs671 }to post questions/answers{\b  }
about homework and lectures. So you should plan to read it regularly. Feel free to use it yourself to post about topics of general interest for the other students. \par 
\pard \s6\qj\fi-480\li480\sb120 \tab 3. {\b Office Hours:} Each of the instructors and the TA has weekly office hours. These are listed on the previous page{\b \par 
}\pard \s6\qj\fi-480\li480\sb120 \tab 4. {\b Email: }We welcome email about the course at any time.\par 
\pard \s6\qj\fi-480\li480\sb120 {\b Readings}. Most lectures will have a reading assignment that we expect you to complete {\i before}{\b  }you come to class. Many of the reading assignments will be drawn from the two required {\b textbooks}
 for the course: {\i Software Engineering Mathematics}, by Woodcock and Loomes (SEM) and {\i Concrrent Systems: Formal Development in CSP}, by M.G. Hinchey and S.A. Jarvis [HJ]. Some readings are in the form of {\b handouts}
 to supplement some lectures; other additional readings are {\b technical} {\b papers}.  These will all be distributed as needed throughout the course.\par 
{\b Homeworks and Lab Exercises}. The course is organize
d around (roughly) weekly homeworks. The purpose of the assignments is to give you practice in using the models and logics of the course. In some cases where a model is supported by tools we may also assign one or more ungraded lab exercises. These are int
ended to give you practice in using the tools before you have to apply them on the homework problems. We encourage you to discuss your homework with other students, but the final write-up must be your own work. \par 
\pard \s6\qj\fi-480\li480\sb120 \tab Homeworks will be graded on a pass/fail bas
is. They will typically be assigned on a Wednesday and due at the beginning of class a week later. To give you the most opportunities to learn from the homework assignments, we will allow you to redo a homework that didn't receive a passing grade. A redone
 homework must be turned in at {\i the class following the one on which it is handed back}.\par 
\pard \s6\qj\fi-480\li480\sb120 {\b Extra copies of handout materials. }Extra copies of lecture slides, handouts, homework assignments, etc. will be available from Cary Lund, WeH 8106.\tab \par 
{\b Exams. }There will be a (take-home) mid-term {\b (handed out October 11, due October 13)} and a (in-class) final examination.\par 
\pard \s6\qj\fi-480\li480\sb120 {\b\v Homework Presentations.}{\v 
 For some homework assignments we will ask students to present their results on the day it is due. The purpose of this is to give the presenter practice at explaining a solution to others and to give the rest of the class a chance to see how someone else s
olved the problem. These presentations will be assigned on a rotating basis, as necessary and will be ungraded.\par 
}\pard \s6\qj\fi-480\li480\sb120 {\b Grading}. The course grade will be determined as a combination of four factors: homework exercises (50%), midterm exam (15%) final exam (25%),  instructors\rquote  judgment (10%).\par 
\pard\plain \s255\qj\sb360\pagebb\tx480 \b\f20 Schedule\par 
\pard\plain \s9\sb40\sa20\tx360\tx1260\tx2880\tx5400\tx7200 \f20\fs20 {\b\ul #\tab Date\tab Topic\tab Subtopic\tab Reading\tab Homework\par 
}\pard \s9\sb40\sa20\tx360\tx1260\tx2880\tx5400\tx7200 1\tab M 8/28\tab Introduction\tab Course intro; What\rquote s a model?\par 
\pard\plain \s11\li360\ri360\sb40\sa40\tx360\tx720\tx1800\tx2880\tx5400\tx7200 \v\f20\fs18 Garlan (+ Wing)\line \tab Lecture\tab A. Course administration, philosophy, goals\line \tab \tab B. Why formal models are important: ball game\line \tab \tab 
C. Math review : material of SEM ch1\line \tab \tab ideas: formal languages, semantics, inference systems, proof, theory\line \tab \tab Note: warn them that reading may not all make sense \line \tab Handout\tab Handout 1: Course Notes\line \tab \tab 
account requests\line \tab \tab HW 1 (D) - Logic\par 
\pard\plain \s9\sb40\sa20\tx360\tx1260\tx2880\tx5400\tx7200 \f20\fs20 2\tab F 9/1\tab Foundations\tab Logic\tab [SEM 1-4]\tab HW 1\par 
\pard\plain \s11\li360\ri360\sb40\sa40\tx360\tx720\tx1800\tx2160\tx5400\tx7200 \v\f20\fs18 Garlan\line \tab Lecture\tab A. Propositional and Predicate logic\line \tab \tab \tab quantifier notation, free/bound variables, truth tables, etc.\line \tab \tab 
B. Proof techniques\line \tab \tab \tab Reasoning with equivalences (ala SEM) \line \tab \tab \tab Natural Deduction -- with two examples\line \tab \tab \tab Skim other and give pointer to later lecture\line \tab Handout\tab HW 2 (D) - More logic\par 
\pard\plain \s9\sb40\sa20\tx360\tx1260\tx2880\tx5400\tx7200 \f20\fs20 3\tab *W 9/6\tab \tab Sets, Relations, Functions\tab [SEM 5-6.3,7.1-7.3]\tab HW 2\par 
\pard\plain \s11\li360\ri360\sb40\sa40\tx360\tx720\tx1800\tx2880\tx5400\tx7200 \v\f20\fs18 Garlan\par 
\tab Lecture\tab A. Set theory: set notation, set comprehension, power sets\line \tab \tab B. Relations, functions, Z funny symbols\tab \line \tab Handout\tab HW 3 (J) -  Proof (not including induction)\line \tab Missing\tab Wing\par 
\pard\plain \s9\sb40\sa20\tx360\tx1260\tx2880\tx5400\tx7200 \f20\fs20 4\tab M 9/11\tab \tab Proof Techniques\tab []\tab \par 
\pard\plain \s11\li360\ri360\sb40\sa40\tx360\tx720\tx1800\tx2880\tx5400\tx7200 \v\f20\fs18 Wing\par 
\tab Lecture\tab A. Equational reasoning\line \tab \tab B. Proof techniques:  illustrate with one point rule, contradiction, case analysis, etc.\line \tab Handout\tab Handout 2, 3(J)\tab \par 
\pard\plain \s9\sb40\sa20\tx360\tx1260\tx2880\tx5400\tx7200 \f20\fs20 5\tab W 9/13\tab \tab Sequences & Induction\tab [Handout 2,3,SEM 8] HW 3\par 
\pard\plain \s11\li360\ri360\sb40\sa40\tx360\tx720\tx1800\tx2880\tx5400\tx7200 \v\f20\fs18 Garlan\par 
\tab Lecture\tab A. Sequences and operations on them\line \tab \tab B. Induction over integers, structural induction with example on binary trees\tab \line \tab Handout\tab HW 4 (D&J) -  induction + state machine basics\line \tab Missing\tab Wing\par 
\pard\plain \s9\sb40\sa20\tx360\tx1260\tx2880\tx5400\tx7200 \f20\fs20 6\tab M 9/18\tab State Machines\tab Basic concepts\tab []\tab \par 
\pard\plain \s11\li360\ri360\sb40\sa40\tx360\tx720\tx1800\tx2880\tx5400\tx7200 \v\f20\fs18 Wing\line \tab Lecture\tab A. States, events, traces, behavior\line \tab \tab B. Infinite vs. finite\line \tab Handout\tab Handout 4\par 
\pard\plain \s9\sb40\sa20\tx360\tx1260\tx2880\tx5400\tx7200 \f20\fs20 7\tab W 9/20\tab \tab Variations\tab [Handout 4]\tab HW 4\par 
\pard\plain \s11\li360\ri360\sb40\sa40\tx360\tx720\tx1800\tx2880\tx5400\tx7200 \v\f20\fs18 Wing\par 
\tab Lecture\tab A.  Var to Val map\line \tab \tab B. Actions, with args and results, nondeterminism\line \tab Handout\tab Handout 5, HW 5 (J) - More state machines\par 
\pard\plain \s9\sb40\sa20\tx360\tx1260\tx2880\tx5400\tx7200 \f20\fs20 8\tab M 9/25\tab \tab Invariants\tab [Handout 5]\tab \par 
\pard\plain \s11\li360\ri360\sb40\sa40\tx360\tx720\tx1800\tx2880\tx5400\tx7200 \v\f20\fs18 Wing\par 
\tab Lecture\tab A. Reasoning about  state machines.\line \tab \tab B. Proving invariants\line \tab \tab C. No time for constraints; edification only.\line \tab Handout\tab Handout 6\line \tab Missing\tab Ivers\par 
\pard\plain \s9\sb40\sa20\tx360\tx1260\tx2880\tx5400\tx7200 \f20\fs20 9\tab W 9/27\tab Z\tab Introduction to Z\tab [Handout 6,Spi89]\tab HW 5\par 
\pard\plain \s11\li360\ri360\sb40\sa40\tx360\tx720\tx1800\tx2160\tx5400\tx7200 \v\f20\fs18 Garlan\line \tab Lecture\tab A. Introduce Z notation using Birthday Book\line \tab \tab \tab Schemas, robust specs, simple shema calculus operators\line \tab \tab 
B. How to use Fuzz\line \tab Handout\tab HW 6 (J&D) - Invariants + Simple Z spec\line \tab Missing\tab Ivers\par 
\pard\plain \s9\sb40\sa20\tx360\tx1260\tx2880\tx5400\tx7200 \f20\fs20 10\tab M 10/2\tab \tab Reasoning about Z Specs\tab [SEM 6.4,7.4]\tab \par 
\pard\plain \s11\li360\ri360\sb40\sa40\tx360\tx720\tx1800\tx2160\tx5400\tx7200 \v\f20\fs18 Garlan\line \tab Lecture\tab A. Preconditions, intialization\line \tab \tab B. Telephone net example\line \tab \tab \tab Framing\line \tab \tab \tab Invariants
\line \tab \tab \tab General reasoning\line \tab Handout\tab Handout 7(D) - Telephone net handout\par 
\pard\plain \s9\sb40\sa20\tx360\tx1260\tx2880\tx5400\tx7200 \f20\fs20 11\tab W 10/4\tab \tab Examples\tab [Handout 7,DG90]\tab HW 6\par 
\pard\plain \s11\li360\ri360\sb40\sa40\tx360\tx720\tx1800\tx2880\tx5400\tx7200 \v\f20\fs18 Garlan\par 
\tab Lecture\tab A. Example of Z specification\line \tab Handout\tab HW 7 (D) - More on Z. Reasoning about Telephone Net, Extending oscilloscope\par 
\pard\plain \s9\sb40\sa20\tx360\tx1260\tx2880\tx5400\tx7200 \f20\fs20 12\tab M 10/9\tab Abstraction\tab State Machines\tab []\tab \par 
\pard\plain \s11\li360\ri360\sb40\sa40\tx360\tx720\tx1800\tx2880\tx5400\tx7200 \v\f20\fs18 Wing\par 
\tab Lecture\tab A. Relating state machines: satisfies (no time for equivalence)\line \tab \tab B. Abstraction functions\line \tab \tab C. Examples: days, sets (if time)\line \tab Handout\tab Handouts 8, 9, 10, 11\par 
\pard\plain \s9\sb40\sa20\tx360\tx1260\tx2880\tx5400\tx7200 \f20\fs20 13\tab W 10/11\tab \tab Abstraction in Z\tab [Handouts 8-11]\tab HW 7\line \tab \tab \tab \tab \tab Midterm out\par 
\pard\plain \s11\li360\ri360\sb40\sa40\tx360\tx720\tx1800\tx2880\tx5400\tx7200 \v\f20\fs18 Garlan\line \tab Lecture\tab A. Data abstraction, \ldblquote abstraction schema\rdblquote \line \tab \tab B. Abstraction over relations\line \tab \tab 
C. Abstraction over Z operations\line \tab Handout\tab Midterm, (due 10/13)\line \tab Missing\tab Wing\line \tab Note\tab mid-semester grades due Oct 16 to Maria\par 
\pard\plain \s9\sb40\sa20\tx360\tx1260\tx2880\tx5400\tx7200 \f20\fs20 14\tab *W 10/18\tab Larch\tab Algebras\tab [SEM 11]\tab \par 
\pard\plain \s11\li360\ri360\sb40\sa40\tx360\tx720\tx1800\tx2880\tx5400\tx7200 \v\f20\fs18 Wing\line \tab Lecture\tab A. Review equational  theories, algebras\line \tab \tab B. Operational semantics (rewriting)\line \tab Handout\tab 
HW 8 (J) - Algebraic reasoning, GH93\line \tab Missing\tab Garlan\par 
\pard\plain \s9\sb40\sa20\tx360\tx1260\tx2880\tx5400\tx7200 \f20\fs20 15\tab M 10/23\tab \tab Interfaces\tab [GH93]\tab \par 
\pard\plain \s11\li360\ri360\sb40\sa40\tx360\tx720\tx1800\tx2880\tx5400\tx7200 \v\f20\fs18 Wing\line \tab Lecture\tab A. Relating specs to code\line \tab \tab B. Pre- and post-conditions at program module level\line \tab Handout\tab AS83\line \tab Missing
\tab Garlan\par 
\pard\plain \s9\sb40\sa20\tx360\tx1260\tx2880\tx5400\tx7200 \f20\fs20 16\tab W 10/25\tab Concurrency\tab Introduction to Concurrency\tab [AS83]\tab HW 8\par 
\pard\plain \s11\li360\ri360\sb40\sa40\tx360\tx720\tx1800\tx2880\tx5400\tx7200 \v\f20\fs18 Wing\line \tab Lecture\tab A. Basic concepts: synchronization and communication\line \tab \tab B. Shared memory vs. message passing\line \tab Handout\tab 
Handout 12,HW 9 (J) - Concurrency, BGHL, Bir89\line \tab Missing\tab Garlan\par 
\pard\plain \s9\sb40\sa20\tx360\tx1260\tx2880\tx5400\tx7200 \f20\fs20 17\tab M 10/30\tab \tab Composing State Machines\tab [Handout 12,BGHL{\i ,Bir89}]\tab \par 
\pard\plain \s11\li360\ri360\sb40\sa40\tx360\tx720\tx1800\tx2880\tx5400\tx7200 \v\f20\fs18 Wing\line \tab Lecture\tab A. Shared Memory Model: building a big state machine\line \tab \tab B. Implementing shared memory model: Threads interface\line \tab 
Handout\tab Handout 13\par 
\pard\plain \s9\sb40\sa20\tx360\tx1260\tx2880\tx5400\tx7200 \f20\fs20 18\tab W 11/1\tab CSP\tab Basic CSP\tab [Handout 13,\par 
\tab \tab \tab \tab HJ 1,2.1-9]\tab HW 9\par 
\pard\plain \s11\li360\ri360\sb40\sa40\tx360\tx720\tx1800\tx2880\tx5400\tx7200 \v\f20\fs18 Garlan\line \tab Lecture\tab A. Basic concepts: prefix, STOP, alphabet, choice, recursion, \line \tab \tab B. Parallelism, deadlock\line \tab \tab C. Communication
\line \tab Handout\tab HW 10 (D) - CSP I\par 
\pard\plain \s9\sb40\sa20\tx360\tx1260\tx2880\tx5400\tx7200 \f20\fs20 19\tab M 11/6\tab \tab Reasoning with CSP\tab [HJ 3.1-3,6]\tab \par 
\pard\plain \s11\li360\ri360\sb40\sa40\tx360\tx720\tx1800\tx2880\tx5400\tx7200 \v\f20\fs18 Garlan\line \tab Lecture\tab A. CSP semantics, laws, style\line \tab Handout\tab \par 
\pard\plain \s9\sb40\sa20\tx360\tx1260\tx2880\tx5400\tx7200 \f20\fs20 20\tab W 11/8\tab \tab Nondeterminism\tab [HJ 2.10,3.4-6]\tab HW 10\par 
\pard\plain \s11\li360\ri360\sb40\sa40\tx360\tx720\tx1800\tx2880\tx5400\tx7200 \v\f20\fs18 Garlan\line \tab Lecture\tab A. External/internal choice, \line \tab \tab B. Need for richer semantic model, failures, divergences\line \tab Handout\tab 
HW 11 (D) - CSP II\par 
\pard\plain \s9\sb40\sa20\tx360\tx1260\tx2880\tx5400\tx7200 \f20\fs20 21\tab M 11/13\tab \tab Applications and Extensions\tab [HJ 7, AG94]\tab \par 
\pard\plain \s11\li360\ri360\sb40\sa40\tx360\tx720\tx1800\tx2880\tx5400\tx7200 \v\f20\fs18 Garlan\line \tab Lecture\tab A. Intro to Wright, FDR(?), Timed CSP?\line \tab Handout\tab MP92  (Chapter 3)\par 
\pard\plain \s9\sb40\sa20\tx360\tx1260\tx2880\tx5400\tx7200 \f20\fs20 22\tab W 11/15\tab Temporal Logic\tab Linear Temporal Logic\tab [{\i MP92}]\tab HW 11\par 
\pard\plain \s11\li360\ri360\sb40\sa40\tx360\tx720\tx1800\tx2880\tx5400\tx7200 \v\f20\fs18 Wing\line \tab Lecture\tab A. Excerpts from Chapter 3 of Manna and Pnueli\line \tab Handout\tab HW 12 (J) - Temporal logic\par 
\pard\plain \s9\sb40\sa20\tx360\tx1260\tx2880\tx5400\tx7200 \f20\fs20 23\tab M 11/20\tab \tab Computational Tree Logic\tab []\tab \par 
\pard\plain \s11\li360\ri360\sb40\sa40\tx360\tx720\tx1800\tx2880\tx5400\tx7200 \v\f20\fs18 Wing\line \tab Lecture\tab A. More on linear TL\line \tab \tab B.  Intro to CTL based on CES\line \tab Handout\tab Pet77\par 
\pard\plain \s9\sb40\sa20\tx360\tx1260\tx2880\tx5400\tx7200 \f20\fs20 24\tab *M 11/27\tab Petri Nets\tab Introduction to Petri Nets\tab [Pet77]\tab HW 12\par 
\pard\plain \s11\li360\ri360\sb40\sa40\tx360\tx720\tx1800\tx2880\tx5400\tx7200 \v\f20\fs18 Garlan\line \tab Lecture\tab \line \tab Handout\tab HW 13 (D) - Petri Nets, Jen91\par 
\pard\plain \s9\sb40\sa20\tx360\tx1260\tx2880\tx5400\tx7200 \f20\fs20 25\tab W 11/29\tab \tab Reasoning about Petri Nets\tab [Jen91]\tab \par 
\pard\plain \s11\li360\ri360\sb40\sa40\tx360\tx720\tx1800\tx2880\tx5400\tx7200 \v\f20\fs18 Garlan\line \tab Lecture\tab \line \tab Handout\tab \par 
\pard\plain \s9\sb40\sa20\tx360\tx1260\tx2880\tx5400\tx7200 \f20\fs20 26\tab M 12/4\tab Intentionally left blank\tab \tab HW 13\tab \par 
\pard\plain \s11\li360\ri360\sb40\sa40\tx360\tx720\tx1800\tx2880\tx5400\tx7200 \v\f20\fs18 ???\line \tab Lecture\tab \line \tab Handout\tab \par 
\pard\plain \s9\sb40\sa20\tx360\tx1260\tx2880\tx5400\tx7200 \f20\fs20 27\tab W 12/6\tab Review for final\tab \par 
\tab \tab \par 
\pard\plain \s11\li360\ri360\sb40\sa40\tx360\tx720\tx1800\tx2880\tx5400\tx7200 \v\f20\fs18 Wing and Garlan\line \tab Lecture\tab \line \tab Handout\tab \par 
\par 
\pard\plain \qj\sb120\tx480\tx1680\tx2880\tx5520\tx7200 \f20\fs20 * marks classes that follow a holiday\par 
\pard\plain \s255\qj\sb360\tx480 \b\f20 \page References\par 
\pard\plain \s7\qj\fi-980\li980\sb120\tx980 \f20\fs20 [AG94]\tab \ldblquote Formalizing Architectural Connection,\rdblquote  R. Allen and D. Garlan, {\i Proc 16th International  Conf. on Software Engineering, }May 1994.\par 
[AS83]\tab "Concepts and Notations for Concurrent Programming," Andrews and Schneider. {\i Computing Surveys}, Vol. 15, No. 1, March 1983.\par 
[Bir89]\tab \ldblquote An Introduction to Programming with Threads,\rdblquote  Andrew Birrell. DEC/SRC TR-35, January 1989.\par 
[BGHL]\tab \ldblquote Thread Synchronization: A Formal Specification,\rdblquote  Birrell, Guttag, Horning, and Levin. Chapter 5 of {\i Systems Programming with Modula-3}, Greg Nelson (editor), Prentice-Hall 1991.\par 
\pard \s7\qj\fi-980\li980\sb120\tx980 {\v [CES]\tab "Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications," Clarke, Emerson, and Sistla. }{\i\v TOPLAS}{\v  Vol. 8, No. 2, April 1986.\par 
}\pard \s7\qj\fi-980\li980\sb120\tx980 {\v [CSP]\tab C.A.R. Hoare, }{\i\v Communicating Sequential Processes,}{\v  Prentice-Hall International, 1985.\par 
}\pard \s7\qj\fi-980\li980\sb120\tx980 [DG90]\tab \ldblquote A Formal Specification of an Oscilloscope,\rdblquote  N. Delisle and D. Garlan. {\i IEEE Software,} Sept 1990.\par 
\pard \s7\qj\fi-980\li980\sb120\tx980 [Fuzz]\tab {\i The Fuzz Manual}, J. M. Spivey, 1988.\par 
\pard \s7\qj\fi-980\li980\sb120\tx980 [GH93]\tab \ldblquote An Introduction to Larch," Guttag and Horning. Chapter 3 of {\i Larch: Languages and Tools for Formal Specification}, Springer-Verlag, 1993.\par 
[GS93]\tab {\i A Logical Approach to Discrete Math}, David Gries and Fred B. Schneider, Springer-Verlag, 1993.\par 
[HJ]\tab {\i Concrrent Systems: Formal Development in CSP}, M.G. Hinchey and S.A. Jarvis, McGraw-Hill, 1995. \par 
\pard \s7\qj\fi-980\li980\sb120\tx980 [Jen91]\tab Coloured Petri Nets: A High Level Language for System Design and Analysis,\rdblquote  K. Jensen. In {\i High-level Petri Nets: Theory and Application}
, K. Jensen and G. Rozenberg (eds.) Springer-Verlag, 1991.\par 
\pard \s7\qj\fi-980\li980\sb120\tx980 [MP92]\tab {\i The Temporal Logic of Reactive and Concurrent Systems}, Zohar Manna and Amir Pnueli,\line Springer-Verlag,1992.\par 
\pard \s7\qj\fi-980\li980\sb120\tx980 [Pet77]\tab \ldblquote Petri Nets,\rdblquote  J. L. Peterson. {\i ACM Computing Surveys,} Sept 1977.\par 
\pard \s7\qj\fi-980\li980\sb120\tx980 [PST]\tab {\i An Introduction to Formal Specification and Z}, Ben Potter, Jane Sinclair, and David Till. Prentice-Hall International, 1991.\par 
\pard \s7\qj\fi-980\li980\sb120\tx980 [SEM]\tab {\i Software Engineering Mathematics}, J.C.P. Woodcock and M. Loomes. Addison-Wesley, 1988.\par 
\pard \s7\qj\fi-980\li980\sb120\tx980 [Spi89]\tab \ldblquote An Introduction to Z and Formal Specification\rdblquote , J. M. Spivey. {\i SW Eng Journal,} January 1989.\par 
\pard \s7\qj\fi-980\li980\sb120\tx980 [ZRM]\tab {\i The Z Notation: A Reference Manual,} J. M. Spivey. Prentice-Hall International, 1989.\par 
\pard \s7\qj\fi-1260\li1260\sb120\tx980\tx1260 \page To do:\par 
\pard \s7\qj\fi-1260\li1260\sb120\tx980\tx1260 New CSP book.  Add ch readings and reference.\par 
\par 
ISumner to do:\par 
URL - did I get it right?\par 
\pard \s7\qj\fi-1260\li1260\sb120\tx980\tx1260 Put Moose icon on Models home page\par 
}