Automatic Analysis of Architectural Style
Author:Daniel Jackson
Submitted for publication.
Download the PostScript.
Abstract
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.
Keywords:
architectural style, event based systems, model checking, formal specification, Z.
Back to Nitpick Home Page