Stepwise Refinement Validation of Design Patterns Formalized in TLA+ using the TLC Model Checker.
Toufik Taibi, Ángel Herranz, Juan José Moreno-Navarro · The Journal of Object Technology · 2009
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.Checking that the refinement properties hold was done using TLC -the TLA+ model checker.