Verifica formale del programma nella pratica

Cercherò di dare una risposta succinta ad alcune delle tue domande.Tieni presente che questo non è strettamente il mio campo di ricerca, quindi alcune delle mie informazioni potrebbero essere obsolete / errate.

1. Esistono molti strumenti progettati specificamente per dimostrare formalmente le proprietà di Java e C ++.

   Tuttavia qui devo fare una piccola digressione: cosa significa dimostrare la correttezza di un programma? Il controllo del tipo Java dimostra una proprietà formale di un programma Java, vale a dire che alcuni errori, come laggiunta di float e int, non possono mai si verificano! Immagino che tu sia interessato a proprietà molto più forti, vale a dire che il tuo programma non può mai entrare in uno stato indesiderato o che loutput di una certa funzione è conforme a una certa specifica matematica. In breve, cè unampia sfumatura di ciò che può significare “provare un programma corretto”, da semplici proprietà di sicurezza a una prova completa che il programma soddisfa una specifica dettagliata.

   Ora presumo che sei interessato a dimostrare proprietà solide sui tuoi programmi. Se sei interessato alle proprietà di sicurezza (il tuo programma non può raggiungere un certo stato), allora in generale sembra che lapproccio migliore sia controllo del modello . Tuttavia, se desideri specificare completamente il comportamento di un programma Java, la soluzione migliore è utilizzare un linguaggio di specifica per tale lingua, ad esempio JML . Esistono linguaggi simili per specificare il comportamento dei programmi C, ad esempio ACSL , ma non so C ++.

2. Una volta che hai le tue specifiche, devi dimostrare che il programma è conforme a quella specifica.

   Per questo hai bisogno di uno strumento che abbia un comprensione formale di entrambi la tua specifica e la semantica operativa del tuo linguaggio (Java o C ++) per esprimere il teorema di adeguatezza , vale a dire che lesecuzione del programma rispetta le specifiche.

   Questo strumento dovrebbe anche consentire di formulare o generare la dimostrazione di quel teorema. Ora entrambi questi compiti (specificare e provare) sono abbastanza difficili, quindi sono spesso separati in due:

   • Uno strumento che analizza il codice, la specifica e genera il teorema di adeguatezza. Come ha detto Frank, Krakatoa è un esempio di tale strumento.

   • Uno strumento che dimostra il teorema ( s), automaticamente o in modo interattivo. Coq interagisce con Krakatoa in questo modo e ci sono alcuni potenti strumenti automatici come Z3 che possono essere utilizzati anche.

   Un punto (minore): ci sono alcuni teoremi che sono troppo difficili da dimostrare con metodi automatizzati, e si sa che i dimostratori automatici di teoremi hanno occasionalmente bug di solidità che li rendono meno affidabili. Questa è unarea in cui Coq brilla in confronto (ma non è automatico!).

3. Se vuoi generare codice Ocaml, scrivi prima in Coq (Gallina), quindi estrai il codice. Tuttavia, Coq è pessimo nel generare C ++ o Java, se è possibile.

4. Gli strumenti di cui sopra possono gestire problemi di threading e prestazioni? Probabilmente no, i problemi di prestazioni e threading vengono gestiti al meglio da strumenti appositamente progettati, poiché sono problemi particolarmente difficili. Non sono sicuro di avere strumenti da consigliare qui, anche se il progetto PolyNI di Martin Hofmann sembra interessante.

In conclusione: la verifica formale dei programmi Java e C ++ del “mondo reale” è un campo ampio e ben sviluppato, e Coq è adatto per parti di tale compito. Puoi trovare una panoramica di alto livello qui , ad esempio.

Commenti

