CMU CS 15-671

Models of Software Systems

David Garlan

Fall 1997

Course Information

The Bare Essentials

Class Meetings:

Monday and Wednesdays, 10:30-11:50, in DH1211

Course Materials and Administration

Course mechanics: Assignments, grading policy, and so on

Announcements will be made on the class bulletin board: cmu.cs.class.cs671

On-line course materials, formatted for web browsing will be made accessible from the syllabus below as they are available.

Schedule and Syllabus

Textbooks and Readings:

The main text for the course is Potter, Sinclair and Till's An Introduction to Formal Specification and Z (Second Edition) [PST]. The supplemental text is Woodcock and Davies' Using Z: Specification, Refinement and Proof [WD97]. In addition, we will read selected papers from other sources. Each lecture (after the first, of course) has hints and questions to guide your reading. Click the button in the Q/A column to see the hints and questions.

Citations in Bold refer to PST. You are expected to read associated introductory material; for example, an assignment of Ch 4.2.1 includes the paragraphs between the Section heading for 4.2 and the actual beginning of 4.2.1. Supplemental readings will be distributed during the semester.

Lectures and Homework Assignments:

# Date Topic Subtopic Reading Homework

1 M 8/25 Introduction Course info; what is a model?

2 W 8/27 Foundations Logic [Handout 1, 1-2]

3 *W 9/3 Sets, Relations, Functions [4.1-3,5] HW 1

4 M 9/8 Cancelled [Handout 2, 9.5-6] HW 2

5 W 9/10 Proof Techniques [Handout 3,4]

6 M 9/15 State Machines Basic concepts [Handout 5] HW 3

7 W 9/17 Variations [Handout 6]

8 M 9/22 Reasoning [Handout 7] HW 4

9 W 9/24 Statecharts [Ha87]

10 M 9/29 Z Introduction to Z [4.4-6,130-155] HW 5

11 W 10/1 Reasoning about Z Specs [7-8(skim),6.5.8,9.1-4]

12 M 10/6 Examples [Handout 8, Handout 8a,DG90] HW 6, Lab 1

13 W 10/8 Abstraction in Z [Handout 9, Handout 10, Handout 11, 10]

Midterm out

14 *W 10/15 Larch Algebras [SEM, Ch 11] HW 7

15 M 10/20 Interfaces [GH93] HW 8

16 W 10/22 Concurrency Introduction to Concurrency [AS83, Handout 12, Handout 13]

17 M 10/27 Petri Nets Introduction to Petri Nets [Pet77] HW 9

18 W 10/29 Reasoning about Petri Nets [Jen91]

19 M 11/3 CSP Introduction to CSP [] HW 10

20 W 11/5 Reasoning with CSP []

21 M 11/10 Nondeterminism [] HW 11

22 W 11/12 Case Study [AGI97, Handout13]

23 M 11/17 Temporal Logic Linear Temporal Logic [] HW 12

24 W 11/19 Other Temporal Logic []

25 M 11/24 Temporal Logic of Actions [Lam 90] HW 13

26 *M 12/1 Applications [12] HW 14

27 W 12/3 Review for Final

This page belongs to the course CMU CS 15-671, Models of Software Systems, offered in the Master of Software Engineering program of the Computer Science Department at Carnegie Mellon University. For assistance or information about these web pages (during the fall 1997 semester), email the teaching associate.