Formalizing Design Patterns

Abstract

Design patterns facilitate reuse of good design practices. They are typically given by using conventional notations that lack well-defined semantics and, therefore reasoning about their behaviors requires formalization. Even when formalized, conventional communication abstractions may lead to too laborious formalizations when addressing the temporal behavior of a pattern as a whole instead of behaviors local to its components. We show that rigorous reasoning can be eased by formalizing temporal behaviors of patterns in terms of high-level abstractions of communication, and that by using property-preserving refinements, specifications can be naturally composed by using patterns as building blocks.