Observatorio de I+D+i UPM

Memorias de investigación
Artículos en revistas:
Stepwise Refinement Validation of Design Patterns Formalized in TLA+ Using the TLC Model Checker
Año:2009
Áreas de investigación
  • Lenguaje de programación
Datos
Descripción
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).
Internacional
Si
JCR del ISI
No
Título de la revista
Journal of Object Technology
ISSN
1660-1769
Factor de impacto JCR
0
Información de impacto
Volumen
8
DOI
Número de revista
2
Desde la página
137
Hasta la página
161
Mes
MARZO
Ranking
Esta actividad pertenece a memorias de investigación
Participantes
  • 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)
Grupos de investigación, Departamentos, Centros e Institutos de I+D+i relacionados
  • 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 2021 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)