Automatic Analysis of Architectural Style

Author:Daniel Jackson

Submitted for publication.

Download the PostScript.


A new technique for analyzing architectural styles is presented. The style is specified in NP, a relational notation similar to Z, along with properties expected to hold for all instances of the style. The specification is checked by Nitpick, a fully automatic checker for NP. Nitpick exhaustively enumerates all instances of the style-that is, all architectures that conform to the style-within given finite bounds, and reports those instances that fail to satisfy the expected properties.

The technique is applied to a specification of a family of implicit invocation styles developed originally in Z by Garlan and Notkin. The analysis exposes some potential troublespots, highlights differences between the styles, and suggests some refinements.


architectural style, event based systems, model checking, formal specification, Z.
Back to Nitpick Home Page