Metodi formali nel software
a.a.2013/2014
Prof.Anna Labella
12/21/2015
1
Cos’è l’informatica?
Tra analitico a priori (matematica)
 e sintetico a posteriori (scienze della
natura) . . .
 Dove collochiamo l'informatica?
Gilles Dowek (2013): informatica scienza
analitica a posteriori.

12/21/2015
2
Dal mondo dell’industria
Research in Software Engineering (RiSE)
Microsoft's Research in Software Engineering in Redmond,
USA.
“Our mission is to advance the state of the art in SE,
to bring those advances to Microsoft’s business,
and to take care of those SE technologies that
are critical to the company,
but not inherently linked to particular products.”
Logic is the calculus of computation
Amir Pnueli.
RiSE understands the importance of logic and
builds powerful inference engines that
help understand complex systems.▪
Tools: Z3 ...
Projects: DKAL LAI L&F M3
12/21/2015
3
Questo insegnamento prevede
un'introduzione ai metodi formali per la specifica,
sviluppo e verifica di software
si propone di introdurre le principali metodologie formali,
e mostrare come queste vengano applicate
nel ciclo di vita del software
Libro di testo: non c’è un vero libro di testo;
tutte le lezioni saranno a disposizione
indicazioni verranno date per i singoli argomenti
Una linea di svolgimento si può trovare su
Understanding formal methods J.-F. Monin Springer, ©2003
Ma è molto più utile
4
12/21/2015
Logic in Computer Science Huth Ryan (2° edizione)
•necessità di una formalizzazione dei requisiti
per la produzione del software,
•il problema della formalizzazione,
comunque necessaria per produrre software:
•tradurre requisiti espressi nel linguaggio
corrente ed in forma vaga a
condizioni per lo sviluppo del software
12/21/2015
5
• il problema di produrre un software
sicuro nel senso dell'assoluta
affidabilità:
• esempi di situazioni critiche
• economia della formalizzazione
12/21/2015
6
•da un linguaggio semi-formale e
sostanzialmente grafico: statecharts e UML
•ad uno formale per “parlarne”.
•Poi bisogna scegliere il tipo di linguaggio
con il quale conviene programmare
ed in base a questo, cioè alle sue primitive
•farne un modello matematico.
12/21/2015
7
Oltre la formalizzazione, un metodo di prova
.
12/21/2015
8
cos’è un metodo?

Qualcosa che dà i mezzi per
raggiungere un certo scopo

Esempio: la fisica

In informatica siamo ancora indietro
12/21/2015
9
Un esempio di metodo formale in azione: I compilatori
Un compilatore è un programma (o un insieme di programmi)
che trasforma il codice sorgente (scritto in un certo linguaggio
di programmazione)
in un altro linguaggio creando un programma eseguibile
Un compilatore di solito esegue le seguenti operazioni:
Analisi lessicale, preprocessing, parsing, analisi semantica,
generazione del codice, ottimizzazione del codice.
Il contesto matematico? La teoria dei linguaggi formali
12/21/2015
10
Siamo a livello di metalinguaggio

A cosa porta l’uso di metodi formali?
12/21/2015
11
Introduzione di nuovi concetti

Ciclo di vita del software

Valutazione dei costi delle diverse fasi

Valutazione del costo degli errori di
progettazione
12/21/2015
12
Prevenzione degli errori

Gli errori non sono soltanto costosi e
difficili da correggere

Si possono dare situazioni critiche
12/21/2015
13
Il primo volo dell'Ariane 5 (Ariane 5 volo 501)
svoltosi il 4 giugno 1996 fallì e il razzo si autodistrusse
dopo 40 secondi dal lancio per via di un malfunzionamento
del software di controllo, creato da uno dei più famosi
bug della storia. Un dato a 64 bit in virgola mobile,
probabilmente quello della pressione, venne convertito
in un intero a 16 bit con segno, questa operazione causò una
trap del processore (operazione errata): il numero in virgola
mobile era troppo grande per poter essere rappresentato
con un intero a 16 bit. Motivi di efficienza avevano
spinto i progettisti a disabilitare il controllo software
(scritto in Ada) sulle trap, anche se altre conversioni
simili nel codice erano corrette. Questo errore scatenò
una reazione a catena che causò poi la deviazione
distruttiva del razzo a causa delle enormi forze aerodinamiche.
Fu necessario quasi un anno e mezzo per capire
quale fosse stato il malfunzionamento che aveva portato
14
12/21/2015
alla distruzione del razzo.
Perché usare la formalizzazione?
A livello di specifica dei requisiti serve a
capire quali siano effettivamente i
bisogni e
 a controllare la validità di certe proprietà
che si richiedono (prototipazione
veloce)

12/21/2015
15
Un linguaggio di specifica deve:

Essere formale

Basato su una teoria matematica (semantica)

Consentire dimostrazioni di proprietà

Permettere lo sviluppo di tools di supporto
12/21/2015
16
Vantaggi

La verifica delle proprietà da soddisfare
viene fatta a priori

Non si tratta di un test per casi, ma di

una prova fornita insieme al software
prodotto
12/21/2015
17
Difficoltà
Rigidità di una qualunque
formalizzazione, soprattutto nei casi
complessi
 Acquisizione di un nuovo “linguaggio”


Lentezza iniziale
12/21/2015
18
Una panoramica

Una teoria
Sistemi di transizione
Teoria degli insiemi
Algebra universale
Lambda-calcolo, ecc.
 Un campo di applicazione
Data processing
Sistemi real-time
Protocolli, ecc.
 Una comunità di utilizzo
12/21/2015
19
Metodi specifici e metodi
generali

Modellare i singoli aspetti del sistema
software: architetture, interfacce,
comportamenti visibili, algoritmi…

Fornire un contesto matematico: si
rinviano le scelte, ma spesso si è poco
“metodologici”
12/21/2015
20
La nozione di “stato”

Stati espliciti

Stati impliciti
12/21/2015
21
Specifica e verifica

Ci occuperemo soprattutto di specifica

Rinviando la verifica ad un altro
insegnamento

Ma tenendo conto delle due
12/21/2015
22
Grande varietà di teorie
matematiche
Metodi algebrici (semantica
denotazionale: i termini sono oggetti
algebrici)
 Metodi logici: si studiano proprietà


Processi (semantica operazionale:
metafora della macchina astratta)
12/21/2015
23
Programma
Logiche temporali e Model checking
 Logica di Hoare e verifica di programmi
 Sistemi reattivi e logica di HennessyMilner
 Strutture d’ordine e semantica
denotazionale

12/21/2015
24
…..esame
Un progetto in collaborazione e un
colloquio orale su una parte del
programma, oppure
 Un colloquio orale su tutto il programma
 Il colloquio su una parte del programma
è alternativo ad una prova intermedia
scritta

12/21/2015
25