Stepwise Refinement Validation of Design
Patterns Formalized in TLA+ using the TLC
Model Checker
Toufik Taibi, Department of Electrical and Computer Engineering
University of Western Ontario London N6A5B9, Ontario, Canada
Ángel Herranz, Babel Group, Universidad Politécnica
de Madrid, Campus de Montegancedo s/n, Boadilla del Monte 28660, Spain
Juan José Moreno-Navarro, Babel Group, Universidad
Politécnica de Madrid & IMDEA-Software, Campus de Montegancedo s/n,
Boadilla del Monte 28660, Spain |
 |
REFEREED
ARTICLE
PDF Version |
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.
Note: Due to the typographical sophistication of this article, no HTML version is available. Please use the PDF version.
About the authors
|
|
Toufik Taibi received his PhD from Multimedia University,
Malaysia in 2003. He is currently a post-doctoral fellow at the department
of Electrical and Computer Engineering at the University
of Western Ontario, Canada. Prior to that he was Assistant Professor
at United Arab Emirates University, UAE. Dr. Taibi has more
than 16 years of combined teaching, research and software industry
experience. His research interests include formal methods as it applied
to software engineering, multi-agent systems and cooperative
distributed systems. He can be reached at ttaibi@uwo.ca. |
|
|
Ángel Herranz is an associate professor of computer science and
member of the Babel Research Group at Universidad Politécnica de
Madrid. He is a partner in Sistemas de Identificaci´on Giro, an electronic
engineering start-up. His research interests include formal
aspects of software development, assisted and automatic program
derivation and programming languages. He can be reached at aherranz@fi.upm.es. |
|
|
Juan José Moreno-Navarro received his Ph.D. degree in Computer
Science from the Technical University of Madrid in 1989. Since
1996 he is full professor at its Department of Computer Science,
where he leads the research group Babel, focused on high-quality
software development through the use of declarative technology.
Currently he is also Deputy Director of IMDEA-Software (Madrid
Research Institute for Software Technologies). His research lines
cover all the topics related to declarative technology and software
development. He can be reached at jjmoreno@fi.upm.es. |
Toufik Taibi, Ángel Herranz, Juan José Moreno-Navarro: "Stepwise Refinement Validation of Design
Patterns Formalized in TLA+ using the TLC
Model Checker", in Journal of Object Technology, vol. 8, no. 2, March-April 2009, pp. 137-161 http://www.jot.fm/issues/issue_2009_03/article3/
|