IPODS

Il concetto tradizionale di computazione si è evoluto sempre più rapidamente negli anni recenti, per venire incontro alle esigenze dei moderni sistemi distribuiti in termini di concorrenza, dinamicità, mobilità, sicurezza, interattività, adattatività. Di pari passo, si è accresciuta la complessità di tali sistemi “globali”, basati su wide area networks come internet e orientati al supporto di una vasta gamma di applicazioni eterogenee che, pur sviluppate separatamente, necessitano di interagire in modo controllato e garantito.

In questo ambito, lo scopo del progetto è stato quello di sviluppare solidi fondamenti matematici per lo studio di scenari collaborativi caratterizzati da un'elevata dinamicità dei partecipanti, i quali possono allacciare o abbandonare collaborazioni in modo autonomo e il cui comportamento è fortemente dipendente dall'ambiente in cui operano, inteso come insieme dei partecipanti coinvolti e delle regole che ne controllano l'interazione. Per esempio, una componente può dovere aggiornare, o sopprimere alcune delle proprie funzionalità o aggiungerne di nuove a seconda del contesto in cui opera, possibilmente in modo automatico. Inoltre possono essere presenti avversari che operano per far fallire certe collaborazioni. Queste caratteristiche pervadono molteplici domini, quali reti sociali, servizi web, transazioni lunghe.

Più concretamente, l'obiettivo è stato quello di estendere e integrare tecniche di analisi statiche e dinamiche per offrire certe garanzie, con livelli variabili, circa la capacità di portare a termine con successo una certa attività, le risorse disponibili e la sicurezza delle comunicazioni. Il progetto è stato caratterizzato dall'individuazione di tre fasi distinte che compaiono nelle collaborazioni: 1) contrattazione; 2) commit; 3) esecuzione. Sostanzialmente in (1) le componenti candidate a partecipare negoziano certe garanzie al fine di definire una sorta di contratto. I singoli partecipanti possono accettare o rifiutare il contratto nella fase (2). Se accettato, il contratto vincolerà il loro comportamento in (3) per garantire un'esecuzione globalmente corretta.

Lo schema fornito dalle fasi (1-3) copre un ampio spettro di situazioni. Per esempio ritroviamo queste fasi nelle transazioni (fasi 1-2); nelle sessioni (fasi 2-3); nelle applicazioni di proof carrying code (fasi 1 e 3). Necessariamente si deve permettere che parte della verifica sia effettuata anche a runtime, sulla base di informazioni sia statiche che negoziabili dinamicamente. Gli strumenti matematici che abbiamo utilizzato sono quelli fornitici dalla teoria della concorrenza (calcoli di processo, reti di Petri, riscrittura di grafi, relazioni comportamentali) e dalla teoria dei tipi (tipi sessione, tipi comportamentali, tipi dipendenti, tipi polimorfi). In particolare, abbiamo studiato come estendere: i calcoli di processi per esprimere vincoli sulle interazioni e per modellare sessioni e transazioni con compensazioni da eseguire in caso di fallimenti; i tipi sessione per ottenere delle conversazioni astratte tra componenti; le relazioni di conformance comportamentale per trattare l'adattività; tipi e teorie osservazionali per esprimere invarianti di sicurezza sui dati e sul comportamento delle componenti.

Queste estensioni ci hanno aiutato a definire astrazioni utili per la specifica di sistemi collaborativi aperti e dinamici, dove i partecipanti hanno spesso una visione parziale del sistema essendo a conoscenza solo di quei componenti con cui interagiscono direttamente. Un aspetto importante per i meccanismi di interazione delineati riguarda la realizzazione di opportune misure che ne garantiscano l'attuazione anche presenza di componenti avversarie. Questo richiede la progettazione di una serie di protocolli di basso livello in grado di determinare, e correggere, qualunque deviazione dal ruolo prestabilito per ciascuna componente.

Ugualmente importante è la realizzazione di meccanismi di protezione dei dati. In un sistema aperto, quale ad esempio un sistema peer-to-peer, è necessario che i partecipanti conoscano quali dati/risorse possono accedere, presso quali componenti. Dualmente, è necessario che ciascuna componente possa specificare politiche di accesso ai propri dati/risorse. Il progetto è stato articolato secondo quattro tematiche principali, ad ognuna delle quali è stato dedicato un Work Package composto di più attività, come dettagliato nella proposta del progetto e riassunto di seguito.

