CMU CS 15-675 Architectures for Software Systems Spring 1997

Formal Models for Procedure Call Systems

The papers:

[SG96]: Sections 6.1, 6.7.

[Sha85]: What Can We Specify?

[AAG93]: Formalizing Style to Understand Descriptions of Software Architecture.

Hints:

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 is how at a high level 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:

   The state space for a register.

   An operation to enroll a new student.

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

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

   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 -|- (right arrow) 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.

Email the Current Maintainer

Modified: 02/26/97