Mtodos para la Construccin de Software Fiable
Mara del Mar Gallardo Pedro Merino Dpto. de Lenguajes y Ciencias de la Computacin Universidad de Mlaga (gallardo, pedro)@lcc.uma.es
Curso de doctorado Mtodos para la Construccin de Software Fiable- 2004/2005 1
Mtodos para la Construccin de Software Fiable Programa/Evaluacin
1. 2. 3. 4. 5. 6. 7. 8. 9. Introduccin Model Checking con TDFs Anlisis Esttico Abstract Model Checking Herramientas (Laboratorio) Model Checking Software Conferencia Realizacin de trabajos (3 semanas) Exposicin de trabajos
Curso de doctorado Mtodos para la Construccin de Software Fiable- 2004/2005
Mtodos para la Construccin de Software Fiable Programa/Evaluacin 1. Introduccin
Motivacin-Algunos errores software Revisin de tcnicas/herramientas de anlisis Tendencia: Integracin de tcnicas y Model Checking Software Referencias
Curso de doctorado Mtodos para la Construccin de Software Fiable- 2004/2005
Algunos errores software
Industria espacial
Mariner 1 Ariane 501 Mars PathFinder Mars Polar Lander
Comunicaciones
Fallos en servicio AT&T
Salud
Therac-25
Aviacin comercial
Peter Ladkin, Universidad de Bilelefed
Armamento
Misiles
Curso de doctorado Mtodos para la Construccin de Software Fiable- 2004/2005
Mariner 1
Proyecto de la NASA para enviar sonda a Venus (1962)
G.J. Myers, Software Reliability: Principles & Practice
Fallo:
Error en una sentencia de cdigo FORTRAN
Efecto
Perdida de la sonda
Curso de doctorado Mtodos para la Construccin de Software Fiable- 2004/2005
... IF (TVAL .LT. 0.2E-2) GOTO 40 DO 40 M = 1, 3 W0 = (M-1)*0.5 X = H*1.74533E-2*W0 DO 20 N0 = 1, 8 EPS = 5.0*10.0**(N0-7) CALL BESJ(X, 0, B0, EPS, IER) IF (IER .EQ. 0) GOTO 10 20 CONTINUE DO 5 K = 1. 3 DO 5 K = 1, 3 T(K) = W0 Z = 1.0/(X**2)*B1**2+3.0977E-4*B0**2 D(K) = 3.076E-2*2.0*(1.0/X*B0*B1+3.0977E-4* *(B0**2-X*B0*B1))/Z E(K) = H**2*93.2943*W0/SIN(W0)*Z H = D(K)-E(K) 5 CONTINUE 10 CONTINUE Y = H/W0-1 40 CONTINUE ...
Mariner 1
Curso de doctorado Mtodos para la Construccin de Software Fiable- 2004/2005
Ariane 501
Proyecto de la ESA para poner satlites en rbita (1996)
Nota de prensa ESA (http://www.esrin.esa.it/htdocs/tidc/Press/Press96/ariane5rep.html)
Fallo:
Conversin de un flotante de 64 bits relativo a la velocidad horizontal a un entero de 16 bits. El nmero era mayor de 32,768 Reutilizacin de cdigo del Ariane 4
Efecto
Explosin a los 40 segundos del despegue Valor estimado con la carga: 500 millones de dolares
Curso de doctorado Mtodos para la Construccin de Software Fiable- 2004/2005
rate-item
cust-rec c nm/justsa GET
Curso de doctorado Mtodos para la Construccin de Software Fiable- 2004/2005
Mars PathFinder
Proyecto de la NASA para analizar la superficie de Marte (1997)
Vehculo para toma de muestras
Fallo:
Implementacin errnea mecanismo de acceso a memoria compartida junto con prioridades. Inversin de prioridades
Efecto:
Reset del software de forma inesperada
Curso de doctorado Mtodos para la Construccin de Software Fiable- 2004/2005
Mars Climate Orbiter
Proyectos de la NASA para analizar la superficie de Marte (1999)
Informe NASA (ftp://ftp.hq.nasa.gov/pub/pao/reports/1999/MCO_report.pdf )
Fallo:
Implementacin errnea de la traduccin entre millas inglesas y metros
Efecto
Perdida de la nave Mars Climate Orbiter en la aproximacin a Marte Perdida de Mars Polar Lander ?
Curso de doctorado Mtodos para la Construccin de Software Fiable- 2004/2005
10
Misiles Patriot
Un misil Patriot de EEUU falla al interceptar un misil Scud Iraqui (1991)
(http://www.math.psu.edu/dan/disasters/patriot.html)
Fallo
Calculo errneo del tiempo desde que se arranc el ordenador por errores aritmticos al aproximar el reloj Los errores se deben al uso de slo 24 bits para representar 1/10.
Efecto
28 soldados muertos y 100 heridos
Curso de doctorado Mtodos para la Construccin de Software Fiable- 2004/2005
11
Errores con Misiles
SEN | Date of References| Description | Event ----------+--------------------------------------------------+--------5/3 | 50 false alerts from NORAD defense system | 1979 | | 8/3 | NORAD defense radar system mistook the Moon for | | a hostile incoming missile | 8/3 | | | | | | | | | | | | | | Computer error caused US naval vessel to open | Jul 1983 fire 180 degrees off target, in the direction of | Mexican merchant ship | || 180 degree heading error caused Soviet test | Dec 1984 missile to aim for Hamburg instead of the Arctic | HMS Sheffield radar system identified incoming Argentinian Exocet missile as non-Soviet & thus friendly; no alarm was raised and the ship sank
8/5
10/2
Curso de doctorado Mtodos para la Construccin de Software Fiable- 2004/2005
12
Fallos en AT&T
Software de las centrales de conmutacin de AT&T en EEUU (1990) Fallo
Sentencia Break mal empleada en una lnea de cdigo incluida como patch
Efecto
9 horas sin servicio telefnico en varias ciudades otro error similar corta comunicaciones con Grecia (1979) Desarrollo de herramientas propias
Curso de doctorado Mtodos para la Construccin de Software Fiable- 2004/2005
13
Therac-25
Acelerador de electrones para tratamiento del cancer (1985-1987)
Curso de doctorado Mtodos para la Construccin de Software Fiable- 2004/2005
14
Therac-25
Fallo
Sentencias muy seguidas de modo X y modo b (menos de 8 segundos). El sistema no lo haba hecho antes. l equipo emite radicacin potente sin protector
Efecto
6 muertos
Curso de doctorado Mtodos para la Construccin de Software Fiable- 2004/2005
15
Aviacin
Curso de doctorado Mtodos para la Construccin de Software Fiable- 2004/2005
16
Aviacin Civil
Deadlock en F16, confusin entre derecha e izquierda volando invertido Vuelo de Air New Zealand cae al detectarse un error software pero sin informar a la tripulacin (1979) Piloto automtico de China Airlines 747 hace caer el avin cerca de San francisco (1985) Errores en el nuevo software causan la caida de Korean Air Lines B747 en Guam (1997) Versin militar de Boeing B737-200 cae en Dubrovnik (Croacia) (1996)
Curso de doctorado Mtodos para la Construccin de Software Fiable- 2004/2005
17
Otros campos ..
SEN | Date of References| Description | Event ----------+--------------------------------------------------+--------10/2 | "Compatible" teller machines of 2 British banks | Jan 1985 | handled leap years differently, witholding cash | | and confiscating cards during New Year holiday | 10/3 | Federal Reserve inter-bank transaction amounts | | multiplied by 1000 because data input procedures | | were inconsistent between client banks | | Robot killed Japanese auto worker attempting to | repair another robot | Jul 1981 |
10/3
10/3
| 14000 Ford Lincolns recalled because computer in | | air suspension system had overheating problem, | | causing automobile to burst into flames |
Curso de doctorado Mtodos para la Construccin de Software Fiable- 2004/2005
18
Otros campos ..
Hardware Sistemas operativos Industria del automvil Procesos de negocios
Las grandes empresas crean grupos para fiabilidad del software NASA, MICROSOFT, INTEL, LUCENT, VOLVO,
La fiabilidad se aborda ACTULMENTE mediante tcnicas de
TESTING/ANALISIS AUTOMTICO
Curso de doctorado Mtodos para la Construccin de Software Fiable- 2004/2005
19
Qu puede obtenerse del anlisis ?
Optimizacin de cdigo (secuencial) Ejecucin paralela/distribuida Transformacin Deteccin de errores Otras informaciones
Curso de doctorado Mtodos para la Construccin de Software Fiable- 2004/2005
20
Tcnicas de Anlisis Automtico/Semi-automtico
Tcnicas tradicionales Compilacin Compilacin especial (optimizada, warnings, ..) Chequeo de buen estilo (p.e. lint) Depuradores ..........
Curso de doctorado Mtodos para la Construccin de Software Fiable- 2004/2005
21
Tcnicas de Anlisis Automtico/Semi-automtico
Anlisis esttico Anlisis de flujo de datos Interpretacin abstracta Anlisis basado en restricciones Chequeo de tipos
Anlisis de de programas
(Prog. Secuencial )
Curso de doctorado Mtodos para la Construccin de Software Fiable- 2004/2005
22
Tcnicas de Anlisis Automtico/Semi-automtico
Anlisis dinmico Anlisis de alcanzabilidad (Validacin) Alcanzabilidad + chequeo de propiedades (Lgica temporal) (Model-Checking) Anlisis en tiempo de ejecucin (Testing)
Anlisis del espacio de estados
(Prog. Concurrente )
Curso de doctorado Mtodos para la Construccin de Software Fiable- 2004/2005
23
Tcnicas de Anlisis Automtico/Semi-automtico
Deduccin automtica Representacin del programa y las propiedades con Lgica de orden superior y uso de herramientas que asisten en la bsqueda de errores/demostraciones
Demostracin de teoremas
(Prog. Secuencial/Concurrente )
Curso de doctorado Mtodos para la Construccin de Software Fiable- 2004/2005
24
Otras Tcnicas de Anlisis SemiAutomtico
Tcnicas de anlisis a priori (sobre modelo)
Programacin entera Programacin lgica .......
Tcnicas de anlisis posteriori (sobre cdigo)
Pruebas de conformidad Otros tipos de test
Curso de doctorado Mtodos para la Construccin de Software Fiable- 2004/2005
25
Revisin de Herramientas empleadas para Testing/Anlisis Automtico/Semi-automtico
Curso de doctorado Mtodos para la Construccin de Software Fiable- 2004/2005
26
Propiedades Modelo Alto nivel
Model checking Generacin de cdigo
Spin Cospan Smv
efic acad ientes mi cas
Promela, CFSM, Petri Lgica Temporal, Autmatas
Nivel de Abstraccin
Propiedades Diseo detallado
Anlisis de alcanzabilidad Generacin de cdigo
Tau Rational Rose Rahapsody Visual State
com inef erciales icie ntes
SDL, UML, StateCharts MSC, Autmatas
Anlisis esttico o dinmico no exhaustivo C, C++, Java Sockets, RPC, middleware
Curso de doctorado Mtodos para la Construccin de Software Fiable- 2004/2005
Cdigo a depurar
Visual Threads Insure ++ Purify Code wizard
co ine merc fic ien te
27
Propiedades
Lgica de orden superior Deduccin automtica
PVS Isabelle HOL
acad inef micas icie ntes
Espec. Programa
Curso de doctorado Mtodos para la Construccin de Software Fiable- 2004/2005
28
Nuevas Herramientas para Anlisis Automtico: Anlisis esttico + Model checking + Demostracin de Teoremas
Curso de doctorado Mtodos para la Construccin de Software Fiable- 2004/2005
29
Modelos abstractos
Propiedades Modelo Alto nivel
Model checking Generacin de cdigo
Spin Cospan Smv
1. Abstraccin
Spin (U. Mlaga) 3VMC (U. Tel Avi)
Promela, CFSM, Petri Lgica Temporal, Autmatas
Integracin
Propiedades
2. Extraccin de modelos +1 FeaVer (Lucent) Bandera (U. Kansas) JPF1 (NASA) 3. Model Checking Software +1 +2 (exhaustivo) SLAM (Microsoft) JPF2 (NASA) Verisoft (Lucent)
Diseo detallado
Anlisis de alcanzabilidad Generacin de cdigo
Tau Rational Rose Rahapsody Visual State
SDL, UML, StateCharts MSC, Autmatas
Anlisis esttico o dinmico no exhaustivo C, C++, Java Sockets, RPC, middleware
Cdigo a depurar
Visual Threads Insure ++ Purify Code wizard
Curso de doctorado Mtodos para la Construccin de Software Fiable- 2004/2005
30
Referencias
Libros sobe anlisis de software
F. Nielson, H.R. Nielson, C. Hankin Principles of Program Analysis, 1998, Springer G.H. Holzmann, The SPIN Model Checker, 2004, Prentice-Hall D. Peled Software Reliability Methods, 2001,Springer E. M. Clarke and O. Grumberg and D. A. Peled, Model Checking, 2000, The MIT Press B. Brard et. al, Systems and Software Verification. Model Checking Techniques and Tools, 1999, Springer
Artculos tipo survey
G. 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.
Curso de doctorado Mtodos para la Construccin de Software Fiable- 2004/2005
31
