|
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. Checking that the refinement properties hold was done using TLC (the TLA+ model checker). | |
|
International
|
Si |
|
JCR
|
No |
|
Title
|
Journal of Object Technology |
|
ISBN
|
1660-1769 |
|
Impact factor JCR
|
0 |
|
Impact info
|
|
|
Volume
|
8 |
|
|
|
|
Journal number
|
2 |
|
From page
|
137 |
|
To page
|
161 |
|
Month
|
MARZO |
|
Ranking
|
|