11497295
Description
Mind Map by Octavio Jose, updated more than 1 year ago
|
Created by Octavio Jose
almost 7 years ago
|
|
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
- 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
- Planeación del incremento.
- Recopilación de requerimientos.
- Especificación de estructura de caja.
- Diseño formal.
- Generación, inspección y verificación de código.
- Planeación de prueba estadística.
- Prueba de uso estadístico.
- Certificación
- Planeación del incremento.
- 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
- 21.2 ESPECIFICACIÓN FUNCIONAL
- 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.
- Caja negra.
- La caja negra especifica el comportamiento de un sistema o de una parte de un
sistema.
- La caja negra especifica el comportamiento de un sistema o de una parte de un
sistema.
- Caja de estado
- La caja de estado encapsula los datos y servicios (operaciones) de estado en una forma análoga a los
objetos.
- La caja de estado encapsula los datos y servicios (operaciones) de estado en una forma análoga a los
objetos.
- Caja clara
- Las funciones de transición que se implican mediante la caja de estado se definen en
la caja clara
- Las funciones de transición que se implican mediante la caja de estado se definen en
la caja clara
- 21.2.1 Especificación de caja negra
- 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]
- 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]
- 21.2.2 Especificación de caja de estado
- La caja de estado es “una simple generalización de una máquina de estado”
- La caja de estado es “una simple generalización de una máquina de estado”
- 21.2.3 Especificación de caja clara
- La especificación de caja clara está cercanamente alineada con el diseño procedural y con la
programación estructurada.
- La especificación de caja clara está cercanamente alineada con el diseño procedural y con la
programación estructurada.
- Caja negra.
- 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.
- 21.3 DISEÑO DE CUARTO LIMPIO
- La ingeniería del software de cuarto limpio utiliza mucho la filosofía de programación
estructurada
- 21.3.1 Refinamiento de diseño
- 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.
- 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.
- 21.3.2 Verificación de diseño
- 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.
- 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.
- 21.4 PRUEBAS DE CUARTO LIMPIO
- 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.
- 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”
- 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.
- 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
- 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.
- La confiabilidad global del sistema se proyecta y se certifica.
- Modelo de muestreo.
- 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.
- El usuario de un programa de computadora rara vez necesita entender los detalles técnicos del diseño
- 21.4.1 Pruebas de uso estadístico
- 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.
- 21.3.1 Refinamiento de diseño
- La ingeniería del software de cuarto limpio utiliza mucho la filosofía de programación
estructurada
- 21.5 CONCEPTOS DE MÉTODOS FORMALES
- Los métodos formales utilizados para desarrollar sistemas de cómputo son técnicas con base
matemática para describir las propiedades del sistema.
- 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
- 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
- Los métodos formales utilizados para desarrollar sistemas de cómputo son técnicas con base
matemática para describir las propiedades del sistema.
- 21.6 APLICACIÓN DE NOTACIÓN MATEMÁTICA7 PARA
ESPECIFICACIÓN FORMAL
- 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.
- 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
- Un lenguaje de especificación formal por lo general se compone de tres componentes primarios:
- 1) una sintaxis que define la notación específica con la que se representa la especificación,
- 2) semántica para ayudar a definir un “universo de objetos” [Win90] que se usarán para describir el
sistema
- 3) un conjunto de relaciones que definen las reglas que indican cuáles objetos satisfacen
adecuadamente la especificación.
- 1) una sintaxis que define la notación específica con la que se representa la especificación,
- 21.7.1 Lenguaje de restricción de objeto (OCL)8
- En el lenguaje está disponible todo el poder de la lógica y de la
matemática discreta.
- 21.7.2 El lenguaje de especificación Z
- 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
- 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
- En el lenguaje está disponible todo el poder de la lógica y de la
matemática discreta.
- Un lenguaje de especificación formal por lo general se compone de tres componentes primarios:
- 21.8 RESUMEN
- 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.
- 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
- Gerardo Alain Salazar Tamay
- MILLAN LUGO JOSE OCTAVIO
- MILLAN LUGO JOSE OCTAVIO
- Gerardo Alain Salazar Tamay
Media attachments
Want to create your own Mind Maps for free with GoConqr? Learn more.