Analyzing and refining an architectural style

Architectural styles have been introduced in [1] in order to classify and analyze software architectures. In that paper, Z was used as a notation to specify and study architectural styles, however some problems remained open concerning specification and analysis of their behavioral properties. We use a new operational semantics to describe and analyze an architectural style of distributed systems. We introduce three refinements of a “Message Router” style, useful to describe distributed applications like e-mail or news systems; we also formalize and prove some properties of the style and, henceforth, of derived software architectures