Course Information
Garlan & Wing Handout 1 August 28, 1995
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 describe abstract formal models for certain classes of systems. Further, you should be able to reason formally about the elementary properties of modeled systems.
Version 1.2 of 8/15/95
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.
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
URL: http://www.cs.cmu.edu/afs/cs/academic/class/15671-f95/www/
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.
Communication. We have set up four mechanisms for out-of-class interaction.
1. The Moose Lounge: This is a virtual lounge for the MSE program. It is a "place" 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.
2. The Course Bulletin Board. We will use cmu.cs.class.cs671 to post questions/answers 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.
3. Office Hours: Each of the instructors and the TA has weekly office hours. These are listed on the previous page
4. Email: We welcome email about the course at any time.
Readings. Most lectures will have a reading assignment that we expect you to complete before you come to class. Many of the reading assignments will be drawn from the two required textbooks for the course: Software Engineering Mathematics, by Woodcock and Loomes (SEM) and Concrrent Systems: Formal Development in CSP, by M.G. Hinchey and S.A. Jarvis [HJ]. Some readings are in the form of handouts to supplement some lectures; other additional readings are technical papers. These will all be distributed as needed throughout the course.
Homeworks and Lab Exercises. The course is organized 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 intended 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.
Homeworks will be graded on a pass/fail basis. 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 the class following the one on which it is handed back.
Extra copies of handout materials. Extra copies of lecture slides, handouts, homework assignments, etc. will be available from Cary Lund, WeH 8106.
Exams. There will be a (take-home) mid-term (handed out October 11, due October 13) and a (in-class) final examination.
Grading. The course grade will be determined as a combination of four factors: homework exercises (50%), midterm exam (15%) final exam (25%), instructors' judgment (10%).
1 M 8/28 Introduction Course intro; What's a model?
2 F 9/1 Foundations Logic [SEM 1-4] HW 1
3 *W 9/6 Sets, Relations, Functions [SEM 5-6.3,7.1-7.3] HW 2
4 M 9/11 Proof Techniques []
5 W 9/13 Sequences & Induction [Handout 2,3,SEM 8] HW 3
6 M 9/18 State Machines Basic concepts []
7 W 9/20 Variations [Handout 4] HW 4
8 M 9/25 Invariants [Handout 5]
9 W 9/27 Z Introduction to Z [Handout 6,Spi89] HW 5
10 M 10/2 Reasoning about Z Specs [SEM 6.4,7.4]
11 W 10/4 Examples [Handout 7,DG90] HW 6
12 M 10/9 Abstraction State Machines []
13 W 10/11 Abstraction in Z [Handouts 8-11] HW 7
Midterm out
14 *W 10/18 Larch Algebras [SEM 11]
15 M 10/23 Interfaces [GH93]
16 W 10/25 Concurrency Introduction to Concurrency [AS83] HW 8
17 M 10/30 Composing State Machines [Handout 12,BGHL,Bir89]
18 W 11/1 CSP Basic CSP [Handout 13,
HJ 1,2.1-9] HW 9
19 M 11/6 Reasoning with CSP [HJ 3.1-3,6]
20 W 11/8 Nondeterminism [HJ 2.10,3.4-6] HW 10
21 M 11/13 Applications and Extensions [HJ 7, AG94]
22 W 11/15 Temporal Logic Linear Temporal Logic [MP92] HW 11
23 M 11/20 Computational Tree Logic []
24 *M 11/27 Petri Nets Introduction to Petri Nets [Pet77] HW 12
25 W 11/29 Reasoning about Petri Nets [Jen91]
26 M 12/4 Intentionally left blank HW 13
27 W 12/6 Review for final
* marks classes that follow a holiday
[AS83] "Concepts and Notations for Concurrent Programming," Andrews and Schneider. Computing Surveys, Vol. 15, No. 1, March 1983.
[Bir89] "An Introduction to Programming with Threads," Andrew Birrell. DEC/SRC TR-35, January 1989.
[BGHL] "Thread Synchronization: A Formal Specification," Birrell, Guttag, Horning, and Levin. Chapter 5 of Systems Programming with Modula-3, Greg Nelson (editor), Prentice-Hall 1991.
[DG90] "A Formal Specification of an Oscilloscope," N. Delisle and D. Garlan. IEEE Software, Sept 1990. [Fuzz] The Fuzz Manual, J. M. Spivey, 1988.
[GH93] "An Introduction to Larch," Guttag and Horning. Chapter 3 of Larch: Languages and Tools for Formal Specification, Springer-Verlag, 1993.
[GS93] A Logical Approach to Discrete Math, David Gries and Fred B. Schneider, Springer-Verlag, 1993.
[HJ] Concurrent Systems: Formal Development in CSP, M.G. Hinchey and S.A. Jarvis, McGraw-Hill, 1995.
[Jen91] Coloured Petri Nets: A High Level Language for System Design and Analysis," K. Jensen. In High-level Petri Nets: Theory and Application, K. Jensen and G. Rozenberg (eds.) Springer-Verlag, 1991.
[MP92] The Temporal Logic of Reactive and Concurrent Systems, Zohar
Manna and Amir Pnueli,
Springer-Verlag,1992.
[Pet77] "Petri Nets," J. L. Peterson. ACM Computing Surveys, Sept 1977.
[PST] An Introduction to Formal Specification and Z, Ben Potter, Jane Sinclair, and David Till. Prentice-Hall International, 1991.
[SEM] Software Engineering Mathematics, J.C.P. Woodcock and M. Loomes. Addison-Wesley, 1988.
[Spi89] "An Introduction to Z and Formal Specification", J. M. Spivey. SW Eng Journal, January 1989.
[ZRM] The Z Notation: A Reference Manual, J. M. Spivey. Prentice-Hall International, 1989.