CMU CS 15-675 Architectures for Software Systems Spring 1997

Formal Models for Processes

The papers:

[AG97]: [AG97]: Allen and Garlan. Formal Modeling and Analysis of the HLA RTI.

[SG96]: [SG96]: Shaw and Garlan. Software Architecture. Section 8.3.

[All97]: [All97]: [All97]: Allen. A Formal Approach to Software Architecture, Chapter 3.

Hints:

The main paper is the case study on the High Level Architecture (HLA) for distributed simulations. This is the paper on which you should focus your efforts. The notation used in that paper is called Wright. The second two readings contain details about that notation. Section 8.3 from the text is short and direct, but uses an earlier version of the language. The excerpt from Allen’s thesis provides a more thorough and up-to-date summary of the notation. But both of these can be viewed as companion readings for the first paper: use them primarily as overview and reference.

Note that the questions are due the class after the lecture. This will allow you learn more about Wright in the lecture before attempting to create some specifications of your own.

Questions:

1. Consider an architectural connector that allows a single student to turn an assignment (electronically). The Handin connector will have two roles: a Student role and a Teacher role. Assume that an assignment can be redone if it is given a failing grade on the first handin. Produce a Wright description for this connector. Indicate any design issues that are raised by the connector, and how you resolved them. (For fun, you might want to see how you would turn this into a connector that can work with an arbitrary, fixed number of students.)

2. Produce a Wright specification for a "merge" filter, similar to the "split" filter in Section 8.3 of the text. Again explain what issues are raised by the specification and how you resolved them.

Email the Current Maintainer

Modified: 06/02/97