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 |