MFDS–Curso 2015-2016– 1
Metodos Formales de Desarrollo de Software
Grado en Ingenierıa Informatica
Paqui LucioDpto de Lenguajes y Sistemas Informaticos.
Grado en Ingenierıa Informatica MFDS–Curso 2015-2016– 1
MFDS–Curso 2015-2016– 2
1.- Introduccion
1.- Introduccion
La construccion de software matematicamente correcto hasido historicamente un gran reto, aunque controvertido.
En 1949, Turing primera prueba formal de correccion.
La idea de programacion estructurada, junto con laimportancia de la correccion de programas, nacen
a finales de los 1960scomo reaccion a la denominada crisis del softwareFloyd (1965), Hoare (1969), Dijkstra (1970), ...
En los 70’s empiezan a aparecer los primeros intentos demecanizar la verificacion de programas.
Grado en Ingenierıa Informatica MFDS–Curso 2015-2016– 2
MFDS–Curso 2015-2016– 3
1.- Introduccion
1970s: Lenguajes formales/con aserciones (LCF/ML, GYPSY,Euclid), Demostradores (Boyer-Moore), Especificacion formal(VDM), tipos algebraicos, logica temporal, ...
1980s: Model checking, verificacion de hardware,demostradores automaticos (HOL,Nuprl,Coq,Isabelle), logicasdinamicas (TLA), lenguajes (Z, OBJ3, Eiffel), ...
1985-87: Therac-25: maquina tratamiento cancer
1990s: Verificacion de software crıtico industrial (Metodo B,Praxis Critical Systems), ... ...
1994: error FDIV (div. coma flotante) del Intel Pentium1996: explota el Ariane-5
Grado en Ingenierıa Informatica MFDS–Curso 2015-2016– 3
MFDS–Curso 2015-2016– 4
1.- Introduccion
El metro de Parıs
Linea 14: Trenes guiados por software (sin conductor)
Sistema especificado completamente en el metodo B (110.000lıneas)
Verificado utilizando distintas herramientas (1.000 proofobligations, 92% probado automaticamente)
Software obtenido por traduccion (automatica) de laespecificacion (86.000 instrucciones en Ada)
Fue puesto en funcionamiento en 1998 (sin error, hasta hoy)
Grado en Ingenierıa Informatica MFDS–Curso 2015-2016– 4
MFDS–Curso 2015-2016– 5
1.- Introduccion
2002: Bill Gates reconoce la importancia de verificar elsoftware:
Software verification has been the Holy Grail ofcomputer science for many decades, but now insome key areas, for example, driver verification, weare building tools that can do actual proof about thesoftware and how it works, in order to guaranteereliability.
Grado en Ingenierıa Informatica MFDS–Curso 2015-2016– 5
MFDS–Curso 2015-2016– 6
1.- Introduccion
2003: Tony Hoare: The Verifying Compiler: A GrandChallenge for Computing Research:
A mature scientific discipline should set its own agenda and pursue ideals of purity,
generality, and accuracy far beyond current needs. Science explains why things work in full
generality by means of calculation and experiment. An engineering discipline exploits
scientific principles in the study of the specification, design, construction, and production
of working artifacts, and improvements to both process and design. The verification
challenge is to achieve a significant body of verified programs that have precise external
specifications, complete internal specifications, machine-checked proofs of correctness with
respect to a sound theory of programming.
reto internacional a 10 o 15 anos.objetivo: el compilador verificador.no solo software crıtico
Grado en Ingenierıa Informatica MFDS–Curso 2015-2016– 6
MFDS–Curso 2015-2016– 7
1.- Introduccion
2005: La empresa “Praxis Critical Systems” da una garantıade 10 anos que cubre fallos de software.
2010: Primera Verified Software Competition
se celebra anualmentealgunas conferencias internacionales han incluido tambiencompeticiones de verificadores (Verification Tools).
Grado en Ingenierıa Informatica MFDS–Curso 2015-2016– 7
MFDS–Curso 2015-2016– 8
1.- Introduccion
2011: Algunas consideraciones pragmaticas de un experto:
Grado en Ingenierıa Informatica MFDS–Curso 2015-2016– 8
MFDS–Curso 2015-2016– 9
1.- Introduccion
2012: Obligatorio el uso de metodos formales y de ve-rificacion del software (crıtico) para ser certificado por la RTCA:
“... Formal methods are mathematically-basedtechniques for the specification, development andverification of software aspects of digital systems.The mathematical basis of formal methods consistsof formal logic, discrete mathematics andcomputer-readable languages. The use of formalmethods is motivated by the expectation that, as inother engineering disciplines, performing appropriatemathematical analyses can contribute to establishingthe correctness and robustness of a design.”
(Suplemento sobre metodos formales en la certificacion DOC-178C)
Grado en Ingenierıa Informatica MFDS–Curso 2015-2016– 9
MFDS–Curso 2015-2016– 10
1.- Introduccion
En el artıculo de IEEE Intelligent Systems, 2014:
Reasoning and Verification: State of the Art and Current Trends(by B. Beckert & R. Hahnle)
aparecen 27 sistemas usados en verificacion de programascomo seleccion de los mas representativos del estado del arte.
Grado en Ingenierıa Informatica MFDS–Curso 2015-2016– 10
MFDS–Curso 2015-2016– 11
1.- Introduccion
Nombre LP Creador Otros detalles
Spark Ada Altran Praxis Comerial
Chalmers Univ.KeY Java Univ. of Karlsruhe Java Card
Univ. of Koblenz.
Spec# C# Microsoft pionero de Microsoft
Why(3) WhyML INRIA, CNRS, Genera OCaml
Java, C, Ada Univ. Paris
Verifast Java, C Univ. of Leuven Separation Logic
Dafny Dafny Microsoft Genera C#
Grado en Ingenierıa Informatica MFDS–Curso 2015-2016– 11
MFDS–Curso 2015-2016– 12
1.- Introduccion
Algunos sistemas de verificacion automatica
combinan la verificacion con tecnicas de depuracion (e.g.contraejemplo de una propiedad asertada)generan codigo de lenguaje comercial (e.g. C++, Java, C#)generan invariantesgeneran expresiones que decrecenno hacen demostracion completamente automatica, sinoasistida (proof-asistants: HOL, Isabel, Coq, ... )generan la hipotesis de inducconhacen pruebas automaticas por induccion...
Grado en Ingenierıa Informatica MFDS–Curso 2015-2016– 12