• static analysis
• IoT-Lysa
• IoT
• fsharp
• compiler
• CFA
• type system

Negli ultimi decenni si sta assistendo ad un profondo cambiamento nel quale il divario tra il mondo fisico e il mondo virtuale si sta riducendo.
Ormai anche gli oggetti piu' comuni sono identificati, localizzati e connessi attraverso Internet e possono potenzialmente accedere a qualunque servizio.
Inoltre il recente sviluppo tecnologico ha reso possibile dotare gli oggetti di sensori e attuatori per interagire in maniera autonoma nell'ambiente circostante.
In questo modo, questi oggetti sono capaci di raccogliere informazioni, elaborarli, scambiarli con altri servizi, creando nuove informazioni.
Tali sistemi di oggetti formano cio' che viene chiamato Internet of Things.

Progettare, implementare, testare un sistema IoT non e' semplice, perche' il progettista deve tenere in considerazione diversi aspetti tra loro interlacciati, come le esigue risorse hardware a disposizione, i protocolli di rete da usare e gli aspetti algoritmici per l'acquisizione e la manipolazione dei dati.
E' dunque fondamentale valutare un sistema fin dalle specifiche, ancora prima di implementarlo, ovvero ragionare su un modello del sistema che riassume le caratteristiche essenziali di un sistema.
A questo scopo e' stato sviluppato il linguaggio IoT-Lysa che fornisce ai progettisti meccanismi sia per la creazione di un modello e sia per la sua validazione.

Questa tesi presenta la specifica e l'implementazione di un type-system per IoT-Lysa.
La specifica del type-system e' definita tramite un insieme di regole di inferenza che realizzano un sistema di deduzione logica indipendente da qualunque algoritmo o linguaggio di programmazione.
Il corrispondente algoritmo di type-checking e' sviluppato come una libreria in fsharp e e' stato integrato in un compilatore esistente che traduce modelli IoT-Lysa in automi.