Title:	ESPECIFICACIÓN FORMAL PARA LA VERIFICACIÓN DINÁMICA DE APLICACIONES WEB
Author(s):	Ascánder Suárez, Oswaldo Olivo
ISBN:	978–972–8924–72-0
Editors:	Flavia Maria Santoro, Pedro Isaías e José María Gutiérrez
Year:	2008
Edition:	Single
Keywords:	aplicaciones web, especificación, verificación , métodos formales, ingeniería de software
Type:	Full Paper
First Page:	233
Last Page:	240
Cover:
Full Contents:	click to dowload
Paper Abstract:	Las Aplicaciones Web constituyen una porción importante del software desarrollado en la actualidad. Entre sus ventajas, desde el punto de vista del usuario, destacan la sencillez de la interfaz, disponibilidad del programa cliente (navegador) sin necesidad de instalaciones complicadas y transparencia frente a actualizaciones. El desarrollador dispone de diversas herramientas que le asisten en el diseño e implementación del producto. Por otra parte, permanece vigente el problem del desarrollo de software : garantizar que la aplicación funciona correctamente. La notación matemática constituye una sólida alternativa para la descripción del comportamiento de programas debido a su expresividad y carencia de ambigüedad. La posibilidad de incluir aserciones en diversos lenguajes de programación invita a considerar el análisis dinámico a la hora de validar el funcionamiento de las aplicaciones. Proponemos la integración de un lenguaje de especificaciones dentro de una herramienta que asiste en el desarrollo de Aplicaciones Web, con la finalidad de efectuar verificación dinámica. El lenguaje de especificación está basado en Java. La herramienta extendida es Cohesión, que apoya al programador en el diseño e implementación de Aplicaciones Web. La verificación dinámica se realiza mediante la inclusión de aserciones (assert) de Java dentro del código de la aplicación. La utilización de Hibernate nos permite tratar las Bases de Datos (BDs) como Tipos Abstractos de Datos (TADs). Traducimos métodos no-puros sobre TADs a sus equivalentes puros gracias a la creación de nuevas instancias de la clase. De esta forma, permitimos la inclusión de operaciones sobre el almacenamiento persistente en las especificaciones. La utilización de una pista de auditoría nos permite determinar dinámicamente el estado de la BD al final de un procedimiento, a partir del estado inicial. En consecuencia, las Aplicaciones Web de mayor interés (aquellas que hacen uso de almacenamiento persistente) pueden ser verificadas. Adicionalmente, el almacenamiento de claves de sesión en la pista de auditoría nos permite resolver el problema de la concurrencia, ya que podemos identificar cuándo y quién ha manipulado la BD.
	Go Back