• Grazie per questo post e per i riferimenti che hai aggiunto. Secondo me, lobiettivo per gli ingegneri del software è quello di essere in grado di rilasciare rapidamente sistemi che 1) forniranno sempre risultati corretti, 2) non falliranno mai. Ho notato un problema di regressione qui, in cui potresti voler dimostrare che la specifica stessa è ” priva di bug ” 🙂 come cercare di definire la ” vera proposizione di un linguaggio ” con un meta-linguaggio, quindi aver bisogno di un altro meta-linguaggio per quello, poi un altro uno …
• Il problema è che ciò che lutente ” vuole ” di solito non è espresso in modo formale linguaggio! In genere non esiste una risposta formale alla domanda: ” questa specifica formale è conforme alla mia idea informale? “. È ‘ possibile testare una specifica formale e dimostrare che ha determinate proprietà matematiche, ma alla fine è necessario mettere in relazione la matematica con il mondo reale, che è un processo non formale.
• Sì, certo, ho sempre realizzato che i metodi formali potevano partire solo da un punto ben definito.Se tale specifica è conforme o meno ai bisogni consci / inconsci / non scoperti degli utenti della vita reale è un altro problema, non risolvibile con metodi formali (ma certamente un problema per gli ingegneri).
• Un teorema è per definizione un proposta dimostrata. Quindi, probabilmente non intendi ” dimostrare il teorema “.
• @nbro Wikipedia sembra essere daccordo con te. Mathworld, tuttavia, definisce un teorema come una proposizione che ” può essere dimostrata essere vera mediante operazioni matematiche accettate “. In questo caso, dare prove di teoremi non solo è possibile, ma necessario per giustificare chiamarli così! 🙂 (questo è un controbilancio, ovviamente)

Vorrei menzionare tre applicazioni straordinarie di metodi formali / strumenti di verifica formale nellindustria o sistemi reali non banali. Tieni presente che ho poca esperienza su questo argomento e le imparo solo leggendo documenti.

1. Lo strumento open source Java Pathfinder (JPF in breve) rilasciato dalla NASA nel 2005 è un sistema per verificare programmi eseguibili Java bytecode (vedere Java Pathfinder @ wiki ). È stato utilizzato per rilevare incongruenze nel software esecutivo per il Rover K9 presso la NASA Ames.

2. Questo documento: Utilizzo del controllo del modello per trovare gravi errori del file system @ OSDI “04 mostra come utilizzare controllo del modello per rilevare errori gravi nei file system. Un sistema chiamato FiSC viene applicato a tre file system ampiamente utilizzati e ampiamente testati: ext3, JFS e ReiserFS e sono stati rilevati 32 bug gravi. Ha vinto il Best Paper Award.

3. Questo documento: How Amazon Web Services Uses Formal Methods @ CACM “15 descrive come AWS applica metodi formali a i suoi prodotti come S3, DynamoDB, EBS e Internal Distributed Lock Manager. Si concentra sullo strumento Lamport “TLA + . A proposito, Lamport ha utilizzato intensamente il suo toolbox TLA. Spesso fornisce una verifica formale (abbastanza completa) in TLA degli algoritmi / teoremi proposti da lui stesso (così come dai coautori) nelle appendici agli articoli.

La verifica formale è ora possibile per i programmi scritti in un sottoinsieme di C ++ progettato per sistemi integrati critici per la sicurezza. Vedi http://eschertech.com/papers/CanCPlusPlusBeMadeAsSafeAsSpark.ppt per una breve presentazione e http://eschertech.com/papers/CanCPlusPlusBeMadeAsSafeAsSpark.pdf per lintero documento.

Commenti

• Grazie per i link. Almeno una breve panoramica del loro contenuto sarebbe utile, per proteggersi dal link rot, soprattutto perché i tuoi link sono a un sito web aziendale: quelli tendono a essere periodicamente riorganizzati, eliminando tutti i link nel sito.

Un formale la specifica di un programma è (più o meno) un programma scritto in un altro linguaggio di programmazione. Di conseguenza, la specifica includerà sicuramente i suoi bug.

Il vantaggio della verifica formale è che, poiché il programma e la specifica sono due implementazioni separate, i loro bug saranno diversi. Ma non sempre: una comune fonte di bug, casi trascurati, spesso corrisponderà. Pertanto, la verifica formale non è una panacea: può comunque perdere un numero non banale di bug.

Uno svantaggio della verifica formale è che può imporre qualcosa come il doppio del costo di implementazione, probabilmente di più (è necessario uno specialista in specifiche formali, e devi utilizzare gli strumenti più o meno sperimentali che ne derivano; non sarà economico).

Immagino che la creazione di casi di test e scaffolding per eseguirli automaticamente sarebbe un uso migliore del tuo tempo.

Commenti

• Il vantaggio della verifica formale è che … Un secondo svantaggio della verifica formale è che … Questo crea confusione.
• Penso che la mancata corrispondenza tra specifica e attività informale sia un problema di analisi dei requisiti software, non un problema di programmazione.