In particolare, nel WP1 su “calcoli di processo” le attività hanno riguardato lo sviluppo di modelli e primitive per collaborazioni aperte e adattive (1.1), per transazioni (1.2) e per la gestione dei fallimenti (1.3).

Nel WP2 su “sistemi di tipi”, le attività hanno riguardato lo sviluppo di tipi per interazioni (2.1), di tipi per la sicurezza (2.2) e di tipi per dati adattivi (2.3).

Nel WP3 su “relazioni di conformità”, intese a specificare sia comportamento dei processi che invarianti sui dati, le attività hanno riguardato lo studio della conformità dei partecipanti (3.1), il rimpiazzamento sicuro di partecipanti (3.2) e tecniche di equivalenza uniformi per comportamenti astratti (3.3).

Infine, nel WP4 su “integrazione di tipi, vincoli e relazioni di conformità”, le attività hanno riguardato lo sviluppo si tipi basati su sistemi di vincoli (4.1), di tipi interazione dinamici sfruttabili e modificabili a run-time (4.2) e l'uso combinato di tipi e relazioni di conformità (4.3).

Per poter trattare le collaborazioni aperte si sono sviluppati dei calcoli dotati di primitive atte a modellare le interazioni fra agenti in ambiti fortemente dinamici. Si è introdotto un calcolo di contratti, arricchito con un sistema a vincoli, che permette di trattare le tre fasi di negoziazione, decisione (commit) ed esecuzione anche in ambiente dinamico. Il sistema a vincoli permette di gestire la fase di contrattazione per realizzare l'accordo tra i componenti, garantendo la protezione delle informazioni locali e la coerenza tra le condizioni richieste dai vari partecipanti. Il trattamento concreto dei vincoli è stato realizzato per mezzo della programmazione logica, riducendo così la risoluzione dei vincoli (e quindi la stipulazione di un contratto) all'esecuzione di un programma logico [BCDM12].

Per quanto riguarda i calcoli con sessioni si sono introdotte le sessioni multi-party in un calcolo con meccanismi di interazione sofisticati, controllato da tipi globali. I tipi globali sono specifiche formali di protocolli di comunicazione espresse in termini delle loro interazioni globali. Si è realizzato un nuovo linguaggio per sequenze infinite dotato di una semantica a tracce che ne giustifica le proprietà e le restrizioni. Attraverso proiezioni dei tipi globali si sono ottenute in tal modo sessioni multi-party le quali, oltre alla tradizionale proprietà di avanzamento godono anche di una proprietà di liveness. Si è potuto dimostrare che tali tipi sessione sono corretti e completi rispetto alla semantica costituita appunto dall'insieme delle tracce del tipo globale di origine, con una nozione di completezza meno rigida rispetto alle definizioni classiche [DL10], in quanto essa permette di non considerare, in un tipo globale sottospecificato, le tracce ridondanti [CDP11, CDP12].

Il lavoro [BLZ11] affronta la rappresentazione con tecniche di trasformazione di grafi della semantica operazionale di un calcolo di processi basato su sessioni e sulla composizione strutturata di servizi. Le sessioni possono essere annidate e le comunicazioni tra processi sono legate alla struttura delle sessioni. La codifica avviene passando da una rappresentazione di grafi gerarchici, la cui gerarchia riflette quella delle sessioni.

Il lavoro [BBB12] definisce un calcolo per interazioni aperte e multiparty, dove cioè il numero di partecipanti non è fissato a priori. Il calcolo estende CCS e pi-calcolo in modo semplice, sostituendo alle azioni di prefisso dei link di comunicazione che possono essere usati per formare catene di comunicazioni lunghe a piacere. Viene definita la semantica operazionale LTS del calcolo per la quale la bisimilarità è una congruenza, garantendo la composizionalità e la sostituibilità dei processi. Come esempio viene mostrato che il link-calcolo è abbastanza espressivo da modellare il calcolo degli ambienti mobili puri, che presenta interessanti aspetti di annidamento di ambienti, come potrebbero essere quelli legati a sessioni o transazioni.

