La presencia de errores en el software es una constante desde que se
diseñaron los primeros lenguajes de programación, y su depuración
siempre ha sido uno de los mayores problemas de su desarrollo.
En este curso, se da una  visión del amplio panorama de las  técnicas y herramientas
más recientes y potentes  para análisis  automático del software
con el fin de aumentar su fiabilidad. Se organizan las aportaciones del mundo
académico e industrial en los  últimos años  y se da una perspectiva de la integración
que se está produciendo, que llevará sin duda a que las técnicas de análisis automático
de errores forme parte de los futuros entornos de desarrollo,
especialmente para aplicaciones como protocolos de comunicación, sistemas oprativos o sistemas empotrados.

El curso se centra en el uso métodos formales para la construcción de software fiable. De forma general,
podemos decir que los métodos  formales son notaciones y técnicas para analizar sistemas,
con prestaciones  mucho más potentes que las realizadas por los compiladores o depuradores.
Son  formales en el sentido de que están basados en alguna teoría
matemática como, por ejemplo, la lógica. En la actualidad se consideran  de mayor interés
los métodos formales denominados fuertes que permiten   la automatización casi completa
de todo el proceso de análisis del software. Los métodos formales, en este contexto, son útiles
para eliminar ambigüedades, y para depurar sistemas. Pueden usarse  para verificar que un sistema
satisface su especificación, o para  encontrar algún caso en el que no lo hace.
Su uso disminuye el tiempo dedicado a encontrar errores de  diseño o de codificación.
Actualmente estám soportados por un conjunto maduro de herramientas
de análisis automático como SPIN, SMV o UPPAAL.

Introducción
Fundamentos de Model Checking

Data Flow Analysis
Interpretación Abstracta
Model Checking Abstracto

Bibliografía

D. A. Peled, Software Reliability Methods, 2001, Springer
E. M. Clarke and O. Grumberg and D. A. Peled, Model Checking, 2000, The MIT Press
B. Bérard et. al, Systems and Software Verification. Model Checking Techniques and Tools, 1999, Springer
F. Nielson, H. R. Nielson, C. Hankin, Principles of Program Analysis, 1998, Springer
G.J. Holzmann. The Spin Model Checker, 2003, Addison-Wesley
G. J. Holzmann, Design and Validation of Computer Protocols, 1991, Prentice-Hall

Material de consulta addicional

•Artículos tipo “survey”

– Clarke E. M., Wing J. M.,  Formal Methods: State of the Art and Future Directions,
ACM Workshop on Strategic Directions in Computing Research, ACM Computing Surveys vol. 28(4): 626-643, 1996.

–Gunter C., Mitchell J.,  Strategic Directions in Software Engineering and Programming Languages,
ACM Workshop on Strategic Directions in Computing Research, ACM Computing Surveys, 28(4): 727-737, 1996.

•Informes sobre errores software