CAP 21.MODELADO Y VERIFICACIÓN FORMAL

En este capítulo se exploran los métodos de modelado y verificación formales y se examina su impacto potencial sobre la ingeniería del software en los años por venir.
21.1ESTRATEGIA DE CUARTO LIMPIO
1. La ingeniería del software de cuarto limpio usa una versión especializada del modelo de software incremental que se introdujo en el capítulo 2
  1. Planeación del incremento.
  2. Recopilación de requerimientos.
  3. Especificación de estructura de caja.
  4. Diseño formal.
  5. Generación, inspección y verificación de código.
  6. Planeación de prueba estadística.
  7. Prueba de uso estadístico.
  8. Certificación
21.2 ESPECIFICACIÓN FUNCIONAL
1. El enfoque de modelado en la ingeniería del software de cuarto limpio usa un método llamado especificación de estructura de caja. Una “caja” encapsula el sistema (o algún aspecto del mismo) en algún nivel de detalle.
  1. Caja negra.
    1. La caja negra especifica el comportamiento de un sistema o de una parte de un sistema.
  2. Caja de estado
    1. La caja de estado encapsula los datos y servicios (operaciones) de estado en una forma análoga a los objetos.
  3. Caja clara
    1. Las funciones de transición que se implican mediante la caja de estado se definen en la caja clara
  4. 21.2.1 Especificación de caja negra
    1. Una especificación de caja negra describe una abstracción, estímulos y respuesta, usando la notación que se muestra en la figura 21.3 [Mil88]
  5. 21.2.2 Especificación de caja de estado
    1. La caja de estado es “una simple generalización de una máquina de estado”
  6. 21.2.3 Especificación de caja clara
    1. La especificación de caja clara está cercanamente alineada con el diseño procedural y con la programación estructurada.
21.3 DISEÑO DE CUARTO LIMPIO
1. La ingeniería del software de cuarto limpio utiliza mucho la filosofía de programación estructurada
  1. 21.3.1 Refinamiento de diseño
    1. Cada especificación de caja clara representa el diseño de un procedimiento (subfunción) requerido para lograr una transición de caja de estado. Dentro de la caja clara se usan constructos de programación estructurada y refinamiento por pasos para representar detalles procedurales.
  2. 21.3.2 Verificación de diseño
    1. Debe observar que el uso de los constructos de programación estructurada restringen el número de pruebas de exactitud que deben realizarse. Una sola condición se verifica para secuencias; dos condiciones se prueban para if-then-elseo y tres condiciones se verifican para ciclo.
  3. 21.4 PRUEBAS DE CUARTO LIMPIO
    1. La meta de la prueba de cuarto limpio es validar los requerimientos de software al demostrar que una muestra estadística de casos de uso (capítulo 5) se ejecuta exitosamente.
      1. 21.4.1 Pruebas de uso estadístico
        El usuario de un programa de computadora rara vez necesita entender los detalles técnicos del diseño
        La prueba de uso estadístico “equivale a examinar el software de la forma en la que los usuarios pretenden usarlo”
        21.4.2 Certificación
        Las técnicas de verificación y prueba analizadas anteriormente en este capítulo conducen a componentes de software (e incrementos completos) que pueden certificarse.
        Modelo de muestreo.
        La prueba de software ejecuta m casos de prueba aleatorios y se certifica si no ocurren fallos o un número específico de ellos.
        Modelo de componente.
        Se certifica un sistema compuesto de n componentes. El modelo de componentes permite al analista determinar la probabilidad de que el componente i fallará antes de su conclusión
        Modelo de certificación.
        La confiabilidad global del sistema se proyecta y se certifica.
21.5 CONCEPTOS DE MÉTODOS FORMALES
1. Los métodos formales utilizados para desarrollar sistemas de cómputo son técnicas con base matemática para describir las propiedades del sistema.
  1. Tales métodos formales proporcionan marcos conceptuales dentro de los cuales las personas pueden especificar, desarrollar y verificar los sistemas en forma sistemática más que ad hoc
21.6 APLICACIÓN DE NOTACIÓN MATEMÁTICA7 PARA ESPECIFICACIÓN FORMAL
1. un importante componente del sistema operativo de una computadora mantiene los archivos que crearon los usuarios. El manipulador de bloques mantiene un reservorio de bloques sin utilizar y también seguirá la pista a los bloques que estén en uso en el momento. Cuando los bloques se liberan de un archivo borrado, por lo general se agregan a una fila de bloques que esperan para agregarse al reservorio de bloques no utilizados.
21.7 LENGUAJES DE ESPECIFICACIÓN FORMAL
1. Un lenguaje de especificación formal por lo general se compone de tres componentes primarios:
  1. 1) una sintaxis que define la notación específica con la que se representa la especificación,
  2. 2) semántica para ayudar a definir un “universo de objetos” [Win90] que se usarán para describir el sistema
  3. 3) un conjunto de relaciones que definen las reglas que indican cuáles objetos satisfacen adecuadamente la especificación.
2. 21.7.1 Lenguaje de restricción de objeto (OCL)8
  1. En el lenguaje está disponible todo el poder de la lógica y de la matemática discreta.
  2. 21.7.2 El lenguaje de especificación Z
    1. Z es un lenguaje de especificación que se usa ampliamente dentro de la comunidad de métodos formales. El lenguaje Z se aplica a conjuntos escritos, relaciones y funciones dentro del contexto de la lógica de predicados de primer orden para construir esquemas, un medio para estructurar la especificación formal
21.8 RESUMEN
1. La ingeniería del software de cuarto limpio es un enfoque formal del desarrollo de software que puede conducir a software con una calidad notablemente alta. Usa la especificación de estructura de cajas para el análisis y el modelado del diseño, y enfatiza la verificación de la exactitud, en lugar de las pruebas, como el mecanismo primario para encontrar y remover errores.
INTEGRANTES
1. Gerardo Alain Salazar Tamay
2. MILLAN LUGO JOSE OCTAVIO
3. MILLAN LUGO JOSE OCTAVIO

Anexos de mídia

S (binary/octet-stream)

Próximo

CAP 21.MODELADO Y VERIFICACIÓN FORMAL

Descrição

Resumo de Recurso

Anexos de mídia

Semelhante

	Criado por Octavio Jose aproximadamente 7 anos atrás