Se hai appreso metodi formali per il software, quanto ti è stato utile trovarlo?

Assolutamente inutile per qualsiasi cosa non banale.

Ho avuto un corso chiamato, appropriatamente, "Formal Methods" che si concentra su Alloy- Non posso assolutamente vederlo da nessuna parte. Aveva un'altra classe che si concentrava sulla modellazione della concorrenza con LTSA - ugualmente inutile.

Il problema è che la maggior parte dei bug e dei problemi nel software (almeno nella mia esperienza) derivano dalla complessità che si verifica al di sotto del livello di astrazione di tali strumenti.

Ho uno sfondo in CSP (Communicating Sequential Processes). Non per trombare il mio corno ma ho scritto la tesi del mio Master su Timed CSP, in particolare "compilando" le specifiche scritte in metodi formali in C ++ eseguibile. Posso dire di avere qualche esperienza con i metodi formali. Una volta che ho completato la mia laurea e ho ottenuto un lavoro nel settore, non ho usato affatto metodi formali. I metodi formali sono ancora troppo teorici per essere applicati nel settore. I metodi formali hanno trovato alcune applicazioni pratiche nell'area dei sistemi embedded. Ad esempio, la NASA utilizza metodi formali nei loro progetti. Vorrei ipotizzare che i metodi formali siano ben lontani dall'essere largamente adottati nel settore. Semplicemente non ha senso scrivere le specifiche del software in metodi formali e quindi "interpretarle" secondo il proprio schema di scelta. L'inglese normale e gli schemi funzionano meglio per questo, mentre i test di unità e integrazione hanno svolto un ottimo lavoro di "verifica" della correttezza del codice. Penso che i metodi formali rimarranno per qualche tempo nel mondo accademico .

Ho letto alcuni libri sui metodi formali e ne ho applicati alcuni. La mia reazione immediata fu: "Accidenti, questi libri mi dicono come essere un buon programmatore, purché sia un perfetto matematico". Un altro punto debole è che puoi dimostrare l'equivalenza solo con un'altra descrizione formale. Scrivere una specifica formale per un programma equivale a scrivere un programma in un linguaggio di livello superiore, e non c'è modo di evitare di introdurre bug in una specifica abbastanza ampia.

Non ho mai reso i metodi formali funzionanti su larga scala. Possono essere utili per ottenere qualcosa di piccolo e difficile, e per convincermi che sono corretti. In questo modo, posso lavorare con blocchi di costruzione leggermente più grandi e talvolta ottenere un po 'di più.

Una cosa che ho raccolto è più generalmente utile è il concetto di invariante, una dichiarazione su un programma e il suo stato che è sempre vero. Tutto ciò che puoi ragionare è buono.

Come accennato sopra, non sono un matematico perfetto, e quindi le mie dimostrazioni a volte contengono errori. Tuttavia, nella mia esperienza questi tendono ad essere grandi errori stupidi facili da individuare e risolvere.

Ho seguito un corso di specializzazione in analisi di programmi formali, in cui ci siamo concentrati sulla semantica operativa. Ho fatto il mio ultimo lavoro sullo sforzo di seL4, rivedendo i metodi formali che hanno usato. Il mio principale take-away in termini di praticità è che è di valore marginale. Non solo devi scrivere il programma, devi scrivere la prova. Wow. Due fonti di bug. Non solo uno. Inoltre, c'era un'enorme quantità di restrizioni applicate al codice reale. È molto difficile descrivere formalmente un computer fisico, incluso I / O.

L'autodidatta TLA + dello scorso anno, lo uso da allora. È uno dei primi strumenti che raggiungo ogni volta che avvio un progetto. L'errore commesso dalla maggior parte delle persone è che presuppongono che i metodi formali siano una cosa "tutto o niente": o non stai usando metodi formali o hai una verifica completa. Tuttavia, c'è qualcosa tra loro: specifica formale , in cui controlli che una specifica astratta del tuo progetto non infrange i tuoi invarianti. A differenza della verifica, le specifiche sono abbastanza pratiche da poter essere utilizzate nell'industria.

Le lingue delle specifiche sono più espressive dei linguaggi di programmazione. Ad esempio, ecco una (molto) semplice specifica PlusCal per un archivio dati distribuito:

process node \in 1..5 \* Nodes
variables online = TRUE,
          stored \in SUBSET data; \* Some set
begin 
  Transfer:
    either
      with node \in Nodes, datum \in stored do
        node.stored := node.stored \union {datum};
      end
    or \* crash
      online := FALSE;
    end either;
end process;

Questo snippet specifica cinque nodi in esecuzione simultanea, eseguendo i trasferimenti in un ordine arbitrario, in cui ogni trasferimento è una parte arbitraria di dati su un nodo arbitrario. Inoltre, abbiamo specificato che qualsiasi trasferimento potrebbe non riuscire e causare il blocco del nodo. E possiamo simulare tutti questi comportamenti nel correttore del modello TLA +! In questo modo possiamo testare che indipendentemente dall'ordine, dai tassi di fallimento, ecc., I nostri requisiti rimangono validi. A proposito, aggiungiamo un paio di requisiti. Innanzitutto, non trasferiamo mai dati su un nodo offline:

[][\A node \in Nodes: ~online => UNCHANGED node.stored]_vars

Nella nostra versione semplificata, il controllore del modello troverà uno stato di errore. Possiamo anche specificare "qualsiasi dato di dati è in almeno un nodo online":

\A d \in data: \E n \in Nodes: n.online /\ d \in n.stored

Che fallirà anche. Buona fortuna controllandoli con un test unitario!

Il limite principale della specifica è che esiste indipendentemente dal tuo codice reale. Può solo dirti che il tuo design è corretto, non che lo hai implementato correttamente. Ma è più veloce da specificare che verificare e cattura i bug che sono troppo sottili per essere testati, quindi trovo che valga la pena. Praticamente qualsiasi codice che coinvolga la concorrenza o più sistemi è un buon posto per una specifica formale.

I diagrammi di stato e le reti di Petri sono utili per la modellazione e l'analisi di protocolli e sistemi realtime. Prima aiutano a progettare una soluzione. In secondo luogo, aiutano a trovare casi di test per software eccitanti in situazioni molto specifiche.

Ero solito lavorare in un dipartimento di ICL, prima che fossero acquistati da Fujitsu. Avevano alcuni grandi contratti di tipo governativo che richiedevano prova che il software funzionasse come pubblicizzato, così hanno costruito una macchina che avrebbe preso le specifiche formali scritte in Z e convalidato il codice mentre correva, con una grande luce verde o rossa per passare / fallire.

È stata una cosa fantastica, ma come sottolinea stimato @FishToaster , era inutile per qualsiasi cosa non banale.