Visualizza il feed RSS

Titolo provvisorio...

Formalmente vostri a prescindere, i fratelli Caponi (che siamo noi, chiusa parente)

Valuta questo inserimento
di pubblicato il 11-12-2019 alle 01:43 (231 Visite)
Nella mia lunga esperienza parallela di formatore ho potuto più volte constatare in prima persona l'enorme fatica dell'iniziare a parlare di metodi e linguaggi formali alle giovani generazioni di laureati in discipline attinenti l'informatica e l'elettronica.
Nel migliore dei casi qualcuno cita UML o i diagrammi di flusso, altri hanno inteso parlare qualche volta delle triple di Hoare, gli elettronici hanno forse visto in laboratorio qualche applicativo avanzato che sfrutta i BDD per la specifica e verifica di progetti Verilog e VHDL, ma in generale la confusione regna sovrana.

Soprattutto, fatto gravissimo, la maggioranza di questi giovanotti e neoprofessionisti - che abbia seguito o meno un corso di metodi formali o software engineering - sembra ignorare bellamente l'enorme potenza dei metodi formali e la loro capacità di condurre alla produzione di software e firmware letteralmente a prova d'errore. Per tacere del fatto, troppo spesso ignorato, che tali metodi non sono mera teoria concepita in qualche eburnea turris accademica tanto per pubblicare qualcosa di nuovo, ma sono usati quotidianamente in società di engineering e softwarehouses di ogni dimensione, accomunate da livelli qualitativi estremamente elevati!

Nel migliore dei casi, i messaggi che passano all'epoca degli studi sono delle strane mezze verità del tipo "I metodi formali esistono da decenni, ma solo di recente hanno attirato attenzione" (falso, o comunque limitato a taluni mercati: sono invece ampiamente in uso nelle applicazioni più critiche, e previsti dalle relative normative, fin dai primi anni Novanta, temporalmente a ridosso di alcuni incidenti realmente gravi come quello del Therac-25) o "Alcune parti dei sistemi particolarmente critici vengono specificate tramite linguaggi formali" (falso: questo è solo uno dei possibili profili di applicazione, il più basilare e meno costoso. Ma la stragrande maggioranza delle normative prevede invece che i relativi sistemi siano specificati e verificati per intero).

Senza pretese di alcun genere, vorrei con questa blog entry fare un minimo di chiarezza iniziale, recuperando in buona parte un vecchio post: tanto per cominciare a capire di cosa si parla.

Personalmente ho iniziato a familiarizzare con i metodi formali quasi trenta anni fa, quando ad esempio le logiche temporali erano una novità nel mondo della ricerca per questo tipo di applicazione. Ho avuto la fortuna e la lungimiranza di fare dei formal methods una delle mie specializzazioni nel momento più fecondo della loro storia e di poter seguire in prima persona sul campo - passo dopo passo, progetto dopo progetto, successo dopo successo - l'intera evoluzione teorica e applicativa di molti di tali metodi. Questa lunga esperienza applicativa ha confermato in modo reiterato e sempre più consapevole la mia felice intuizione iniziale riguardo la potenza di siffatti metodi nei frangenti più critici e complessi non solo della progettazione hardware, ma anche e soprattutto per software e firmware.


Cosa è un linguaggio formale (Formal Language)?
Si tratta di linguaggi simbolici, di natura strettamente logico-matematica, dotati di un vocabolario, di una sintassi e di una semantica non ambigua: il tutto specificato in modo formale e rigoroso. Esistono diverse classi di linguaggi formali sviluppati negli ultimi 30 anni di studio sul software engineering e sui metodi informazionali: linguaggi algebrici come LARCH, OBJ, LOTOS, CASL; linguaggi di modellazione come Z, VDM, CSP, ma anche Reti di Petri ed altri automi a stati finiti; linguaggi più recenti, come OCL e Trio, basati sostanzialmente sui linguaggi di modellazione ibridati con altri simbolismi semiformali (es. UML), e poi logiche temporali lineari, circolari, branching (CTL*, da cui CTL e LTL...). Esistono ulteriori approcci complementari, sostanzialmente basati sulle semantiche formali dei linguaggi di programmazione, e qui giganteggia l'interpretazione astratta: un sapere esoterico incapsulato in applicativi complessi e costosissimi, come Polyspace o l'assai meno pretenziosa suite di applicativi proposti da AbsInt.
I linguaggi menzionati, e affini, permettono in generale la specifica e la verifica di proprietà statiche ma anche dinamiche del software, secondo il tipo di linguaggio/framework: in molte occasioni la soluzione migliore è, infatti, la combinazione integrata di più metodi formali.
Per ribadire meglio la distinzione, vale la pena di sottolineare che invece UML e i diagrammi di flusso ISO 5807:1985 non sono linguaggi e metodi formali. In tal caso si parla invece di metodi semiformali.

Naturalmente detti linguaggi non sono neppure lontanamente parenti dei comuni linguaggi di programmazione. L'uso di un linguaggio formale richiede di operare una duplice astrazione di tipo matematico, a livello sia procedurale che rappresentativo: questo è il loro punto di estrema forza ed universalità, ma è anche causa di una serie di difficoltà operative nell'utilizzo, che richiede predisposizione, costanza e pratica assidua.

