I metodi formali di verifica del programma hanno un posto nell'industria?

Question

Ho dato un'occhiata a Hoare Logic al college. Quello che abbiamo fatto è stato davvero semplice. La maggior parte di ciò che ho fatto è stata la dimostrazione della correttezza dei programmi semplici costituiti dai loop while, dalle istruzioni if e dalla sequenza di istruzioni, ma niente di più. Questi metodi sembrano molto utili!

I metodi formali sono ampiamente utilizzati nell'industria?

Questi metodi sono utilizzati per dimostrare il software mission-critical?

Answer 1

Questa è una domanda vicino al mio cuore (sono un ricercatore in Software Verification utilizzando le logiche formali), quindi probabilmente non sarai sorpreso quando dico che penso che queste tecniche abbiano un posto utile, e non sono ancora usato abbastanza nel settore.

Esistono molti livelli di "metodi formali", quindi suppongo che intendiate quelli che poggiano su una base matematica rigorosa (al contrario, per esempio, seguendo un processo in stile 6-Sigma). Alcuni tipi di metodi formali hanno avuto un grande successo - i sistemi di tipo sono un esempio. Anche gli strumenti di analisi statica basati sull'analisi del flusso di dati sono popolari, il model checking è quasi onnipresente nella progettazione dell'hardware e modelli computazionali come Pi-Calculus e CCS sembrano ispirare alcuni reali cambiamenti nella progettazione del linguaggio pratico per la concorrenza. L'analisi della terminologia è stata recentemente oggetto di molta stampa: il progetto SDV di Microsoft e il lavoro di Byron Cook sono esempi recenti di crossover di ricerca/pratica in metodi formali.

Hoare Il ragionamento non ha fatto grandi progressi nel settore - questo è per più motivi di quanti ne possa elencare, ma sospetto che sia per lo più intorno alla complessità della scrittura e quindi alla dimostrazione di specifiche per programmi reali (tendono ad essere grande e non riescono a esprimere le proprietà di molti ambienti del mondo reale). Diversi sotto-campi in questo tipo di ragionamento stanno ora facendo grandi progressi in questi problemi - Separation Logic essendo uno.

Questa è parzialmente la natura della ricerca (difficile) in corso. Ma devo confessare che noi, come teorici, non abbiamo completamente educato il settore a spiegare perché le nostre tecniche sono utili, per tenerle pertinenti alle esigenze del settore e renderle accessibili agli sviluppatori di software. A un certo livello, non è questo il nostro problema: siamo ricercatori, spesso matematici, e l'uso pratico non è il massimo nelle nostre menti. Inoltre, le tecniche sviluppate sono spesso troppo embrionali per l'uso in sistemi su larga scala: lavoriamo su piccoli programmi, su sistemi semplificati, facciamo lavorare la matematica e andiamo avanti. Non comprando molto queste scuse però - dovremmo essere più attivi nel promuovere le nostre idee e ottenere un circuito di feedback tra l'industria e il nostro lavoro (uno dei motivi principali per cui sono tornato alla ricerca).

E 'probabilmente una buona idea per me di far risorgere il mio weblog, e fare qualche più post su questa roba ...

Answer 2

"I metodi formali sono utilizzati nell'industria?"

Sì.

L'istruzione assert in molti linguaggi di programmazione è legata ai metodi formali per la verifica di un programma.

"I metodi formali sono ampiamente utilizzati nell'industria?"

No.

"Sono questi i metodi usati per dimostrare il software mission-critical?"

A volte. Più spesso, sono utilizzati per dimostrare che il software è sicuro. Più formalmente, vengono utilizzati per provare alcune asserzioni relative alla sicurezza del software.

Answer 3

Bene, Sir Tony Hoare è entrato in Microsoft Research circa 10 anni fa e una delle cose che ha iniziato è stata una verifica formale del kernel di Windows NT. In effetti, questo è stato uno dei motivi del lungo ritardo di Windows Vista: a partire da Vista, ampie parti del kernel sono effettivamente verificate formalmente wrt. a certe proprietà come assenza di deadlock, assenza di perdite di informazioni ecc.

Questo non è certamente tipico, ma è probabilmente l'unica applicazione più importante della verifica formale del programma, in termini di impatto (dopo tutto, quasi ogni umano l'essere è in qualche modo, forma o forma influenzata da un computer che esegue Windows).

Answer 4

Sì, sono utilizzati, ma non ampiamente in tutte le aree. Esistono più metodi oltre alla logica Hoare, alcuni sono usati più, altri meno, a seconda dell'idoneità per un determinato compito. Il problema comune è che il software è biiiiiiig e verificare che tutto sia corretto è ancora un problema troppo difficile.

