Observatorio de I+D+i UPM

Memorias de investigación
Ponencias en congresos:
Automatic Proof of Refinement among Design Patterns using the TLC
Año:2007
Áreas de investigación
  • Lenguaje de programación
Datos
Descripción
Design patterns are reuse artifacts meant to improve the quality of software designs as well as the productivity of designers. Patterns (and their relationships) are mostly described in an informal fashion which leads to ambiguity and limits tools support. This has worsened with the growing number of well-established and candidate patterns. This paper discusses how to formally specify the "solution element" of patterns and their relationships using TLA+, the formal specification language of Temporal Logic of Actions (TLA). The paper first classifies and formally defines the most common relationships between patterns. Then, it shows how to automatically proof the existence of a "refines" relationship between patterns using TLC-the TLA+ Model Checker.
Internacional
Si
Nombre congreso
6th WSEAS International Conference on Applied Computer Science (ACOS 2006)
Tipo de participación
960
Lugar del congreso
Hangzhou, China
Revisores
Si
ISBN o ISSN
978-960-8457-61-4
DOI
Fecha inicio congreso
15/04/2007
Fecha fin congreso
17/04/2007
Desde la página
Hasta la página
Título de las actas
Esta actividad pertenece a memorias de investigación
Participantes
  • Autor: Toufik Taibi (College of Information Technology, United Arab Emirates University, Al Ain, United Arab Emirates)
  • Autor: Angel Herranz Nieva (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 2022 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)