A cosa serve un FL ?
Sostanzialmente un linguaggio formale nasce per assolvere a due scopi:

1) Dare una descrizione matematicamente corretta e non ambigua delle specifiche (specifica formale del software o livello 0); questo serve a comprendere perfettamente la specifica, aggirando i limiti del linguaggio naturale, evidenziando anche eventuali incongruenze della specifica stessa.

2) Verificare in modo estremamente rigoroso, con una vera e propria dimostrazione logica - esattamente come un qualsiasi teorema - che il software scritto rispetti la specifica (verifica formale del software, livello 1).

Non è poco.
Nella pratica invalsa sono riconosciuti tre livelli principali di uso e applicazione dei FL, con costi ovviamente diversi: si va dalla semplice specifica formale, allo sviluppo e verifica formali, fino alla completa dimostrazione di correttezza ("livello 2" in letteratura), il livello più esaustivo e dai costi più elevati, giustificato unicamente nelle applicazioni per le quali sarebbe maggiore il costo di eventuali errori, tanto da renderne inaccettabile il guasto o malfunzionamento.

Perché nessuno o quasi parla di linguaggi e metodi formali ?
Nonostante la loro impressionante potenza logica, che consente in molti campi di far sparire alla radice i concetti stessi di "errore software", "patch", "vulnerabilità" ed altri orrori (su cui peraltro alcuni individui ed aziende hanno costruito intere carriere e lucrosi commerci), i metodi formali ed i relativi linguaggi non vanno molto di moda nel mass market e dintorni. Tuttavia, la prova più evidente del loro assoluto successo è manifestata da una assenza: l'assenza di gravi notizie negative che riguardano i sistemi critici che ogni giorno regolano il traffico aereo e navale, i sistemi militari, i satelliti, le centrali energetiche, gli impianti petrolchimici... come al solito, un singolo albero che cade fa un gran fragore, ma una intera foresta che cresce non si nota neppure.

I motivi della negligenza nel mass market sono svariati ed investono non solo le caratteristiche intrinseche dei FL, ma anche fattori umani ed aziendali distribuiti tra tutti gli attori del processo di sviluppo software. Qui si possono forse accennare superficialmente almeno gli aspetti principali:

- Un linguaggio formale è eccellente per descrivere task critici, sistemi di controllo, famiglie coordinate e concorrenti di macchine Mealy o Moore arbitrariamente complesse, sistemi a parallelismo massivo, kernel realtime, file systems a prova d'errore, database in tempo reale, macchine virtuali, compilatori di compilatori ed altre straordinarie vette di complessità concettuale informatica (e non solo, basti pensare alle logiche sequenziali ed ai VLSI).
Purtroppo però i linguaggi formali "classici" servono letteramente a nulla nella descrizione di una interfaccina utente interattiva o di un wordprocessor, di un sito web o altro. Sebbene LTL/CTL da un lato e OCL dall'altro siano nati anche per estendere le classi di applicabilità, questa limitazione ha comunque ancor oggi un suo peso.

- I linguaggi formali sono automatizzabili, nel senso che sono manipolabili (a livello simbolico) e verificabili da un calcolatore, anche se non esiste un metodo "automatico" per sviluppare del software partendo dalle specifiche. Per una sfortunata contingenza, tuttavia, al di là di qualche simpatico balocco accademico e di alcuni inguardabili accrocchi low-cost, un software in grado di integrare decentemente l'uso di uno o più FL in un coerente processo di sviluppo industriale ha un costo di licenza in €/$ che parte da cifre a quattro o anche cinque zeri. Non essendo oggetti commercialmente appetibili, chi li ha sviluppati inhouse (con notevoli costi) se li tiene ben stretti.

