Programa de la presentación
El problema
Técnicas relacionadas
Solución aportada
Estudio práctico y resultados
Conclusiones y trabajo futuro
Componentes software
Componente software (según Szyperski)
Unidad de composición con interfaces especificadas contractualmente y dependencias contextuales explícitas
Entendido como unidad de despliegue independiente
Frecuentemente…
Se piensa en ActiveX, CORBA o similares
Se equipara “componente” a “objeto empaquetado”
Beneficios esperados: ahorro de tiempo, mayor fiabilidad
Problemas del uso de componentes en la práctica – I
Dados ciertos componentes correctos, ¿será correcto el sistema resultante?
Errores derivados de la propia combinación
“Comportamiento emergente”
Violación de los requisitos de funcionamiento de algún componente
Recursos para verificar la conexión entre componentes
Frecuentemente, sólo verificación de signaturas
En algunos casos, mecanismos de tiempo de ejecución
Problemas del uso de componentes en la práctica – II
Verificación de signaturas
Habitualmente, se limita al tipo y número de los parámetros
OK
Especificación
void f(int x, int y)
f(3, 5);
Uso
Especificación
“Que x sea siempre mayor que y”
void f(int x, int y)
f(3, 5);
Uso
¿OK?
void f(int x, int y)
{
…
assert(x <= y);
…
}
Falta de mecanismos de verificación – I
Verificación de signaturas
Muy limitada
Especificación textual
Sujeta a ambigüedades
No hay garantías de que se aplique
No se puede automatizar la verificación
Código de salvaguardia
Sólo funciona en tiempo de ejecución
Puede haber problemas que no se detecten
Semántica limitada (ej.: “No utilizar en sistemas de tiempo real”)
Falta de mecanismos de verificación – II
Muchos defectos se podrían prever
Conocimiento a priori
Se pueden conocer propiedades indecidibles
Habitualmente se pierde
Necesidad de un mecanismo que permita aprovechar el conocimiento a priori
Verificación basada en ese conocimiento
Falta de mecanismos de verificación – III
Se necesitaría un sistema de verificación:
Que pudiera utilizarse en tiempo de construcción del software (no de ejecución)
Automático (la especificación acompañaría al componente y se tendría en cuenta de forma inmediata)
Susceptible de ser utilizado con facilidad en entornos de producción
Flexible (un método general aplicable a diversos aspectos y ámbitos del desarrollo, con una semántica abierta)
Tesis – I
Es posible verificar, de manera estática, automática y asequible que, hasta donde nos es posible asegurar con el conocimiento disponible, al combinar ciertos componentes software no se han violado las condiciones de funcionamiento correcto de ninguno de ellos.
Tesis – II
Verificación
Estática – sin poner el sistema en funcionamiento (detección temprana de los defectos, aprovechamiento del conocimiento disponible)
Automática – menor coste, mayor frecuencia, menor ambigüedad
Asequible
Técnicas conocidas y viables
Comprendido y aplicado con facilidad por el personal típico
General, flexible (retorno de inversión)
Esto exige un modelo sencillo
Método de trabajo
Proponer un modelo de verificación que cumpla los objetivos marcados
Probar la viabilidad técnica de las herramientas desarrollando prototipos con medios limitados
Probar la aplicabilidad de ese modelo a problemas prácticos diferentes
Métodos formales
Especificación formal de la interfaz
SDL, Estelle, Lotos / Z, VDM, B…
Especificación
Refinamiento
Prueba de adecuación
Problemas:
Asequibilidad (o percepción sobre ella). Wing, Bowen & Hinchey, Pressman, Parnas, Meyer, Szyperski…
Componentes
Conocimiento
Automatización y herramientas
Flexibilidad
Análisis estático e interpretación abstracta
Evaluación de código fuente con algoritmos
Semántica menos precisa pero computable
Valores abstractos de variables
Convergencia
Cousot & Cousot, PAG, PolySpace…
Problemas
Componentes
Asequibilidad
Flexibilidad (alg. específicos, código fuente)
Especificación semántica
Técnicas para describir formalmente el comportamiento de un lenguaje de programación
Posibilidad de trasladarlas al ámbito de componentes
Problemas
Legibilidad
Modularidad (hay trabajos prometedores)
Falta de madurez e implementaciones
Especificación de procesos
CSP (CCS, ACP, otros), ?-cálculo, ?L-cálculo, derivados (Piccola, Pict, etc.)
Problemas
Orientadas a procesos (CSP y similares)
Notaciones formales (asequibilidad)
Flexibilidad
Bajo nivel
Orientados a concurrencia (Pict)
Orientados a composición y no tanto a verificación (Piccola)
Contratos
Varios enfoques
Unilateral (Meyer)
Bilateral (Wirfs-Brock, Reenskaug)
Contratos de reutilización (Vrije Universiteit Brussels)
Lenguaje Contract
Problemas
Meyer: estado concreto, verificaciones ejecutables
Wirfs-Brock, Reenskaug: centrados en análisis/diseño
Contratos de reutilización: poca flexibilidad
Lenguaje Contract: no orientado a verificación
Estilos arquitectónicos
Incoherencias entre estilos arquitectónicos (Carnegie Mellon)
ADLs (Wright, Aesop, Darwin, Rapide, UniCon…)
Problemas
Flexibilidad
Automatización
Análisis estático (limitado)
Asequibilidad (WRIGHT: notaciones basadas en CSP)
Página siguiente |