Automatic Analysis of Architectural Style
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