Poni alcune domande diverse. Sono daccordo che sembra che i metodi di verifica formale per applicazioni industriali / commerciali non siano così comuni. si dovrebbe tuttavia rendersi conto che molti principi di “verifica formale” sono incorporati nei compilatori per determinare la correttezza del programma! quindi in un certo senso, se utilizzi un compilatore moderno, stai utilizzando gran parte dello stato dellarte nella verifica formale.

Dici “Sono stanco di testare” ma verifica formale non è davvero un sostituto per il test. in un certo senso è una variazione dei test.

Parli di Java.ci sono molti metodi avanzati di verifica formale incorporati in un programma di verifica java chiamato FindBugs che in effetti può essere eseguito su basi di codice di grandi dimensioni. Si noti che verranno visualizzati “falsi positivi e falsi negativi” e i risultati devono essere rivisti / analizzati da uno sviluppatore umano. Ma nota anche se non mostra veri difetti funzionali, generalmente mostra “antipattern” che dovrebbero essere comunque evitati nel codice.

Non fai più menzione della tua particolare applicazione se non “industriale” . La verifica formale in pratica tende a dipendere dalla particolare applicazione.

Le tecniche di verifica formale sembrano essere ampiamente utilizzate in EE per dimostrare la correttezza del circuito, ad es. nella progettazione di un microprocessore.

Di seguito è riportato un esempio di unindagine sugli strumenti di verifica formale nel campo EE di Lars Philipson .

Commenti

• ‘ è fuorviante dire che ” a molti dei principi della ” verifica formale ” sono incorporati nei compilatori per determinare la correttezza del programma “. Quello a cui ti riferisci è il controllo statico del tipo che fanno alcuni compilatori, ma le proprietà verificate in questo modo sono piuttosto semplici, ad es. evitando di aggiungere un numero e una stringa. Ciò è utile, ma molto diverso da ciò che di solito viene ignorato dalla ” verifica formale “.
• non lha fatto fare riferimento specificamente al controllo del tipo statico, sebbene questo sia un esempio semplice / comune. Le tecniche di ottimizzazione del compilatore imho, che sono diffuse e avanzate, sono più o meno simili ai principi di verifica formale, perché implicano tecniche avanzate per determinare / mostrare lequivalenza di varianti di programma ottimizzate. quindi sembra che sia importante evitare il problema di ” spostando i pali della porta ” e non presumere che semplicemente perché un compilatore lo fa o è costruito nel compilatore, non è una verifica formale.
• ha convenuto che questa non è unintesa comune. le tecniche di ottimizzazione sono più o meno la creazione di un modello di comportamento del programma, ad esempio di un ciclo o una subroutine, e lottimizzazione di quel modello, e quindi la generazione di nuovo codice che è provabilmente equivalente. quindi alcune di queste ottimizzazioni sono piuttosto sofisticate nel riorganizzare il codice & per me fanno uso di principi di verifica formale. sembrano esserci molti altri esempi di metodi di verifica formale nel compilatore … la domanda originale poneva molte domande diverse come molti hanno notato, non sto tentando di rispondere a tutte le domande in essa contenute.
• dal in questo modo sembrano esserci alcuni principi di verifica formale utilizzati anche in JRE, java runtime engine, ad es. ottimizzazione dinamica, ecc …
• che è ” il sogno di una verifica formale ” a cui fa riferimento il filmus sopra, imho unastrazione chimerica, e lindustria pragmatica / utilitaristica / realistica la riconosce ampiamente come tale. è noto da decenni che basi di codice di grandi dimensioni hanno intrinsecamente $ x $ bug / difetti per $ y $ K-righe di codice e questo non cambierà mai, non importa quanto la teoria / tecnologia avanzi, è un fatto di atura umana . e infatti i teoremi matematici creati dalluomo hanno le stesse proprietà, anche se questo non è molto apprezzato!

Forse, un controllo del modello potrebbe essere utile.

http://alloytools.org/documentation.html Alloy è un controllo del modello .

Una bella presentazione che spiega il concetto di controllo del modello utilizzando Alloy: https://www.youtube.com/watch?v=FvNRlE4E9QQ

Nella stessa famiglia di strumenti arriva il “test basato sulla proprietà”, tutti cercano di trovare un controesempio per il dato modello di specifica del tuo software.