Metodi e imprese formali [chiuso]

Question

...

Insegno metodi formali nell'ingegneria del software. Insegno anche a "metodologie agili". Molte persone sembrano pensare che ciò sia contraddittorio. Penso che abbia molto senso ... Lavoro anche per un'azienda, dove dobbiamo davvero fare le cose :) Mentre posso applicare i miei punti di competenza guadagnati su " specifica " quotidianamente, i miei colleghi in genere fuggono dalla parola "formale".

Pensavo che ciò fosse dovuto al modo intrinseco che impariamo a programmare: di solito siamo spinti a trovare una soluzione funzionante, a non capire il problema. Poi ho pensato che ciò fosse dovuto al fatto che la maggior parte delle persone nella comunità formale non sono ingegneri, ma matematici o informatici. Oggi mi chiedo se sia solo perché la comunità dei metodi formali si nasconde dietro una sorta di "offuscamento" legge per utilizzare tutti i simboli UNICODE disponibili, sviluppare attivamente strumenti scortesi e poco estetici e ridere di fronte agli standard.

Sì, mi sono spostato da un "biasimo loro" a un "incolpare noi" prospettiva ;-)

Quindi, la mia domanda è: usi qualche tipo di metodo formale nella tua azienda? Li hai introdotti o erano prerequisiti? Quali tecniche usi per eliminare la nebbia della matematica dalle paure delle persone e incoraggiarle a usare metodi formali? Cosa pensi che manchino gli strumenti attuali per un uso più generale?

Answer 1

La chiave per convincere le persone ad acquistare in qualsiasi metodi o metodologie è mostrare loro come risolve i problemi che stanno avendo. Se riescono a vedere ciò renderà le loro vite migliori, hai molte più possibilità di farli adottare le tecniche.

E se non puoi mostrarglielo, forse volevi adottare i metodi basati sulla filosofia piuttosto che sulla praticità. A meno che gli altri non condividano la tua filosofia, non puoi arrivare da nessuna parte. E forse non dovresti.

Nel corso dei decenni ci sono state molte metodologie. I più recenti affrontano sempre le carenze dei vecchi, ma i progetti continuano a finire nei guai e fallire. Perché? Perché le rock star che escogitano nuove metodologie sono rock star e hanno creato una nuova metodologia proprio perché comprendono i problemi di fondo e come applicarli. Coloro che vengono dopo tendono a seguire ciecamente la ricetta e non funziona così bene.

Quindi penso che la cosa migliore sia insegnare i problemi sottostanti e quindi mostrare come vari metodi tentano di affrontarli. Le differenze tra aziende, progetti e team sono così grandi che nessuna metodologia può essere applicata con successo a tutte le combinazioni. Imparare a scegliere uno strumento adeguato e applicarlo bene è fondamentale.

Answer 2

Grazie per tutti i contributi. Sono molto perspicaci. Mi permetta di infiammare un po '(non prenderlo sul personale, però :-)

Molte persone sembrano pensare che i metodi formali riguardino solo la verifica del programma. O sistemi critici. Questo può essere vero se perseguiamo il cliché finale: per dimostrare che stiamo facendo il programma giusto (v.s. validazione, che chiede, come ha detto un collaboratore, se stiamo facendo il programma giusto).

Ma considera gli strumenti per la ricerca / controllo dei modelli, come Alloy. Imparare a usare uno strumento come questo richiede una quantità trascurabile di tempo per chiunque sia abituato a UML e OO. Tuttavia, può darti una visione immediata del tuo modello. Di solito non ci vogliono più di 10 minuti per trovare un contro-esempio su un sottoinsieme abbastanza piccolo del modello che si sta tentando di usare (e questo include in primo luogo la descrizione del modello in Alloy).

Prendi come esempio la progettazione dei requisiti. Uno di solito disegna un sacco di UML. Poche persone usano OCL, tuttavia, e molte regole aziendali sono informalmente annotate in linguaggio naturale. Perché? Vincoli temporali?

