Observatorio de I+D+i UPM

Memorias de investigación
Research Publications in journals:
Stepwise Refinement Validation of Design Patterns Formalized in TLA+ Using the TLC Model Checker
Year:2009
Research Areas
  • Programming language
Information
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
Participants
  • Autor: Toufik Taibi (Department of Electrical and Computer Engineering at the University of Western Ontario, Canada.)
  • Autor: Angel Herranz Nieva (UPM)
  • Autor: Juan Jose Moreno Navarro (UPM)
Research Group, Departaments and Institutes related
  • Creador: Grupo de Investigación: BABEL: Desarrollo de Software Fiable y de Alta Calidad a partir de Tecnología Declarativa
  • Departamento: Lenguajes y Sistemas Informáticos e Ingeniería de Software
S2i 2019 Observatorio de investigación @ UPM con la colaboración del Consejo Social UPM
Cofinanciación del MINECO en el marco del Programa INNCIDE 2011 (OTR-2011-0236)
Cofinanciación del MINECO en el marco del Programa INNPACTO (IPT-020000-2010-22)