Infinite-state Verification e Link con EOS
Giorgio Delzanno
Verification

Goal
Aumentare qualita’, affidabilita e sicurezza e ridurre costi
nello sviluppo di software, sistemi distribuiti e protocolli

Metodo
Dimostrare formalmente che l’implementazione di un
sistema soddisfa le specifiche funzionali definite nella fase
di design
Considerazioni

Quando applicare un metodo di verifica?


Durante sviluppo del sistema lavorando su un modello
dell’implementazione
A sviluppo ultimato:



Si applica al modello concettuale di un sistema (es. algoritmo in
pseudo codice, descrizione informale di un protocollo)
Si estrae (in modo manuale o automatico) un modello
dall’implementazione (es. macchina a stati finiti da codice C)
Verification vs Simulation


Verification = provare formalmente correttezza di un modello
Simulation = cercare errori generando test cases
Computer-aided Automated Verification

Goal
Automatizzare la fase di verifica di un sistema software
(progettare programmi che verificano altri programmi)

Metodo
Algoritmi, strutture dati e tecniche di astrazione per
estrarre un modello dall’implementazione
e per verificare proprieta’ funzionali del modello
Modelli e Proprieta’

Modelli :





Automi a stati finiti
Reti di Petri
Logica del I ordine o logica superiore
Semantica operazionale e denotazionale …..
Proprieta’




Insiemi di stati
Insiemi di configurazioni di una rete di Petri
Formule logiche (es. logica temporale)
Asserzioni ad hoc (es. a la Hoare) ….
Tecniche

Theorem Proving




Semi-automatico
Per modelli e proprieta’ molto generali (es. logica del
prim’ordine, ordine superiore)
Uso complicato e limitato ad esperti
Model Checking




Push button technology
Modelli con spazio degli stati finito
Proprieta’ in logica temporale
Possibile integrazione in altri tool di analisi
Ricerca svolta in questi anni

Estensione delle tecniche di model checking a sistemi con
spazio degli stati potenzialmente infinito



Analisi delle proprieta’ computazionali di modelli infinite-state
Algoritmi simbolici per l’analisi e verifica funzionale
Aumentare l’espressivita’ dei modelli trattati permette di
ridurre l’incidenza delle tecniche di astrazione (spesso
applicate manualmente)
Tecniche

Modelli infinite-state


Rappresentazione simbolica di insiemi di configurazioni


Programmi logici/riscrittura con vincoli, reti di Petri colorate,
process calculi (pi-calculus, mobile ambient)
Con vincoli aritmetici, automi, ed espressioni regolari
Esplorazione dello spazio degli stati di un modello


Calcolo simbolico di punto fisso
Terminazione basata su particolari ordinamenti


well-quasi ordering (vettori, stringhe, bags, trees, graphs)
Astrazioni ed euristiche per terminazione

widening, approssimazioni, ...
Risultati e applicazioni


Risultati di decidibilita e algoritmi di verifica
per l’analisi automatica di sistemi concorrenti parametrici
nel numero di componenti
Applicazione a




Protocolli di cache coherence
Modelli di programmi C e Java multithreaded
Protocolli crittografici multi-sessione
Alg. concorrenti e distribuiti per N processi


Es. bakery, szymanski, ricart-agrawala
Mobile ambients, membrane computing, molecular biology
(Kappa)
Towards Verification of Multithreaded Java Programs
[Tacas 2001]



Modellazione (manuale) di programmi Java (flattened)
tramite famiglia di automi finiti con operazioni di
comunicazione che modellano wait/notify/notify_all
Astrazione dei modelli con estensioni di reti di Petri
(es. transfer arc, rendez-vous non bloccante)
Algoritmo di analisi


backward reachability per safety properties (mutua esclusione)
con strutture dati dedicate (sort of BDD per memorizzare
insiemi di marking)
static analysis (marking equation=linear integer programming)
Progetti e collaborazioni

Progetti PRIN




“CoVer”: Constraint-based Verification (Gabbrielli)
“AIDA’’: Abstract Interpretation (Giacobazzi)
“Vincoli e preferenze” (F. Rossi)
Collaborazioni





Parosh Abdulla (Uppsala University)
Ahmed Rezine (Liafa, Paris VII)
Javier Esparza (TUM)
Andreas Podelski (Un. Freiburg)
Jean-Francois Raskin (U. Bruxelles)
Direzioni future e possibili link con EOS
Verified Software Initiative (Hoare et al.)
Combinare formal verification e program analysis sullo
stile di tool quali SLAM (Microsoft) e BLAST (Berkeley)
usati per testare driver scritti in C
Es. SLAM=CFL reachability con BDD + predicate
abstraction
Possibili punti da esplorare

Analisi programmi object-oriented multithreaded (es.
Concurrent Java)

Estrazione di modelli infinite-state da instrumented
code
(specifiche di linguaggi Java-like?)

Astrazioni + infinite-state model checking

Abstraction refinement
Keywords (catturate stamane ...)





Reti di Petri (object/nested nets ~ reflective nets?)
Logiche (temporali?) per verifica
Calcoli a processi/oggetti
Tipi comportamentali  Modelli infinite-state (CCS/Reti
di Petri)
Calcoli per systems biology