7/26/2019 TC3005v8 (1)
1/9
TC3005. Mtodos Formales de Ingeniera de Software.
(3 - 0 8. .Requisito: TC2003 Teora de la computacin. 9 ITC).
Equivalencia: No tiene
======================================================
Intencin del curso en el contexto general del plan de estudios
Es un curso de nivel avanzado en el rea de ingeniera de software en donde los
alumnos aprenden a valorar la utilidad de las herramientas formales en Ing. de
Software, as como a usar algunas tcnicas concretas y herramientas
computacionales para especificar propiedades de un sistema de software y
verificarlas formalmente.
Objetivo general del curso:
Al finalizar este curso el estudiante sercapaz de aplicar una metodologa de
mtodos formales para el desarrollo de software, especificar en un lenguaje formal
un producto de software, especificar en un lenguaje formal (no necesariamente el
mismo) las propiedades crticas de diseo de dicho software, y verificar que ste
cumple las propiedades especificadas.
Competencias que desarrolla el curso:
Competencias relacionadas con conocimiento de tareas o formas de
llevarlas a cabo:C1.Ser capaz de identificar y justificar los escenarios donde la aplicacin de mtodos
formales de software puede ser ms benfica desde el punto de vista del costo y
beneficio.
C2.Ser capaz de encontrar, para un sistema de software, las propiedades -expresables
matemticamente- que pueden tener ms impacto en cuanto a la calidad,
seguridad o utilidad de dicho sistema.
C3.Ser capaz de modelar formalmente las caractersticas y propiedades que debe
tener un sistema de software.
C4.Ser capaz de verificar formalmente que un sistema de software cumple con
propiedades previamente establecidas, con ayuda de una herramientacomputacional.
Competencias relacionadas con habilidades analticas y creativas:
Especificacin formal de propiedades
Identificacin y solucin de problemas
Toma de decisiones
7/26/2019 TC3005v8 (1)
2/9
Anlisis de problemas
Anlisis y sntesis de informacin
Anlisis del costo-beneficio
TCNICA DIDCTICA: Aprendizaje basado en proyectos
El instructor del curso debe confeccionar el contenido temtico, considerando el modelo
que adoptar para el desarrollo formal de software. El curso contempla el estudio
obligatorio de la verificacin de modelos (model checking), que puede complementarse
con de otra tcnica ms relacionada con demostracin de teoremas (proof checking).
Para especificar sistemas fijos y acotados, y analizar sus condiciones (modales)
temporales, se sugiere que el instructor seleccione una de las siguientes herramientas (con
los mtodos asociados): SMV, Symbolic Model Checking
SPIN, Communicating Automata
CADP, Process Algebras
DESIGN/CPN, Coloured Petri Nets
Mientras que para especificar sistemas genricos, familias de sistemas, y analizar sus
propiedades, se sugiere que el instructor seleccione una de las siguientes herramientas
(con los mtodos asociados):
Isabelle, HOL, PVS, etc., Lgicas de orden mayor
NuPRL, System F, etc., Teora de tipos
Otter, Vampire, SPASS, etc., Lgica de primer orden (con igualdad)Al seleccionar estas herramientas, el instructor tiene el compromiso de cerrar el mdulo
2, estudiando slo los temas relacionados.
7/26/2019 TC3005v8 (1)
3/9
4. Temas y Sub-temas
1 Panorama de Mtodos Formales en Ing. de Software
1.1 Ques un mtodo formal?
1.2 Algunas aplicaciones industriales
1.3 El papel de los mtodos formales en ingeniera de software1.3.1 Procesos ms rigurosos
1.3.2 Desarrollo de software usando mtodos formales
1.4 Limitaciones de los mtodos formales
1.5 Un panorama de los mtodos formales
1.5.1 Especificacin de comportamiento (autmatas, lgebra de
procesos, lgica temporal, etc.)
1.5.2 Especificaciones basadas en teora de conjuntos (notacin
Z, VDM, el mtodo B, etc.)
1.5.3 Especificaciones algebraicas (tipos, tipos de datos
abstractos, semntica)1.5.4 Verificacin de programas mediante aserciones (lgica de
Hoare, lgica dinmica)
2 Nociones Bsicas y Herramientas Matemticas (elegir slo las necesarias)
2.1 Revisin de conceptos matemticos
2.1.1 Diagnstico de lagunas en conceptos matemticos (Teora
de Conjuntos, Relaciones y funciones, Secuencias, Lgica
proposicional, Consecuencia lgica, Algebras y morfismos,
Induccin matemtica).
2.1.2 Plan individualizado de revisin.
2.2 Ramas de la lgica (Teora de modelos, Teora de demostraciones, Teoraaxiomtica de conjuntos y teora de tipos, Teora de lo computable).
2.3 Lgica Temporal.
2.4 Aplicacin de la Lgica de Hoare a la prueba de programas.
2.4.1 Revisin de los conceptos de Precondiciones y
postcondiciones.
2.4.2 Reglas de la lgica de Hoare.
2.4.3 Clculo de precondiciones ms dbiles.
2.5 Recursividad y Puntos fijos.
2.6 Induccin matemtica bien fundada
2.6.1 Puntos fijos
3 Especificacin de Sistemas de Software y de sus propiedades
3.1 Enfoques de especificacin de un sistema (comportamiento, estructura
(algebraico), etc.)
3.2 Descripcin de sistemas mediante autmatas, procesos, tipos, funciones,
relaciones, lenguaje imperativo, etc.)
3.3 Sintaxis del lenguaje de especificacin
7/26/2019 TC3005v8 (1)
4/9
3.4 Semntica del lenguaje de especificacin
3.5 Especificando con lgica temporal
3.5.1 Propiedades de calidad de alcance (reachability
properties)
3.5.1.1 Clculo del grafo de calidad de alcance
3.5.2 Propiedades de salvedad (safety properties)3.5.2.1 Definicin
3.5.2.2 Salvedad en la prctica
3.5.2.3 El mtodo de variables de historia
3.5.3 Propiedades de vivacidad (liveness properties)
3.5.3.1 Vivacidad en el modelo o en la propiedad
3.5.3.2 Verificacin bajo hiptesis de vivacidad
3.5.3.3 Vivacidad acotada
3.5.4 Propiedad de sin inter-bloqueos (deadlock-freeness)
3.5.4.1 Sin inter-bloqueos vs salvedad, vivacidad
3.5.4.2 Sin inter-bloqueos en combinacin con
abstraccin
3.5.5 Propiedades de equidad (fairness properties)
3.5.5.1 Equidad y no determinacin
3.5.5.2 Propiedades de equidad e hiptesis de equidad
3.5.5.3 Equidad fuerte y equidad dbil
3.5.5.4 Equidad en el modelo o en la propiedad
3.5.6 Mtodos de abstraccin
3.5.6.1 Cundo es necesario usar un modelo de
abstraccin
3.5.6.2 Abstraccin mediante el aglutinamiento de
estados3.5.6.3 Abstraccin en las variables
3.5.6.4 Abstraccin por restriccin
3.5.6.5 Qupuede demostrarse en el autmata
abstracto?
3.6 Especificando con lgicas clsicas (y no clsicas)
3.6.1 Correccin
3.6.2 Calidad de cobertura
3.6.3 Terminacin
3.6.4 Refinamiento
4 Verificacin formal de Software4.1 Verificacin de propiedades modales y temporales
4.1.1 Qupuede hacerse con la herramienta seleccionada?
4.1.2 Simulacin
4.1.3 Anlisis
4.1.4 Registro de documentacin existente y casos de estudio
4.2 Verificacin de propiedades de correccin, terminacin, etc.
7/26/2019 TC3005v8 (1)
5/9
4.2.1 Qupuede hacerse con la herramienta seleccionada?
4.2.2 Sistema de inferencia
4.2.3 Mtodos de inferencia
Registro de documentacin existente y casos de estudio
7/26/2019 TC3005v8 (1)
6/9
OBJETIVOS ESPECIFICOS DE APRENDIZAJE
1 Panorama de Mtodos Formales en Ing. de Software
Que el estudiante valore la necesidad de herramientas formales para el
desarrollo de software, e identifique las situaciones en que la verificacin formal
es especialmente importante.
Que el estudiante adquiera un panorama general y una taxonoma de los
distintos tipos de mtodos (lgicos, descriptivos, operacionales, etc.) y
herramientas que se han utilizado para la verificacin formal de software, sus
respectivas ventajas y debilidades, ascomo sus aplicaciones.
2 Nociones Bsicas y Herramientas Matemticas (elegir slo las necesarias)
Que el estudiante repase o adquiera las nociones bsicas necesarias para los
mtodos que se vern luego en el.
3 Especificacin de Sistemas de Software y de sus propiedades
Que el estudiante especifique un sistema usando un lenguaje formal (autmatas,
lgebra de procesos, lenguajes de especificacin algebraicos, Z, etc.).
Que el estudiante conozca y pueda manejar un ambiente computacional
especfico para escribir especificaciones formales.
Que el estudiante conozca los distintos tipos de propiedades que pueden
requerirse acerca de un software (viveza, calidad de alcance, propiedades
estructurales, condiciones siempre falsas, salvedad, respuesta, precedencia,
dependientes del dominio del sistema, etc.).
Que el estudiante sea capaz de encontrar, en un caso espec fico, las propiedades
que son crticas y que deben respetarse desde el diseo hasta la implementacin.
Que el estudiante sea capaz de expresar, en un lenguaje formal dado,
propiedades de un sistema expresadas informalmente.
Que el estudiante conozca y pueda manejar un ambiente computacional
especfico para expresar concretamente propiedades de un sistema.
4 Verificacin formal de Software
Que el estudiante conozca las distintas opciones de herramientas que existen
para hacer verificacin formal de software, de acuerdo al enfoque usado en la
especificacin del sistema y de sus propiedades.
Que el estudiante aplique al menos dos herramientas existentes para verificar
formalmente, una de ellas siendo Model Checking (que debe manejaraceptablemente).
Que el estudiante conozca las distintas opciones para Model Checking, como:
simulacin (explora los estados alcanzados por el sistema), bsqueda exhaustiva,
Run Time Result Checking, generacin de contra-ejemplos, etc.
7/26/2019 TC3005v8 (1)
7/9
Que el estudiante sea capaz de utilizar los mtodos de verificacin formal de
software en casos especficos, y con ayuda de herramientas computacionales de
soporte a dichos mtodos.
7/26/2019 TC3005v8 (1)
8/9
Metodologa del curso: Se sugiere POL, idealmente en combinacin con otra materia en
que se haga tambin un desarrollo de software basado en mtodos como UML.
TIEMPO ESTIMADO DE CADA TEMA
1. Panorama de los Mtodos Formales (6 horas)
2. Nociones Bsicas y Herramientas Matemticas (6 horas)
3. Especificacin de Software y sus propiedades (24 horas)
4. Verificacin formal de Software (12 horas)
Total: 48 horas
POLITICAS DE EVALUACION SUGERIDAS
Examenes Parciales 30%
Tareas, lecciones aprendidas 10%
Examen Final 20%
Desarrollo del Proyecto de aplicacin del mtodo
formal
40%
Bibliografa:
Understanding Formal Methods
by Jean-Francois Monin, M.G. Hinchey(Translator)
Paperback:276 pages
Publisher:Springer; 1 edition (January 17, 2003)
Language:English
ISBN:1!2332"76
Consulta:
Systems and Software Verification : Model-Checking Techniques and Tools
by B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, P. Schnoebelen,P. McKenzie (Translator)
Publisher: Springer; 1 edition (August 9, 2001)
Language: English
ISBN: 3540415238
Automated Theorem Proving in Software Engineering
by D. Loveland (Foreword), Johann M. Schumann
http://www.amazon.com/exec/obidos/search-handle-url/index=books&field-author-exact=Jean-Francois%20Monin/102-2158379-0539323http://www.amazon.com/exec/obidos/search-handle-url/index=books&field-author-exact=M.G.%20Hinchey/102-2158379-0539323http://www.amazon.com/exec/obidos/search-handle-url/index=books&field-author-exact=M.G.%20Hinchey/102-2158379-0539323http://www.amazon.com/exec/obidos/search-handle-url/index=books&field-author-exact=Jean-Francois%20Monin/102-2158379-0539323http://www.amazon.com/exec/obidos/search-handle-url/index=books&field-author-exact=M.G.%20Hinchey/102-2158379-05393237/26/2019 TC3005v8 (1)
9/9
Hardcover: 228 pages
Publisher: Springer; 1 edition (June, 2001)
Language: English
ISBN: 3540679898
Model CheckingEdmund M. Clarke, Orna Grumberg, Doron A. Peled
The MIT Press, 2000
ISBN 0262032708
The Spin #odel $he$%er, pri&er and re'eren$e &anual
erard J *ol+&annddison -esley, 200"ISBN 0-321-22862-6
The Way of Z: Practical programming with formal methods
Jonathan JackyOxford University Press
Adicionalmente incluirse material bibliogrfico propio de las herramientas seleccionadas
por el profesor.
Top Related