Abbiamo anche studiato tecniche operazionali mirando a problemi di dinamicità ed adattabilità di processi. In [BDPZ11a, BDPZ11b] si propone il concetto di adaptable process come un modo di superare le limitazioni che i process calculi hanno per descrivere i pattern di evoluzione dinamica. Tali pattern sono basati su metodi diretti per controllare il comportamento e la locazione di processi in esecuzione, e quindi costituiscono il core delle capacità di adattamento presenti in svariati sistemi concorrenti moderni. Gli adaptable process hanno una locazione e sono sensibili alle azioni di dynamic update a tempo di esecuzione; questo consente di esprimere una vasta tipologia di pattern di evolvabilità per i processi concorrenti. Abbiamo anche studiato, in un calcolo core per gli adaptable process, due verification problem per essi: bounded e eventual adaptation. Mentre il primo assicura che il numero degli stati erronei consecutivi che possono essere attraversati durante una computazione è limitato da un qualche dato numero k, il secondo assicura che, se il sistema entra in uno stato con errori allora uno stato senza errori verrà prima o poi raggiunto. Si studia la (non-)decidibilità di questi due problemi in diverse varianti del calcolo, che risultano dal considerare sia topologie dinamiche e statiche per gli adaptable process, sia diversi pattern di evolvabilità.

I lavori [BKLS11, BK12] si collocano nell'ambito delle attività riguardanti transazioni e gestione dei fallimenti. In [BKLS11] viene identificata una nuova politica di compensazioni per il calcolo di processi Sagas che migliora le quattro politiche di compensazione precedentemente definite. La nuova semantica viene definita in modo denotazionale (per tracce) e in modo operazionale concorrente (mediante codifica in reti di Petri 1-safe). Il lavoro [BK12] estende il precedente definendo una semantica operazionale small-step che corrisponde a quella in [BKLS11] e che puo' essere riadattata facilmente per catturare le altre politiche note.

Il lavoro [BFK12] riprende il calcolo di processi Sagas per mostrare come possa essere usato per definire composizioni di processi che siano in grado di garantire per costruzione la soddisfacibilità di alcune proprietà logiche.

Il lavoro [BMM12] definisce un calcolo di processi comunicanti che estende il join calcolo con la possibilità di definire delle transazioni dinamiche basate sulla comunicazione. Viene mostrato come schemi ricorrenti di transazioni possano essere codificati facilmente e come il nuovo calcolo sia implementabile in jocaml.

Altri lavori hanno riguardato l'ottimizzazione di codice parallelo per piattaforme multi-core e many-core [ACTTK12] e supporti formali per l'integrazione di manager per diversi aspetti non-funzionali all'interno della stessa applicazione parallela [ADKMS12].

I tipi sessione, che permettono di rappresentare in maniera astratta interazioni strutturate anche con più partecipanti e di verificarne la compatibilità nella fase di commit e poi di garantirne in fase di esecuzione proprietà comportamentali come assenza di deadlock o di livelock, erano stati studiati da un punto di vista essenzialmente statico, cioè relativamente a sistemi la cui configurazione era nota e fissata nella fase di analisi e poteva evolversi solo in funzione della computazione che essa determinava. Nel corso del progetto, essi sono stati generalizzati, in modo da poterli utilizzare nell'analisi di sistemi aperti dove la dinamicità è una caratteristica essenziale [BCDM12].

Si è inoltre studiato come coniugare la programmazione a sessioni con la programmazione a oggetti. Innovando profondamente la sintassi e il sistema di tipi, si è raggiunto lo scopo di poter garantire mediante un'analisi statica che una sessione, una volta iniziate, non possa bloccarsi per un deadlock di comunicazione ma prosegua fino alla sua naturale terminazione. A tal fine si sono usati i tipi unione, che si comportano come i minimi supertipi comuni di un insieme di classi, e permettono di implementare senza bisogno di ulteriore programmazione classi non correlate fra di loro ma dotate di interfacce simili. L'integrazione dei tipi-unione in un linguaggio a oggetti basato sulle classi ha portato ad amalgamare sessioni e metodi così da consentire scambi flessibili di dati nel rispetto di protocolli di comunicazione su cui ci si è preventivamente accordati [BCDGV12].