Ora considera il fatto che la maggioranza usa solo il suo istinto per dimostrare che un modello è soddisfacente. Ancora una volta, perché? Posso impiegare la stessa quantità di tempo (probabilmente anche meno, dal momento che non ho bisogno di preoccuparmi di disegnare l'estetica) per scrivere quel modello in lega e solo verificarne la soddisfazione? E che tipo di matematica ho bisogno adesso? & Quot; predicati " ;? Nome di fantasia per IF e booleani ;-) Quantificatori? Nomi di fantasia per ForEachs () ...

Che dire dei grandi sistemi di informazione? Non hanno bisogno di essere critici ... Prova ad analizzare nella tua testa un diagramma concettuale (non di implementazione!) Con oltre 600 classi. Vedo molte persone sbattere la testa contro il muro con errori del modello facili da fare perché hanno perso qualche vincolo, o il modello consente che accadano cose stupide.

Il fatto è che non è necessario usare approcci formali dalla testa alla coda. Certo, ho potuto provare un'intera domanda in Coq e certificare che è conforme al 100% con alcune specifiche. Questo potrebbe essere l'approccio informatico / matematico.

Tuttavia, con una filosofia GTD, perché non posso delegare alcune attività per il computer e consentirgli di aiutare a migliorare il mio sviluppo? È davvero una questione di "tempo", o semplice, semplice mancanza di capacità tecniche e volontà di imparare / inventare?

Answer 3

Lavorare con lo sviluppo IT della linea di business in un'azienda significa dover trasferire le conoscenze sull'azienda da veri e propri uomini d'affari ai capi degli sviluppatori. Mentre io stesso trovo che la matematica astratta sia uno dei più grandi passatempi che esista, è uno strumento di comunicazione terribile. E la comunicazione è tutto. Anche se potrei avere un certo successo convincendo le persone IT ad abbracciare più notazioni astratte, fondamentalmente non ho alcuna possibilità con gli uomini d'affari.

Mentre ci sono alcune aree in cui posso vedere un ruolo per i metodi formali in un'azienda (software specialistico pesante in matematica e logica, notevole necessità di proprietà dimostrabili come nei software critici per la sicurezza), essi forniscono poco aiuto per ottenere requisiti corretti su per esempio come eseguire un ordine cliente inviando uno o più ordini di fornitura a un insieme di possibili fornitori esterni o interni.

Penso che la giuria sia ancora fuori per approcci basati su modelli e linguaggi specifici di dominio. Penso che avranno successo o meno a seconda che forniscano un feedback più rapido dall'IT ai desideri e alle esigenze del lato aziendale e se presumono che gli uomini d'affari dovranno studiare in modo significativo.

La tecnologia è semplice. La comunicazione è difficile. I metodi formali possono aiutarci a fare le cose bene, ma quelli che ho visto non fanno nulla per aiutarci a fare le cose giuste. (Sì, questi sono cliché, ma è perché sono inevitabilmente e dolorosamente veri.)

Answer 4

Sto seguendo un corso su "Specifiche e verifica". Come parte della struttura del corso stiamo facendo quanto segue- 1. Strumenti di apprendimento come PVS (Prototype Verification System) http://pvs.csl.sri.com/ e SMV (modellazione e verifica del software) http: //www.cs.cmu .edu / ~ ModelCHECK / smv.html 2. A parte ciò, analizziamo gli incidenti verificatisi a causa di guasti del software. Ad es. - Fallimento di Ariane V

Ritengo che i metodi formali siano più applicabili agli scenari in cui il costo del fallimento è superiore al costo di progettazione. E sembra appropriato usarli per i software utilizzati in sistemi critici. Immagino che sia utilizzato nell'avionica, nella progettazione di chip ecc. E che anche l'attuale industria automobilistica lo stia mettendo in pratica.

Answer 5

Ho cercato di convincere la gente ad abbracciare un paio di volte i metodi di specifica formale (Z e Alloy) e ho fatto la stessa esperienza che hai: la maggior parte delle persone, pur sentendo di servire uno scopo utile, è molto a disagio nel usarli per lavoro effettivo.

Abbastanza divertente, le stesse persone sono più che felici di produrre diagrammi UML completamente inutili in quantità enormi.

Penso che ci siano due ragioni principali per questo:

a.) Molti sviluppatori sono a disagio con il livello di astrazione richiesto da un approccio formale. Il fatto che la maggior parte dell'educazione matematica entry-level sia tutto un calcolo e che la matematica non discreta potrebbe avere a che fare con questo.

b.) I metodi formali richiedono un approccio di progettazione molto bottom-up in cui si progetta il modello principale da zero e lo si rende ermetico e quindi si collega ai requisiti dell'utente reale fornendo un'interfaccia sopra di esso. Poiché tendiamo ad avere requisiti che guidano gli sforzi di sviluppo, un approccio dall'alto verso il basso sembra più naturale sebbene spesso porti a modelli incoerenti. È come riqualificare un seminterrato sotto casa dopo che è già stato costruito.

Answer 6

I metodi formali non hanno senso nei sistemi in cui il costo del fallimento è basso.

In un'applicazione Web di produzione, hai più box front-end, più box back-end, più box database - se un programma su uno di essi fallisce, è un non-evento. L'hardware è così economico che puoi costruire questi sistemi a costi molto inferiori al costo di specificare formalmente tutto il tuo software.