CMU CS 15-675 Architectures for Software Systems Spring 1996

Formal Models for Procedure Call Systems

Garlan & Shaw Questions on Readings for Lecture 6 Due: Wed Jan 31, 1996

The papers:

Shaw and Garlan (1995): Software Architecture, Sections 6.1, 6.7.

Shaw (1985): What Can We Specify?

Spivey (1989): An Introduction to Z and Formal Specification, pp 40-45.

Abowd, Allen, and Garlan (1995): Formalizing Style to Understand Descriptions of Software Architecture.

Hints:

In the Spivey reading pay most attention to how schemas are defined and combined. The material on refinement (following page 45) can be read for additional information on how Z is used. This material should be review for students who have already taken Models of Software Systems.

In Abowd et al., the important parts are the beginning and the end. The middle contains some detailed descriptions of particular styles. We will be looking at those specific formal models in more detail later in the course, so for now just skim them. The main thing is to understand at a high level how style specifications are instances of the general framework proposed in the paper, and the arguments about why it is worth going to the trouble of producing the formalisms.

So, read pp 1-9 and pp 21-25 carefully. Read, but don't sweat about, pp 10-20. Note also that the appendix contains a summary of the notation used. This is a duplication of Section 6.7 in the text.

Questions:

1) Write a Z specification of the following system: a teacher wants to keep a register of students in her class, and to record which program each student is in. Specify:

(a) The state space for a register.

(b) An operation to enroll a new student.

(c) An operation to change the program of a student (already enrolled in the class).

(d) An operation to enquire which program a student (who must be enrolled in the class) is in.

(e) Optional: format and check your specification using the Fuzz typechecker.

Hint: start with given set [NAME] representing the names of students, and define PROGRAM ::= MSE | UNDERGRAD | INI | OTHER

Then consider using a schema of the form, adding the appropriate state invariant

__ClassRegister_____________________

| students: P NAME

| status: NAME æ|Æ PROGRAM

| ___________

| ...

|________________________________

2) What kinds of analyses and comparisons does a formal representation of style permit?

3) Briefly describe one property of a Pipe-Filter style that is not a property of Event Systems. ÿ