Un problema dei tipi sessione è che quando i tipi sessione e i construtti linguistici corrispondenti sono aggiunti alla sintassi di un calcolo, danno origine a categorie sintattiche separate, con conseguenze duplicazione del lavoro necessario per svilupparne la teoria. Abbiamo mostrato che i tipi sessione, almeno nella forma diadica, possono essere codificati sui sistemi di tipo standard dei linguaggi per la concorrenza. Il codaggio permette di ritrovare proprietà fondamentali dei tipi sessione come semplici corollari. Per quanto riguarda il controllo delle risorse, si sono estesi sistemi di tipi ed effetti in modo da poter considerare politiche di controllo delle risorse decentralizzate e dinamiche. A loro volta tali politiche governano i diritti di accesso, la propagazione e la revoca delle capacità, il cambio dei possessori di dati, i ruoli dei partecipanti, etc. In particolare ci interessava garantire la riservatezza dell'informazione che le componenti mobili possono trasportare e/o comunicare in modo selettivo. A tal fine si è introdotto un calcolo di sessioni multiparty con delega, arricchito con la presenza di livelli di sicurezza tanto per i partecipanti che per i dati. Il calcolo è dotato di un sistema di tipi che assicura che il flusso di informazioni rispetti i fissati parametri di sicurezza. In particolare, il sistema di tipi impedisce fughe di informazione dipendenti dagli specifici costrutti del calcolo, come l'apertura di una nuova sessione, la selezione, il branching o l'attivazione di una delega. I tradizionali tipi di sessione interagiscono con i tipi per la sicurezza in un gioco reciproco che assicura la correttezza della comunicazione e la fedeltà delle sessioni. Attraverso l'uso congiunto di questi due sistemi si è potuta così garantire la proprietà di non-interferenza, cioè che l'informazione venga fornita solo ai partecipanti che sono in grado di riceverla, e la confidenzialità, cioè che un utilizzatore autorizzato non possa divulgare l'informazione confidenziale ad altri utilizzatori non autorizzati, rivelando così un segreto. Si è anche permessa la declassificazione, cioè che un partecipante autorizzato possa far passare un'informazione da un livello di segretezza ad uno inferiore, possibilmente solo all'interno di determinati contesti e/o per determinati partecipanti e/o prima/dopo aver scambiato determinati messaggi [CCDR10, CCD11, CCD12].

Si è poi esteso il meccanismo delle sessioni multiparty con un sistema di reputazione dei partecipanti. La reputazione associata ad un agente in una sessione relativa ad un servizio web è ottenuta raccogliendo le informazioni rilevanti sul suo comportamento nelle sessioni passate. Il sistema controlla le reputazioni degli agenti prima di consentirne l'ingresso nella sessione, anche in base al ruolo che essi intendono svolgere in essa. Inoltre, ogni agente può dichiarare delle politiche che esso richiede siano seguite dagli altri partecipanti, e poi sulla base di esse aggiornare le reputazioni [BCCD12]. Tipi per il controllo di risorse sono anche stati usati per modellare sistemi biologici [Bio11, BDGT12] e il tempo di calcolo [DR12].

Abbiamo sviluppato modelli comportamentali e tecniche di analisi statica per schemi di autenticazione più espressivi, per il controllo degli accessi alle risorse e per politiche di autenticazione in sistemi distribuiti, basati su raffinamento di sistemi di tipi e su tecniche di model checking.

In particolare, in [BF10] abbiamo sviluppato un insieme di astrazioni di canali che forniscono primitive di alto livello per la specifica di principal onesti in una rete, facilitando al tempo stesso l'analisi degli attacchi di avversari che possono essere installati al livello della rete da un intruso. Abbiamo investigato l'espressività delle astrazioni in base a diverse equivalenze per bisimulazione definite per la sicurezza che nascono dal considerare intrusi con: (i) diverse capability con cui dotare gli avversari e (ii) diverse capacità di controllo sulle interazioni tra i principals.

