Metodi Formali nel Processo di Sviluppo del Software

I metodi formali nel processo di sviluppo del software permettono di creare una specifica più completa, uniforme e non ambigua rispetto alle metriche usate tradizionalmente e di ridurre il numero di errori. Tale specifica, basata su cognizioni matematiche, può essere dimostrata, corretta ed eseguita ad alto livello. In questo post ci occuperemo del metodo delle Abstract State Machine per l'analisi e il design del software. Il metodo ASM, permette di seguire il processo di sviluppo dalla raccolta dei requisiti fino all'implementazione, gestendo la dimensione del software, la sua complessità ed affidabilità, permette una modellazione di alto livello accurata, al livello di astrazione attraverso una catena modelli di sistema con livelli di astrazione via via sempre più raffinati. Contrariamente ad UML permette inoltre una maggiore accuratezza. L'Abstract State Machine è un modello di computazione espresso con una notazione rigorosa dal punto di vista matematico e rivolto alla pratica grazie alla sua comprensibilità. Si individuano diverse categorie di ASM: Le Basic ASM, basate su determinismo e parallelismo, idonee per programmi flat; Le Turbo ASM, basate su composizione sequenziale e iterazione, idonee per applicazioni con chiamate ricorsive; Le Multi-Agent ASM (sincrone e asincrone) sono definite come un insieme di agenti che eseguono la loro ASM in parallelo.

 

Le ABS consistono in un vocabolario ∑, un insieme di stati iniziali, un insieme di regole, un simbolo di regola distinto chiamato "main rule" . Gli stati possono essere visti come delle memorie astratte; il vocabolario 

∑ è una collezione finita di simboli funzionali tali che:

• ogni simbolo ha una arietà, i nomi di funzione nullari vengono anche chiamati costanti.
• i simboli di funzione possono esseer statici ( undef, true, false)
• oppure dinamici ( monitorati, condivisi, di output ecc)

Uno stato S sul vocabolario ∑ è una coppia (D,I) dove D rappresenta il dominio e I la funzione di interpretazione dei simboli funzionali in ∑. D è anche chiamato "base set" dello stato, è possibile definire funzioni parziali, una relazione ha sempre valori true,false o undef, nelle applicazioni D viene spesso suddiviso in universi più piccoli. In uno stato i simboli di funzione e gli argomenti delle funzioni sono le locazioni di memoria mentre i valori delle funzioni sono i loro contenuti. Definiamo una "locazione" di uno stato S come una coppia costituita da un simbolo funzionale n-ario f e un insieme di n elementi (a1,...an)  del dominio D. Definiamo un aggiornamento per S, una coppia (l,v) dove l è una locazione di S e v un elemento di D. Un insieme di aggiornamenti viene detto consistente se non ha aggiornamenti in collisione, ovvero se per ogni locazione l e tutti gli elementi u,w è vero che se (l,v),(l,w) appartengono all'insieme allora v=w. Se un insieme di aggiornamenti consistente U viene "sparato" in un dato stato allora il risultato è un nuovo stato. In questo nuovo stato rimane inalterato il contenuto delle locazioni non considerate, mentre per ogni (l,v) in U il contenuto della locazione l nel nuovo stato sarà v. Se un insieme di aggiornamenti U consistente viene sparato in un nuovo stato S, il nuovo stato risultante S+U viene determinato univocamente.Le regole di transizione dell'ASM definiscono la sintassi del programma; interpretando il programma nello stato corrente viene determinato un insieme di aggiornamenti che sparati sullo stato corrente realizzano il nuovo stato. Le regole di transizione sono:

skip  ,regola di skip

f(s1,...sn) .= t  ,regola di Update.

P par Q   ,regola di Block.

if t then P else Q  ,regola di Condition 

let x=t in P ,regola di Let

forall x with y do P  , regola di Forall

choose x with y do P  ,regola di Choose

 Una dichiarazione di regola per un simbolo di regola r di arietà n è una espressione r(x1,...xn)=P , dove P è una regola di transizione e x1,...xn sono le variabili libere di P. In una chiamata ad una regola r(t1,...tn) le variabili xi vengono sostituite con i parametri ti.

Le ASM non prevedono variabili globali. I parametri formali della testa sono le uniche variabili che hanno uno scope globale. Diciamo che una macchina M può fare una mossa da uno stato S ad uno stato T e scriviamo     S => T se

•  se la main rule di M restituisce un insieme di aggiornamenti consistente U partendo dallo stato S e
• T = S+U

Gli aggiornamenti in U vengono detti aggiornamenti interni ( per distinguerli dai possibili aggiornamenti di locazioni monitorate o condivise). T viene detto stato interno successivo. La computazione di una ASM comincia nello stato iniziale, non appena viene compiuta una mossa la computazione procede richiedendo solo che le mosse dell'ambiente che aggiornano le locazioni monitorate e condivise producano uno stato nuovo per la mossa successiva. Se uno stato la macchina non può produrre un insieme di aggiornamenti consistente oppure non è in grado di produrre nessun insieme di aggiornamento lo stato viene definito l'ultimo della computazione.