Metodologías de análisis y diseño OCL (Object Constraint Language) Catalysis Problemas Orientados al modelado, no a la verificación estática Automatización
Plataformas de componentes OSF/DCE (IDL) COM, CORBA, JavaBeans “Estándares de cableado” (Szyperski) Ya funcionan (éxito comercial) Problemas Orientados a la composición, no a la verificación
Resumen de tendencias analizadas
El modelo de componentes Itacio Un modelo de componentes que responda a los requisitos de la tesis Primera consideración: definición abierta de “componente” Uso del término distinto al habitual Problema de nomenclatura, pero… difícil de evitar ¿Por qué Itacio? “Enterré en precioso mármol para la mansión eterna el tierno cuerpo de Itacio”
Componente – I Entidad que consta de una frontera y un conjunto de expresiones restrictivas Frontera: consta de puntos de conexión Fuentes Sumideros Expresiones restrictivas Requisitos (para los sumideros) Garantías (sobre las fuentes)
Componente – II Sumidero1 Sumidero2 Sumidero3 Fuente1 Fuente2 (Gp:) Signaturas – Sumidero1(int) – Sumidero2(int, char) – Sumidero3(char) Código
(Gp:) Requisitos – Sumidero1 debe ser menor que Sumidero2 + Sumidero3 Garantías – El valor de Fuente1 siempre estará entre el de Sumidero2 y Sumidero3 (Gp:) Signaturas – Sumidero1(int) – Sumidero2(int, char) – Sumidero3(char) Código
Sistema – I Grafo finito Nodos: componentes Arcos: pares fuente/sumidero Predicados auxiliares Corrección topológica de un sistema No hay puntos de conexión aislados No hay arcos repetidos
Sistema – II s1 válido ? s1 positivo s1 s2 f1 positivo ? s1 en [1..5] y s2 positivo s1 s2 s1 s2 f1 f1 es 5 f1 f1 está en [10..20] f1 …… ? OK ¿válido?
Expresiones restrictivas Requisitos y garantías: lógica de primer orden Cláusula Horn (CLP) Programación lógica Gran flexibilidad para representar conocimiento Ampliamente conocida (asequible) Automatizable (procesos de inferencia definidos) Herramientas disponibles y estables CLP: Gran potencia y eficiencia
Generación de la base de conocimientos – I Recopilar las expresiones restrictivas de los componentes del sistema Modificarlas de modo que quede implícita la información sobre topología De este modo, el proceso de inferencia se remonta a los componentes implicados
Generación de la base de conocimientos – II s1 válido ? s1 positivo s1 s2 f1 positivo ? s1 en [1..5] y s2 positivo f1 f2 s1 s2 f1 f1 es 5 f1 f1 está en [10..20] f1 …… A B C (Gp:) es 5 (Gp:) A (Gp:) está en [10..20] (Gp:) B
(Gp:) C (Gp:) es positivo si (Gp:) A (Gp:) en [1..5]^ (Gp:) positivo (Gp:) B
(Gp:) C (Gp:) es válido si (Gp:) C (Gp:) positivo
Proceso de verificación Proceso de inferencia del motor CLP Hipótesis del Mundo Cerrado (CWA) Enfoque exigente: si no se satisface explícitamente un requisito, se da por supuesto que se viola El proceso de inferencia puede señalar qué requisito no se cumple y por qué Con un buen diseño de los predicados, el sistema puede ofrecer explicaciones El sistema y su diagnóstico pueden representarse gráficamente
Relación con los objetivos Sistema de verificación Como proceso de inferencia en lógica de primer orden Verificación estática Verificación automática Modelo asequible Gran simplicidad del modelo (mínimo de conceptos) Simplicidad de la implementación (CLP) Verificación basada en el conocimiento disponible Aprovechamiento del conocimiento Gran flexibilidad y potencial de aplicación
Prototipos desarrollados Itacio-SEDA Basado en herramienta gráfica propietaria Motor de inferencia: ECLiPSe Itacio-XJ Datos: ficheros de texto Representación: Internet Explorer / VML Motor de inferencia: ECLiPSe Itacio-XDB Datos: base de datos ODBC Representación: Internet Explorer / VML Motor de inferencia: ECLiPSe
Prototipo Itacio-SEDA
Prototipo Itacio-XJ
Prototipo Itacio-XDB
Ejemplos: microcomponentes – I Representar elementos básicos de un lenguaje (operadores, funciones, etc.) Rudimentario sistema de generación de código (Gp:) Dividir (Gp:) op1 (Gp:) op2 (Gp:) Leer valor (Gp:) res (Gp:) Leer valor (Gp:) res (Gp:) res (Gp:) Imprimir valor (Gp:) val
(Gp:) Dividir (Gp:) op1 (Gp:) op2 (Gp:) Leer valor (Gp:) res (Gp:) Leer valor (Gp:) res (Gp:) res (Gp:) Imprimir valor (Gp:) val
(Gp:) #include void main(void) { double val1; scanf(“%lf”, &val1); double val2; scanf(“%lf”, &val2); double res=val1/val2; printf(“%lf”, res); }
(Gp:) Denominador puede ser 0
Ejemplos: microcomponentes – II Dificultades: generación de código (no era objeto de la tesis) (Gp:) Dividir (Gp:) op1 (Gp:) op2 (Gp:) Leer valor (Gp:) res (Gp:) Leer valor (Gp:) res (Gp:) res (Gp:) Imprimir valor (Gp:) val (Gp:) valido(op2):- not igual_que(op2, 0). … …
Según Carine Lucas Contrato de reutilización: conjunto de participantes con nombre, cláusula de relación e interfaz. Cláusula de relación: indicación de que un participante “conoce a” otro. Interfaz: conjunto de descripciones de operaciones (nombre y operaciones invocadas por esta). Verificaciones de consistencia (no invocar operaciones inexistentes, no eliminar operaciones en uso…) Modificaciones a contratos Modeladas como operadores (8 combinaciones) Lucas propone reglas para operadores aplicables Si se modela un sistema como contratos, con este modelo se puede verificar la evolución (usando las reglas establecidas) Ejemplos: Contratos de reutilización – I
Modelando contratos en Itacio El contrato es un componente Cada modificación es otro componente La conexión entre contratos y sucesivas modificaciones modela la evolución del sistema Los requisitos y garantías permiten validar las operaciones realizadas Ejemplos: Contratos de reutilización – II
Type=smplDrive Sources=res BEGIN_RESTRICTIONS isContract($res$). participant($res$, smplDriver). participant($res$, smplCar). acqRelationship($res$, smplDriver, myCar, smplCar). operation($res$, smplDriver, go). operation($res$, smplDriver, stop). … operationInvocation($res$, smplDriver, go, myCar, startEngine). operationInvocation($res$, smplDriver, go, myCar, pushGasPedal). … END_RESTRICTIONS
Ejemplos: Contratos de reutilización – III
Ejemplos: Contratos de reutilización – IV
Ejemplos: Diagnóstico remoto de equipos – I
Ejemplos: Diagnóstico remoto de equipos – II Las expresiones restrictivas realizan comprobaciones reales en el equipo cliente (enlazando CLP con DLLs)
Ejemplos: WaveX – I Sistema de procesamiento de sonido en tiempo real Basado en componentes (efectos, transformaciones) Combinaciones no válidas (imposible verificación meramente local) Necesidad de sistema de ayuda al usuario
Ejemplos: WaveX – II
Ejemplos: WaveX – III
Ejemplos: Modelo de Hamlet et al Un modelo de fiabilidad para componentes software Cada componente tiene asociada una hoja de transformación que indica cómo transforma los dominios de entrada en los de salida Cada componente tiene también una tasa de fallos asociada a cada combinación de subdominios Expresando esta información como expresiones restrictivas, se puede reflejar este modelo en Itacio
Ejemplos: Compatibilidad entre protocolos – I Verificaciones temporales (ordenación de llamadas) Los contratos de reutilización no lo reflejan Modelo de Yellin y Strom Especificar protocolos indicando las transiciones posibles (es decir, el orden de invocación admitido en cada componente para sus operaciones) Algoritmo para verificar la compatibilidad de los protocolos de dos componentes ¿Susceptible de ser modelado en Itacio?
Ejemplos: Compatibilidad entre protocolos – II ys_collaboration($file$). ys_states($file$, initFile, [], [createdFileObj, openingFile, openFile,readingFile, endOfFile, notReadingFile]). ys_sent_message($file$, openFileError). ys_sent_message($file$, openFileOk). … ys_received_message($file$, fileConstructor). ys_received_message($file$, fileDestructor). … ys_transition($file$, initFile, +, fileConstructor, createdFileObj). ys_transition($file$, createdFileObj, +, fileDestructor, initFile). …
Ejemplo: Compatibilidad entre protocolos – III ¿Son compatibles componentes con estos protocolos?
Ejemplo: Compatibilidad entre protocolos – IV
Conclusiones Basándose en: Interpretación de los resultados obtenidos Análisis del estado del arte Escrutinio público Se concluye que: 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.
Aportaciones Tecnología de componentes software Estudio específico de alternativas Definición abierta de componente Gestión del conocimiento aplicada Modelo de componente que permite incorporar conocimiento Esquema de generación de la BC para inferencias Ingeniería del software Método de modelado de componentes para verificación y con las restricciones descritas (gran flexibilidad y generalidad) Ejemplos de aplicación de modelo de componentes a campos diversos Sistema de verificación plenamente viable en la práctica Diversos prototipos
Trabajo futuro – I Mejoras Gestión del conocimiento Corrección de las especificaciones Razonamiento aproximado / probabilístico Relajación del criterio de corrección topológica Relación con la Ingeniería del Software Herramientas de producción (no prototipos) Integración con procesos de desarrollo Nuevos campos de aplicación del modelo Ingeniería inversa para búsqueda de defectos Búsqueda de componentes Anticipación y ayuda al diseño Relación entre expresiones restrictivas y código fuente
Trabajo futuro – II Relación con técnicas formales Especificación de la semántica del modelo mediante semántica monádica reutilizable Modelado de los componentes mediante semántica modular Creación de lenguaje independiente y extensible de propósito específico Adaptación de una técnica de especificación semántica al trabajo con componentes
| Página siguiente |