- Ingegneri e sviluppatori, seppure con una distribuzione altalenante secondo l'epoca ed il luogo degli studi, hanno in genere scarsa familiarità con la matematica discreta, le logiche temporali ed in generale le logiche formali superiori.
A pochi practitioners è realmente chiaro come calare questi linguaggi nella pratica, poiché l'uso dei FL deve partire dall'analisi e guidare, senza compromessi o pasticci, l'intero processo di sviluppo.
Il successo commerciale dei RAD ed il ricorso continuo alla prototipazione ingenera abitudini sbagliate (trial and error, iperfetazione di prototipi, eccesso di concentrazione sull'implementazione) e sostanzialmente incompatibili col rigore dei FL: abitudini che nella pratica risultano assai difficili da sradicare e fortificate dietro un'enorme muraglia di hype e pregiudizi fuorvianti. In questo la formazione superiore, sia per le nuove leve che per i professionisti, dovrebbe avere un ruolo più incisivo, a partire dalla divulgazione di case studies non banali il cui successo è dovuto all'impiego rigoroso e costante dei metodi formali.

- Sempre restando nelle softwarehouses, il management non ha la benché minima idea del risparmio di tempi e costi nascosti (nonché di seccature) che si può ottenere spendendo un po' di più all'inizio, nella formazione e nell'applicazione sistematica dei FL all'intero processo di sviluppo. Vista la forma mentis di coloro che prendono decisioni economiche con risvolti tecnici, appare estremamente difficile riuscire a dimostrare in che modo un elevato costo iniziale (non ricorrente, NRE costs) e del personale potrà, sul medio periodo, comportare un'enorme economia di gestione tagliando nettamente i costi di manutenzione dovuti ad errori, con ampie ricadute positive sul valore del prodotto e del brand.

- Dal lato dei clienti la situazione è perfino peggiore. Il cliente medio non riesce a mettere assieme e poi validare una specifica decente, per problemi di linguaggio: s'immagini cosa può succedere quando si mettano in mano ad un committente qualsiasi migliaia di pagine fitte di simboli incomprensibili non solo ai profani, ma perfino ad una moltitudine di ingegneri e informatici. In breve, fuori dai mercati critici pochissimi clienti hanno la capacità e la volontà di finanziare un processo di specifica formale che non sono neppure in grado di seguire e comprendere.

I linguaggi formali sono invece una norma quotidiana in tutti i settori nei quali l'elevata affidabilità del sistema, definita quantitativamente dalle varie normative, è fondamentale, senza compromessi. Sono anche estremamente importanti in ambito IEEE, ACM, ISO ed in generale nella definizione degli standard. Quasi tutte le normative (altro mondo sconosciuto per i più) inerenti i sistemi critici fanno diretto riferimento all'uso obbligatorio di metodi formali, ad esempio:
DO-178/B, la più rigorosa attualmente in vigore, per applicazioni avioniche ed equivalenti;
EN 60880 per il nucleare e l'energetica;
MIL-STD-498, ovviamente di natura militare;
ESA PSS05 per l'aerospaziale;
EN 50128 per il mondo ferroviario;.
EN 61508 sicurezza funzionale industriale e generale, con le sue numerose derivate (es. EN 61511 per l'industria di processo, EN 60601 per l'elettromedicale...).

Conclusione: se si ha una buona predisposizione logico-matematica (ma non occorre certo essere "geni" per capire ed usare un linguaggio formale: ben altro è idearne uno veramente valido, efficace, usabile!), ed una naturale propensione per l'ordine, la qualità ed i lavori fatti una volta per tutte in modo impeccabile, conviene sempre e comunque studiare bene i principi del software engineering, apprendere almeno un paio di linguaggi formali ed esercitarsi vita natural durante nel loro utilizzo.
Allo stesso scopo, un buon corso avanzato di logica matematica non dovrebbe esimersi dal trattare ampiamente le logiche temporali (almeno quelle lineari) e possibilmente anche la teoria categoriale. In questo modo ne guadagnerà, per apertura mentale ed abitudine al rigore logico, anche la produzione del software meno critico, cioè lo sbocco lavorativo a cui è orientata la stragrande maggioranza degli studenti.


• Un minimo assaggio di bibliografia, privilegiando le edizioni più recenti e i manuali di base:

- "Simulation engineering", Ledin, CMP books, 1-57820-080-6
- "Computability and Logic", Boolos & Burgess, Cambridge University Press, 0-521-00758-5
- "The Way of Z: Practical Programming with Formal Methods", J. Jacky, Cambridge Press, 0521559768
- "Z: An Introduction to Formal Methods", Diller, Wiley, 0471939730
- "Introduction to Formal Specification And Z", Potter & Sinclair, Prentice-Hall, 0132422077
- "Understanding Z: A Specification Language and its Formal Semantics", Spivey, Cambridge University Press, 0521054141
- "Le Reti di Petri: Teoria e Pratica. 1. Teoria e Analisi", G. W. Brams, Editions Masson
- "Le Reti di Petri: Teoria e Pratica. 2. Modellazione e Applicazioni", G. W. Brams, Editions Masson
- "Teoria dei sistemi ad eventi discreti", Carlucci & Menga, UTET
- "Automazione Industriale: Controllo Logico con Reti di Petri", Luca Ferrarini, Pitagora Editrice
- "Model checking", Clarke & Grumberg, MIT Press, 0-262-03270-8
- "Software blueprints", Robertson & Agustì, AWL, 0-201-39819-2
- "Introduction to Formal Languages", Révész, Dover, 0-486-66697-2
- "Logic in computer science", Huth + Ryan, Cambridge, 0-521-65602-8

- "The temporal logic of reactive and concurrent systems", Manna & Pnueli, Springer-Verlag, 0-387-97664-7
- "Computer-aided verification - CAV 90, LNCS 531", Clarke & Kurshan, Springer-Verlag, 0-387-54477-1
- "Computer-aided verification - CAV 97, LNCS 1254", Grumberg, Springer-Verlag, 3-540-63166-6
- "Computer-aided verification - PSCS", Kurshan, Princeton press, 0-691-03436-2

aggiornamento da 31-12-2019 a 15:41 di M.A.W. 1968

Categorie
Libri , Programmazione , Scienza