Stepwise Refinement Validation of Design Patterns Formalized in TLA+ using the TLC Model Checker.

Abstract

Despite being around for only a little more than a decade, design patterns have proved to be successful reuse artifacts. However, the fact that they are mostly described informally gives rise to ambiguity and hinders correct usage. This paper discusses how to formally specify the "solution element" of patterns using TLA+, the formal specification language of Temporal Logic of Actions (TLA). The focus is first on formally specifying the most abstract version of a pattern before validly doing stepwise refinements by adding more details along the way until reaching a concrete implementation.