In [BCM10] abbiamo sfruttato questo framework per definire un sistema di tipi statico per segretezza e autenticazione. In [BM10, Mod12, BCMM12] abbiamo esteso l'insieme di astrazioni dei canali introducendo la nozione di canale forwarding che abbiamo usato nella specifica e analisi di protocolli di e-commerce. Abbiamo anche sviluppato una implementazione prototipale di un model checker di protocolli sfruttando il framework AVISPA-OFMC. In [BCEM11, BCEM12] abbiamo studiato una nuova tecnica per l'analisi di implementazioni distribuite di protocolli che integra raffinamento di sistemi di tipi e sottostrutture per consentire la verifica di sistemi di autorizzazione resource aware, con politiche che predicano sopra il numero di accessi, livelli di uso e di consumo delle risorse. In [BCFS12,Ros10] abbiamo sviluppato tecniche di model checking per la verifica di politiche di sicurezza nel contesto di sistemi di computazione orientati ai servizi [Ros10] e di politiche di controllo degli accessi nella sicurezza dei sistemi operativi, e nello specifico per sistemi grsecurity, e RBAC su Unix/Linux.

Il problema della gestione dei dati nei sistemi informativi aperti è stato affrontato ispirandosi al calcolo Xdpi, che descrive l'evoluzione di una rete di locazioni in cui ogni locazione contiene un albero che rappresenta sia dati che processi mobili in formato XML, come richiesto dalla dinamicità ed eterogeneità dei sistemi aperti, dove i dati possono contenere a loro volta del codice in forma di scripts. Lo scenario è quello in cui ogni locazione ha le proprie regole tanto per l'accesso e la modifica dei dati quanto per l'ingresso e l'uscita dei processi.

Per quanto riguarda il fondamentale aspetto della sicurezza, la soluzione realizzata consiste nel classificare tramite opportuni tipi gli eventi rilevanti, affidando poi al controllo di tipi (type checking) la verifica delle proprietà di sicurezza. Più precisamente, sia ai dati che ai processi vengono assegnati dei livelli di sicurezza che controllano tutti gli eventi, modellati come passi di un calcolo alla Xdpi. Il controllo dell'accesso è basato sui “ruoli”: ogni albero di dati è etichettato con dei ruoli, e ogni processo può assumere differenti ruoli e può dinamicamente abilitare e disabilitare dei ruoli; la politica di una locazione è espressa in termini dei possibili ruoli di processi e dati al proprio interno; così i diritti dei processi dipendono sia dai ruoli ad essi dinamicamente associati che dalla locazione in cui si trovano. I ruoli sono un insieme ordinato, e il calcolo è definito in modo tale da garantire che valgano certe proprietà rilevanti. Ad esempio: un processo può migrare da una locazione ad un'altra solo se è in accordo con la politica della locazione di arrivo.

In questo modo si garantisce che i processi possano sempre trovare i tipi di dato attesi, che la confidenzialità dei dati venga preservata, cioè che un processo possa conoscere solo l'informazione a cui ha diritto di accedere secondo il proprio ruolo, e infine che ai processi “avversari” che non rispettano le politiche delle locazioni sia impossibile violare i livelli di sicurezza dei dati [DGJP11, GJPD12].

L'attività si è poi rivolta al noto paradigma dei Linked Data, che stabilisce delle linee-guida per la pubblicazione e il consumo di dati sul web. La semplice nozione di provenienza in un grafo etichettato è stata estesa con un formato più ricco, che riflette il comportamento dei processi che operano su quei dati, e ne traccia non solo il “dove” di provenienza, ma anche il “da chi”, cioè chi ha pubblicato i dati, e inoltre, in una certa misura, anche il “perchè” (where, who, why). Più precisamente, il meccanismo dei “grafi con nomi” (named graphs), usato nel modello Linked Data per indicare la provenienza, è stato esteso in modo da poter indicare, oltre alla locazione da cui il dato proviene, anche l'agente che lo ha trasmesso e la ragione per cui lo ha trasmesso e poi in modo da poter tracciare tutta la storia della sua provenienza. E' stato poi definito un linguaggio per descrivere i processi che manipolano questi dati e i sistemi costituiti da agenti, processi e dati, dove i processi fanno uso dei tre operatori get, insert e delete che permettono di modellare sia le operazioni HTTP che i meccanismi di query. Tale linguaggio è stato dotato di un sistema di tipi e di una semantica operazionale formalmente specificata: il sistema di tipi controlla la conformità degli agenti alle politiche delle diverse locazioni, la semantica operazionale determina l'evoluzione dei sistemi e le loro interazioni [DHS12]. Abbiamo poi studiato la tipizzazione di dati in formato XML, con particolare attenzione ai problemi fondazionali relativi alla verifica della conformità di un valore alla sua descrizione, e dell'inclusione di un tipo XML, definito tramite espressioni regolari, in un altro tipo XML [CGS11, CGPS12].

