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

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