Verification of Embedded Software:
Problems and Perspectives
Andrea Minuto 801040
Barbara De Vido 802663
Analisi e Verifica Programmi A.A.2004/2005
Sommario
1. Introduzione
2. Metodi Formali
3. Sfide nella verifica dell’E.S.
4. Conclusioni
5. Bibliografia
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
1. Introduzione
2. Metodi Formali
3. Sfide nella verifica dell’E.S.
4. Conclusioni
5. Bibliografia
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
1. Introduzione
• Definizione Embedded Software(E.S.):
– Usati in sistemi elettronici a microprocessore
progettati appositamente per determinate
applicazioni (ad hoc).
– Operano in autonomia o connessi ad altri pc.
– Funzioni tipicamente di monitoring e controllo.
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
1. Introduzione
• Situazione attuale
– Numero e quantità di E.S. in crescita continua
– Mantenendo il tasso di crash attuale e
moltiplicando per 10 il volume dei software
attuali si otterrebbero pc che vanno in crash
ogni 3 minuti!!
– Inaccettabile per applicazioni Safety-Critical
– Tecniche di Verifica (formali e non) devono
scalare di conseguenza dato che non sono
linearmente proporzionali alla dimensione del
SW
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
1. Introduzione
• Evidenzieremo alcuni problemi ed
soluzioni di interpretazioni astratte basate
su analisi statiche.
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
1. Introduzione
2. Metodi Formali
3. Sfide nella verifica dell’E.S.
4. Conclusioni
5. Bibliografia
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
2. Metodi Formali
• Definizione rigorosa tramite formalismo
algebrico.
• Grosso potenziale applicativo.
• Costo elevato
• Rallentamento del processo di sviluppo
• Richiedono cambiamenti nel ciclo di
sviluppo
Vediamo ora due casi studio…
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
2. Casi studio
• Driverless Meteor line 14 (Parigi):
– B-Method verificato con teoremi
interattivi
– Attualmente attivo e nessun incidente
– Possibili errori in interfacce (non
sviluppati in B)
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
2. Casi studio
• Arian 5:
– Causa crash:
• Spegnimento processore sistema inerziale
– Fallimento dovuto ad un eccezione non
gestita
– Conversione non protetta da fp 64b a int 16b
– Origine:
• Trovato tramite interpretazione astratta su analisi
statica
• Non tutti gli errori posso essere trovati
– Solo approssimazioni!
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
2. Model Checking
• Metodo formale più industrializzato
• Definizione:
– Tecnica algoritmica per controllare che il
comportamento di un sistema a stati di transizione sia
conforme alle specifiche del comportamento
temporale.
• Caratteristiche
– Utilizzato soprattutto dai costruttori HW (Proc.)
– Enumerazione esaustiva dello spazio degli stati
– Dimensione dello spazio degli stati è esponenziale
rispetto alla dimensione del modello
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
2. Model Checking
• NON PROVA CHE E’CORRETTO
• Trova i bug che altri metodi informali
(testing e simulazione) non trovano.
• Ancora molto da SVILUPPARE
• Rimangono necessari per la validazione e
la verifica:
• Debugging
• Simulations
• Runtime test
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
1. Introduzione
2. Metodi Formali
3. Sfide nella verifica dell’E.S.
4. Conclusioni
5. Bibliografia
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
1. Modelli software
6. Modularità
2. Specifiche
7. Timing
3. Strutture controllo
8. Proprietà
4. Proprietà numeriche
9. Distribuzione & …
5. Strutture dati
10. User interfaces
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
3.1. Modelli Software
• Semantiche di linguaggi di
programmazione sono Modelli standard
• Formalizzano l’esecuzione di programma
in termini matematici astratti
• Sono base di analisi e verifica del S.W.
• Vantaggi
– Tools producono automaticamente un modello
del programma da verificare
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
3.1. Modelli Software
• Problemi:
– Gli standard cambiano di continuo
– I compilatori non implementano strettamente
le specifiche degli standard esistenti
Comportamenti diversi del programma
– Librerie con specifiche NON formali
– Tools di verifica non aderenti allo “standard
reale”
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
3.1. Far funzionare le astrazioni
• Nel M.C. il modello è datoverifica ad
esso relativa
• Preserva solo le caratteristiche
selezionate più semplici(approssimazione)
• Requisiti del design del modello:
1. Un linguaggio per l’implementazione
2. Un linguaggio di verifica per il modello
3. Un linguaggio logico per le specifiche
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
3.1. Far funzionare le astrazioni
• Utilizzo di astrazione come via di mezzo
tra modello concreto e modello “di
approssimazione più astratto”
• Modello concreto finitofunzioni di
astrazione e concretizzazione computabili
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
3.1. Astrazione
• Se modello concreto non finito allora…
– Uso di un modello Astratto FINITO
– Possibile automazione del design
• Prova Soundness:
– Metodo deduttivo
• Prova Astrazione = prova argomento induttivo
– Check sul modello astratto
• Prova Astrazione = prova diretta modello concreto
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
3.1. Astrazione
• Problema scelta Astrazione:
– Beneficio non sempre visibile
– Modifica programmarifare scelta
• Difficoltà di applicazione su Embedded
software che evolve lentamente
• Studio di previsione sulle modifiche e
mantenimento
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
3.1. Astrazioni standard
• Astrazione fornita come modello finito.
– Utente non deve estrarre il modello.
– Sceglie solo tra astrazioni predefinite.
• Analizzatore applicato a infiniti programmi
• Astrazioni dominio infinito con Widening e
Narrowing
• Necessaria classe di astrazioni “general
purpose”
• Problema: falsi allarmi
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
3.1. Widening/Narrowing
• Necessarie per domini astratti infiniti che
non soddisfano le condizioni catena
• Accelerano convergenza al punto-fisso
• Tecniche di approssimazione dinamica
(astrazione statica)
• Astrazioni esprimibili come Widening
• Assicura l’esistenza della
rappresentazione e del modello iniziale
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
3.1. Widening/Narrowing
• Widening su thresholds=astrazione statica
– Poca espressività
• Widening dinamico risolve il problema
state space explosion nel model checking
• Modello è esplorato più volte su differenti
livelli di astrazioni determinate
dinamicamente da widenings
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
3.2. Specifiche
• Linguaggio di specifica in model check:
– Logico temporale
– Calcolo punto-fisso
• Specifica fornita automaticamente o dall’utente
per test astratti
• Entrambi i casi analisi simili
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
3.3. Strutture di controllo
• Flat modelling non è adatto a linguaggi
funzionali
– Struttura dati finita ≠> semantica finita
• Anche strutture sempliciastrazioni di
controllo sono:
– Grezze
– Utilizzabili solo per proprietà sicure
• Es: modelli control-flow per “liveness”
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
3.3. Strutture di controllo
• Astrazione dal basso:
– Verifica di una proprietà alla volta
– Necessari più modelli (uno per ogni prop.)
• Astrazione dall’alto:
– Verifica safety ma non liveness
• Futuro embedded software:
– Multithreaded programming
• Richiesta di competenza High level e strumenti di
analisi precisi per superare il problema control-flow
(race condition,untrapped exception,deadlocks).
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
3.4. Proprietà numeriche
• Proprietà Interi:
– Gestite da astrazioni nei domini infiniti erano
non relazionali poi relazionali
• Relazionali:
– Il numero di valori connessi limitato
• Staticamente
• Dinamicamente (widenings molto usato nel model
checking)
• Ancora molto da fare…
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
3.4. Proprietà numeriche
• Proprietà floating point:
– Computaz. fp molto usate con precisione fissa
– Incontrollabile perdita di precisione
– Errori run-time dovuti alla non validità delle
leggi algebriche
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
3.4. Esempio errore Patriot
Velocità di crociera:
MACH 2 (1522 mph)
( 2450 km/h )
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
3.5. Strutture dati
• Generalmente ignorate in model checking
• Quando usata:
– Di solito informale…
– Su base sintattica…
No per proprietà
liveness
• Embedded sw non può ignorare struttura
dati, cast e aliases (es.:puntatori…)
• Astrazioni standard ancora da sviluppare
– Es.:Domini ristretti per check over flow
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
3.6. Modularità
• Modelli del model checking possono
seguire la struttura dell’analisi statica.
• Metodi di composizione:
1. Analisi basata sulla semplificazione
2. Analisi casi peggiori
3. Analisi separata con interfacce
4. Analisi simbolica relazionale
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
3.7. Timing
• Embedded S.W. devono rispettare vincoli
di tempo
• Costruzione manuale di modelli
estremamente difficile se non impossibile
– Limiti di pochi microsecondi
– Vanno prese in considerazione cache e
pipeline di sistema
• Idem in analisi del programma
– semantica a livello assembler
– Modello di tempo del processore stesso
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
3.8. Proprietà
Di terminazione e Unbound liveness
• Testare liveness è più difficile che testare
safety
• Facile nei modelli finiti  perché prova
liveness = prova stronger safety
• Difficile per modelli infiniti  uso di
funzioni varianti difficili da identificare.
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
3.9. Distribuzione e mobilità
• Passaggio da controllo centralizzato a
controllo distribuito
– Cambio radicale di modelli programmazione
• Es: Shared memory  message passing
– Ragionare in termini di insiemi di tracce e non
di sequenze di insiemi di stati
• Astrazioni set-based inadeguate
– Evoluzione rapida LAN  WAN
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
3.9. Distribuzione e mobilità
• Mobilità importante
• Cambi continui nella topologia di
comunicazione
• Uso di strutture ricorsive unbounded di
difficile analisi
• Verifica delle proprietà difficile
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
3.10. User interfaces
• Interfacce utenti sono considerate tools.
• I tools basati su metodi formali rispondono
» SI
» NO
• Non sono ancora in grado di rispondere a
quesiti incerti
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
1. Introduzione
2. Metodi Formali
3. Sfide nella verifica dell’E.S.
4. Conclusioni
5. Bibliografia
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
4. Conclusioni
• Verifica formale è essenziale per design di
applicazioni safety critical !
• La validazione deve evolvere dal
debugging alla verifica
• Il successo dipende dalle scelte di
modello/semantica/specifiche considerate:
– Hand-made models
• Sicuro successo
• Alto costo
• Legati interpretazione astratta
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
4. Conclusioni
– Modelli di specifica applicazione
• Costruiti da astrazioni automatiche
• Richiedono modello di reference e teorema di
verifica soundness
• Estremamente costosi
– Astrazioni riusabili
• Rispettano specifiche predefinite e/o definite
dall’utente
• Interpretazione astrattaimportante metodo
formale per tool automatici di supporto
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
4. Conclusioni
• Formidabile sfida nel prossimo decennio…
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
5. Bibliografia
1. Introduzione
2. Metodi Formali
3. Sfide nella verifica dell’E.S.
4. Conclusioni
5. Bibliografia
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
5. Reference
• [0] Verification of Embedded Software: Problems and Perspectives
Cousot&Cousot
• [1] J.A. Abraham. The myth of fault tolerance in complex systems,
keynote speech. In The Pacic Rim International Symposium on
Dependable Computing, PRDC'99, Hong Kong, CN. IEEE Comp.
Soc. Press, 1617 Dec. 1999.
http://www.cerc.utexas.edu/~jaa/talks/prdc-1999/.
• [2] S. Abramsky, D.M. Gabbay, and T.S.E. Maibaum, eds. Semantic
Modelling , volume 4 of Handbook of Logic in Computer Science.
Clarendon Press, 1995.
• [3] J.-R. Abrial. The B-Book. Cambridge U. Press, 1996.
• [4] R. Alur and D.L. Dill. A theory of timed automata. Theoret.
Comput. Sci. ,126(2):183235, 1994.
• [5] T. Ball and S.K. Rajamani. Bebop: A symbolic model checker for
boolean programs. In K. Havelund, J. Penix, and W. Visser, eds.,
Proc. 7th SPIN Workshop,Stanford, CA, LNCS 1885, pages 113130.
Springer-Verlag, Aug. 30 Sep. 1,2000.
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
5. Reference
•
•
•
•
•
[6] I. Beer, S. Ben-David, C. Eisner, D. Geist, L. Gluhovsky, T. Heyman, A.
Landver, P. Paanah, Y. Rodeh, G. Ronin, and Y. Wolfsthal. RuleBase: Model
checking at IBM. In O. Grumberg, editor, Proc. 9th Int. Conf. CAV '97, Haifa,
IL, LNCS 1254, pages 480483. Springer-Verlag, 2225 Jul. 1997.
[7] A.M. Ben-Amram and N.D. Jones. Computational complexity via
programming languages: constant factors do matter. Acta Informat. ,
37(2):83120, 2000.
[8] A. Benveniste, P. Le Guernic, and C. Jacquemot. Synchronous
programming with events and relations: the Signal language and its
semantics. Sci. Comput. Programming, 16(2):103149, 1991.
[9] A. Biere, A. Cimatti, E.M. Clarke, M. Fujita, and Y. Zhu. Symbolic model
checking using SAT procedures instead of BDDs. In Proc. 36th Conf. DAC
'99, New Orleans, LA, pages 317320. ACM Press, 2125 June 1999.
[10] B. Boigelot and P. Godefroid. Symbolic verication of communication
protocols with innite state spaces using QDDs (extended abstract). In R.
Alur and T.A. Henzinger, eds., Proc. 8th Int. Conf. CAV '96, New Brunswick,
NJ, LNCS 1102, pages 112. Springer-Verlag, 31 Jul. 3 Aug. 1996.
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005
Fine!!
Grazie per l’attenzione!
A. Minuto B. De Vido - Analisi e Verifica Programmi A.A.2004/2005