In questo contesto, il risultato principale è stato la ridefinizione del problema del type-checking di un linguaggio per la manipolazione di dati XML in termini di inclusione asimmetrica, e la definizione di un algoritmo polinomiale per la risoluzione di tale problema nel contesto di linguaggi di tipo estremamente espressivi, che non erano precedentemente affrontabili se non con costi computazionali proibitivi. Abbiamo studiato l'inferenza di tipi in situazioni in cui si debbano gestire grandi quantità di dati provenienti da fonti diverse e non dotati di una tipizzazione a priori [CGS12].

Un obiettivo è stato quello di sviluppare tecniche di tipo basate sulle relazioni logiche. Si tratta di una tecnica molto potente e molto utilizzata su linguaggi sequenziali di ordine superiore, per esempio per provare proprietà comportamentali (come la indistinguibilità tra due termini che manipolano dati di diverso tipo). Infatti, su linguaggi sequenziali di ordine superiore talvolta le relazioni logiche sono l'unica tecnica possibile. Abbiamo definito [DHS10] tecniche basate su sistemi di tipo in grado di assicurare la terminazione (il fatto che il dialogo di interazioni tra i componenti di un sistema termini), su linguaggi che combinano construtti funzionali (“higher-order”) e construtti per la concorrenza. Le tecniche combinano le relazioni logiche con tecniche da term-rewriting.

In un altra direzione di lavoro [SKS11], abbiamo introdotto un metodo per definire e provare uguaglianze tra termini di linguaggi di tipo “higher-order” (cioè dove esistono variabili che possono essere istanziate con termini del linguaggio stesso). Rispetto ad altre tecniche nella letteratura, queste tecniche hanno il vantaggio di permettere prove semplici (inclusa la prova di congruenza per la bisimulazione) e di potere essere facilmente adattate ad una grande varietà di linguaggi.

Il lavoro [BMM11a] affronta la rappresentazione di reti di Petri come algebra di connettori resource-aware, ponendo le basi per esprimere collaborazioni aperte in modo composizionale. Le reti di Petri vengono infatti dotate di opportune interfacce nelle quali vengono esposti frammenti di transizioni che possono essere completati mediante composizione sequenziale.

Il tema dei connettori viene ripreso in [BMM11b] per mostrare come sia possibile codificare un semplice meccanismo di calcolo basato su compensazioni in diversi framework, quali BIP, Reo, e tile model.

Lo studio di metodi in grado di operare in presenza di dati incerti è stato trattato in [MM10a, MM10b], per quanto riguarda i modelli, e in [MM10d] relativamente alla manipolazione di informazioni incerte. Uno studio di caso, orientato all'analisi di quanto dati reali utilizzati in processi ospedalieri siano affetti da diverse tipologie di incertezza, è stato presentato in [BFGLMMM10].

