Qual è la tua esperienza con il controllo del modello software?[Chiuso]

Question

• Che tipi di applicazioni hai utilizzato verifica del modello per?
• Quale strumento di controllo del modello hai utilizzato?
• Come riassumeresti la tua esperienza con la tecnica, in particolare nel valutare la sua efficacia nel fornire software di qualità superiore?

Nel corso dei miei studi, ho avuto la possibilità di utilizzare Rotazione, e ha suscitato la mia curiosità riguardo all'entità effettiva del model testing e al valore che le organizzazioni ne traggono.Nella mia esperienza lavorativa, ho lavorato su applicazioni aziendali, dove (naturalmente) non viene presa in considerazione l'applicazione della verifica formale alla logica.Mi piacerebbe davvero conoscere l'esperienza di controllo del modello della gente di SO e i pensieri sull'argomento.Il model check diventerà mai una pratica di sviluppo più ampiamente utilizzata che dovremmo avere nel nostro toolkit?

Answer 1

Ho appena finito un corso sul controllo del modello e sui grandi strumenti che abbiamo utilizzato Rotazione E SMV.Alla fine li abbiamo utilizzati per verificare le proprietà sui problemi comuni di sincronizzazione e ho trovato SMV leggermente più semplice da usare.

Sebbene questi strumenti siano divertenti da usare, penso che brillino davvero quando li combini con qualcosa che impone dinamicamente vincoli al tuo programma (in modo che sia un po' più facile verificare cose "utili" sul tuo programma).Alla fine abbiamo preso il Framework WebFlow primaverile, che utilizza XML per scrivere un file simile a una macchina a stati che specifica quali pagine Web possono passare a quali altre e utilizza SMV per poter eseguire la verifica su tali applicazioni (spina spudorata qui).

Per rispondere alla tua ultima domanda, penso che il controllo del modello sia sicuramente utile, ma sono più propenso a utilizzare il test unitario come una tecnica che mi fa sentire a mio agio nel fornire il mio prodotto finale.

Answer 2

Abbiamo utilizzato diversi modelli di controllo nell'insegnamento, nella progettazione e nello sviluppo di sistemi.La nostra cassetta degli attrezzi include SPIN, UPPAL, Java Pathfinder, PVS e Bogor.Ognuno ha i suoi punti di forza e di debolezza.Tutti trovano problemi con modelli che sono semplicemente impossibili da scoprire per gli esseri umani.La loro usabilità varia, sebbene la maggior parte sia automatizzata tramite pulsante.

Quando utilizzare un controllo modello?Direi ogni volta che descrivi un modello che deve avere (o non avere) proprietà particolari ed è più grande di una manciata di concetti.Chiunque pensi di poter descrivere e comprendere qualcosa di più grande o più complesso si inganna.

Answer 3

Per quali tipi di applicazioni hai utilizzato il model testing?

Abbiamo utilizzato il controllo del modello Java Path Finder per verificare alcune proprietà di sicurezza (deadlock, race condition) e temporali (utilizzando la logica temporale lineare per specificarle).Supporta asserzioni classiche (come NotNull) su Java (bytecode): serve per il controllo del modello del programma.

Quale strumento di controllo del modello hai utilizzato?

Abbiamo usato Trova percorso Java (per scopi accademici).Inizialmente è un software open source sviluppato dalla NASA.

Come riassumeresti la tua esperienza con la tecnica, in particolare nel valutare la sua efficacia nel fornire software di qualità superiore?

Il controllo del modello del programma presenta un grosso problema con l'esplosione dello spazio degli stati (utilizzo della memoria e del disco).Ma esiste un’ampia varietà di tecniche per ridurre i problemi, per gestire grandi artefatti, come la riduzione parziale dell’ordine, l’astrazione, la riduzione della simmetria, ecc.

Answer 4

Ho utilizzato SPIN per individuare un problema di concorrenza nel software PLC.Ha rilevato una condizione di gara insospettata che sarebbe stata molto difficile da individuare mediante ispezione o test.

A proposito, esiste un libro "SPIN for Dummies"?Ho dovuto impararlo dal libro "The SPIN Model Checker" e da vari tutorial online.

Answer 5

Ho fatto alcune ricerche su questo argomento durante il mio periodo all'università, ampliando il campo Controllo del modello di assieme per l'esplorazione dello stato.

Abbiamo utilizzato una macchina virtuale per percorrere ogni possibile percorso/stato del programma, utilizzando A* e alcune euristiche, a seconda del tipo di errore (deadlock, errori I/O, ...)

È stato ispirato da Java Pathfinder e ha funzionato con il codice C++.(Tutto ciò che GCC potrebbe compilare)

Ma secondo la nostra esperienza questo tipo di tecnologia non sarà presto utilizzata nelle applicazioni aziendali, a causa dei problemi legati alla GUI, del lavoro necessario per creare un ambiente di test iniziale e degli enormi requisiti hardware.(Hai bisogno di molta RAM e spazio su disco, a causa del gigantesco spazio di stato)