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

By: Toufik Taibi, Angel Herranz, Juan Jose Moreno-Navarro

Abstract

The structural aspect of patterns is represented by sub-classes participating in the pattern and associations between them. Classes are represented as sets of instances (objects), each of which is represented by an identity taken from an infinite set of object identities. As such we use the terms object and object identity interchangeably. Associations are represented as mathematical relations between objects.

Cite as:

Toufik Taibi, Angel Herranz, Juan Jose Moreno-Navarro, “Stepwise Refinement Validation of Design Patterns Formalized in TLA+ using the TLC Model Checker”, Journal of Object Technology, Volume 8, no. 2 (March 2009), pp. 137-161, doi:10.5381/jot.2009.8.2.a3.