L'analisi di sistemi sociali complessi [CLMPR10,MR11,RMI11] e processi di trasformazione di informazioni [MMR10a,MMR10b] è stata in seguito sviluppata nella definizione di metodi di estrazione di queste informazioni, nello specifico contesto in cui i processi di manipolazione da esse subiti abbiano determinato strutture complesse contenenti svariate tipologie di dati e di strutture dati, ad esempio etichette temporali relative a specifiche manipolazioni avvenute durante la loro generazione [MM10c,MMNR11]. In [GR10a, GR12] abbiamo sviluppato un calcolo di processi per modellare e ragionare su Mobile Ad Hoc Networks (MANETs). Il calcolo cattura in modo naturale le caratteristiche essenziali delle MANET, inclusa la capacità per un nodo di fare il broadcast di un messaggio verso ogni altro nodo entro il suo raggio di trasmissione, e anche di spostarsi dentro e fuori dal raggio di trasmissione di altri nodi. In [GHMR11a] abbiamo esteso il calcolo con attributi quantitativi per rappresentare la mobilità dei nodi in termini di distribuzione di probabilità sulle locazioni. La relazione di equivalenza risultante ci fornisce una tecnica per verificare se due reti esibiscono o meno lo stesso comportamento osservabile in termini di connettività a di valutare le reti quantitativamente in termini di consumo di energia e throughput globale. In [GHMR11b] abbiamo sfruttato lo stesso framework per l'analisi di due protocolli ben noti per il controllo degli errori: stop-and-wait (SW) e go-back-N (GBN). In [GR10b, BGHMR12] abbiamo esteso il framework con metriche per la misurazione delle interferenze. In [GDMR12] abbiamo esteso il framework per applicarlo all'analisi di uno scenario di comunicazione wireless indoor, per valutare la vulnerabilità della rete a intercettazioni casuali e jamming. Infine in [GHKMRS12] abbiamo implementato il nostro modello sulla piattaforma di model checking PRISM.

In [BCDM12] si è integrata la tecnologia dei tipi sessione con quella della programmazione a vincoli. Il sistema di vincoli ha permesso di superare alcune note difficoltà e inadeguatezze dei calcoli di processi: in primo luogo, il risultato dell'analisi statica è sempre on-off, cioè l'interazione o è accettabile o non lo è, mentre in realtà nella maggior parte dei casi essa potrebbe comunque essere consentita restringendo opportunamente i comportamenti dei partecipanti; in secondo luogo, il processo di verifica deve essere ripetuto per ciascuna coppia di partecipanti, mentre sarebbe più conveniente scinderlo in tre parti, una al tempo di compilazione in cui si stabiliscono i singoli comportamenti, una ad un tempo analogo a quello di linking in cui si stabilisce il comportamento globale, e una al tempo di esecuzione in cui si effettua un controllo per ogni coppia di partners. Infatti, con l'approccio a vincoli, la fase di compilazione costruisce induttivamente i vincoli individuali, la fase di matching compone i vincoli e ha successo solo se i vincoli sono compatibili, infine nella fase di esecuzione il rispetto dei vincoli viene monitorato da guardie di tipo “ask”. Un vincolo è un insieme di assegnazione di termini di Herbrand a variabili di un programma logico. Il sistema di vincoli ha la struttura algebrica di un semi-anello, dove gli elementi del semi-anello sono i vincoli, la moltiplicazione ha il significato di composizione di vincoli e l'addizione computa il minimo limite superiore. Si ottengono in questo modo vincoli flessibili, che non forniscono come risultati solo dei valori booleani vero o falso, bensì dei dati più informativi, come grado di preferenza, costo, ecc. Vengono in tal modo garantite proprietà quali:

• la coerenza, che garantisce che lo scambio di dati durante le interazioni rispetti i protocolli concordati;
• il progresso o avanzamento, che garantisce che un'attività, una volta iniziata, viene condotta a termine;
• la sicurezza e la protezione dei dati scambiati, grazie a opportuni vincoli sulla istanziabilità delle variabili logiche.

Le primitive fondamentali dei sistemi di vincoli sono state usate per rappresentare raffinamenti o modifiche (tell) o indebolimenti (retract) delle specifiche del protocollo e per verificare (ask) la loro compatibilità e le altre proprietà in esame, operando così una trasposizione e un adattamento da un linguaggio di processi a un sia pur peculiare linguaggio di tipi.

Si sono inoltre studiati algoritmi di inferenza di tipi, che permettono di ricavare le proprietà di un processo, e dei protocolli che esso realizza, in tutte le fasi dell'interazione, in modo da poter usare tecniche di interleaving [DHS12].