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-0539323

7/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.