Ad esempio il dimostratore di teoremi (un software che aiuta l'uomo a dimostrare la correttezza del programma) ACL2 è stato utilizzato per dimostrare che una determinata unità di elaborazione a virgola mobile non ha un determinato tipo di errore. È stato un compito importante, quindi questa tecnica non è troppo comune.

Il controllo del modello, un altro tipo di verifica formale, viene utilizzato piuttosto ampiamente al giorno d'oggi, ad esempio Microsoft fornisce un tipo di controllo del modello nel kit di sviluppo del driver e può essere utilizzato per verificare il driver per una serie di errori comuni. I correttori di modello vengono spesso utilizzati anche per verificare i circuiti hardware.

Test rigorosi possono anche essere considerati come verifica formale: esistono alcune specifiche formali su quali percorsi del programma devono essere testati e così via.

Answer 5

Polyspace è un prodotto commerciale a (terribilmente costoso, ma molto buono) basata sulla verifica del programma. È piuttosto pragmatico, in quanto si riduce a "un collaudo dell'unità potenziato che probabilmente troverà alcuni bug" per i prossimi tre anni della tua vita che saranno spesi mostrando che questi 10 file hanno zero difetti ".

Si basa più sulla verifica negativa ("questo programma non corromperà il tuo stack") che sulla verifica positiva ("questo programma farà esattamente quello che queste 50 pagine di equazioni dicono che lo farà").

Answer 6

Non posso commentare molto sul software mission-critical, anche se so che l'industria avionica utilizza un'ampia varietà di tecniche per convalidare il software, inclusi i metodi in stile Hoare.

I metodi formali hanno sofferto perché i primi sostenitori come Edsger Dijkstra hanno insistito sul fatto che dovrebbero essere usati ovunque. Né i formalismi né il supporto software erano all'altezza del lavoro. I sostenitori più ragionevoli credono che questi metodi dovrebbero essere usati su problemi che sono difficili. Non sono ampiamente utilizzati nell'industria, ma l'adozione è in aumento. Probabilmente le più grandi conquiste sono state nell'uso dei metodi formali per controllare le proprietà di sicurezza del software. Alcuni dei miei esempi preferiti sono il correttore del modello SPIN e il codice di prova di George Necula.

Allontanandosi dalla pratica e nella ricerca, il progetto del sistema operativo Microsoft Singularity riguarda l'utilizzo di metodi formali per fornire garanzie di sicurezza che normalmente richiedono il supporto hardware. Questo a sua volta porta a prestazioni più veloci e garanzie più forti.Ad esempio, in singolarità hanno dimostrato che se un driver di dispositivo di terze parti è consentito nel sistema (il che significa che sono state dimostrate le condizioni di verifica di base), allora non è possibile abbattere l'intero sistema operativo – che il peggio che può fare è proprio dispositivo.

I metodi formali non sono ancora ampiamente utilizzati nell'industria, ma sono più utilizzati di quanto non fossero 20 anni fa, e tra 20 anni saranno ancora più ampiamente utilizzati. Quindi sei a prova di futuro :-)

Answer 7

Per aggiungere a Jorg answer, ecco uno interview con Tony Hoare. Gli strumenti a cui Jorg si riferisce, credo, sono PREfast e PREfix. Vedere here per ulteriori informazioni.

Answer 8

Esistono due approcci diversi ai metodi formali nel settore.

Un approccio è modificare completamente il processo di sviluppo. La notazione Z e il metodo B menzionati sono in questa prima categoria. B è stato applicato allo sviluppo della linea 14 della metropolitana senza conducente a Parigi (se ne hai la possibilità, sali sul carro anteriore.) Non è frequente che tu abbia la possibilità di vedere i binari davanti a te).

Un altro approccio, più incrementale, è conservare i processi di sviluppo e verifica esistenti e sostituire solo una delle attività di verifica alla volta con un nuovo metodo. Questo è molto interessante, ma significa sviluppare strumenti di analisi statica per linguaggi obsoleti e usati che spesso non sono facili da analizzare (perché non erano progettati per essere). Se andate a (per esempio)

http://dblp.uni-trier.de/db/indices/a-tree/d/Delmas:David.html

(spiacente, solo un collegamento ipertestuale permesso per i nuovi utenti :()

troverete esempi di applicazioni pratiche di metodi formali per la verifica della C programmi (con analizzatori statici Astrée, Caveat, Fluctuat, Frama-C) e codice binario (con strumenti di AbsInt GmbH)

A proposito, dal momento che hai menzionato Hoare Logic, nella lista sopra di strumenti, solo Caveat è basato sulla logica Hoare (e Frama-C ha un plug-in di logica Hoare). Gli altri r ely sull'interpretazione astratta, una tecnica diversa con un approccio più automatico.

Answer 9

Oltre di altri approcci più procedurali, la logica Hoare era nella base di Design by Contract, introdotto come una tecnica orientato agli oggetti da Bertrand Meyer in Eiffel (see Meyer's article of 1992, pagina 4). Mentre Design by Contract non è lo stesso dei metodi di verifica formale (per una cosa, DbC non produce nulla fino al momento dell'esecuzione del software), a mio parere fornisce un uso più pratico.

Answer 10

La mia area di competenza è l'uso di metodi formali per l'analisi del codice statico per dimostrare che il software è privo di errori di runtime. Questo è implementato utilizzando una tecnica di metodi formali nota come "interpretazione astratta". La tecnica essenzialmente ti permette di provare certi attributi di un programma s/w. Per esempio. dimostrare che a + b non sarà overflow o x/(x-y) non determinerà una divisione per zero. Un esempio di strumento di analisi statica che utilizza questa tecnica è Polyspace.

Rispetto alla tua domanda: "I metodi formali sono ampiamente utilizzati nell'industria?" e "Questi metodi sono utilizzati per dimostrare il software mission-critical?"

La risposta è sì.Questo parere si basa sulla mia esperienza e sul supporto dello strumento Polyspace per le industrie che si basano sull'uso di software embedded per controllare sistemi critici di sicurezza quali acceleratore elettronico in un'automobile, sistema di frenatura per un treno, controller per motori a getto, pompa di infusione per somministrazione di farmaci, ecc. Queste industrie usano effettivamente questi tipi di strumenti dei metodi formali.

Non credo che il 100% di questi segmenti del settore stia utilizzando questi strumenti, ma l'utilizzo è in aumento. La mia opinione è che le industrie aerospaziale e automobilistica conducono con l'industria dei dispositivi medici che sta rapidamente aumentando l'uso.