CMU CS 15-675 Architectures for Software Systems Spring 1998

F2: Formal Models for Procedure Call Systems

with answers

Garlan & Kazman Questions on Readings for Lecture 11 Due: Mon Feb 23, 1998

The papers:

[SG96]: Sections 6.1, 6.7.

[Spi89]: An Introduction to Z and Formal Specification

[AAG93]: Formalizing Style to Understand Descriptions of Software Architecture (Read sections 1-3, 6-7; skim sections 4-5.)

Hints:

These readings are about using the Z specification language for formalizing architectural models. The idea here is not to be an expert on Z, but rather to have a reading knowledge of what others have written.

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.

The Spivey paper provides a quick introduction to Z. You need only read the first couple parts -- up through building a robust specification. Ignore the parts of the paper on refinement.

Questions:

Write a Z specification of the following system: a college accounting system is to keep an on-line record of student registrations, and to record which program each student is in. Part of this system will be modeled by a set of objects representing each class. Each of these objects keeps track of the students in the class and the degree program that each is associated with.

Specify:

(a) The state space for a class register.

(b) An operation to add a new student to that class

(c) An operation to change the degree program of a student (where the student must 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 ::= GRADUATE | MSE | UNDERGRAD | INI | OTHER

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

 

__ClassRegister_____________________

|class: N

| students: P NAME

| status: NAME ¾|® PROGRAM

| ___________

| ...

|________________________________

Answer: see separate handout

 


Back

Heather L. Marko