Desarrollo Formal de Software

Información Básica

Textos del Curso

  • Abrial, Jean-Raymond. The B-Book. Assigning Programs to Meanings. 1a ed.
  • Wordsworth, J.B. Software engineering with B.
  • Huth, M.R. and Ryan,M. Logic in computer science : modelling and reasoning about systems. 1ed.
  • Abrial, Jean-Raymond. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010.

Información Específica del Curso

  • El curso busca ilustrar sobre la conveniencia de utilizar una metodología no tradicional de modelamiento de sistemas y desarrollo de software: el modelamiento formal mediante el estudio de casos promueve la necesidad de asignar el grueso del esfuerzo de modelamiento en la especificación y el diseño, antes que en la implementación y depuración. Se utiliza con este fin el método B, apoyado en software de generación automática de obligaciones de prueba y de generación automática de código en Java.

Objetivos Específicos del Curso

Objetivos de aprendizaje:
  • Identificar las ventajas de desarrollar software formalmente.
  • Argumentar por qué los métodos formales son un mecanismo de aseguramiento de la calidad del software.
  • Describir formalmente sistemas completos mediante refinamiento formal.
  • Diseñar y verificar sistemas utilizando el método Event-B.
  • Integrar las obligaciones de prueba en el proceso de desarrollo de software y entender su importancia.
  • Expresar el modelo de un sistema en una herramienta de apoyo al desarrollo formal.
  • Analizar estrategias para realizar una prueba interactiva.
  • Aplicar las pruebas interactivas para el desarrollo y la verificación de sistemas.
  • Modelar formalmente un programa.
  • Construir un programa a partir de su modelo formal.
  • Aplicar herramientas de chequeo de modelos en el diseño.
Relación con los resultados de programa
Resultados de Programa
A B C D E F G H I J K
Relevancia 1 2 1 1 1 5 5

Escala: (1) baja relevancia - (5) alta relevancia.

Tópicos del Curso

  • Uso de matemáticas en modelamiento de sistemas.
  • Dónde integrar métodos formales de diseño.
  • La noción de modelo: parte estática y dinámica.
  • Máquinas, contextos. Un sistema simple.
  • Qué probar de un sistema, invariantes.
  • El cálculo de secuentes. Pruebas en Rodin.
  • Jerarquía de modelos.
  • Relación de la abstracción y el refinamiento.
  • Obligaciones de prueba del refinamiento.
  • Pruebas de refinamiento en Rodin.
  • Qué es un patrón de diseño.
  • Sincronización fuerte y débil.
  • El modelo de un programa.
  • Refinamiento de programas, variante e invariante.
  • Optimizar a partir del invariante.
 
pregrados/dptoccomputacionyelectronica/desarrolloformal.txt · Última modificación: 2014/07/15 15:58 por lsosorio
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki