logo SBA

ETD

Archivio digitale delle tesi discusse presso l’Università di Pisa

Tesi etd-04042018-122122


Tipo di tesi
Tesi di laurea magistrale
Autore
FORTE, FEDERICO
URN
etd-04042018-122122
Titolo
Un type-system per IoT-Lysa: un linguaggio per modellare sistemi IoT.
Dipartimento
INFORMATICA
Corso di studi
INFORMATICA
Relatori
relatore Prof. Degano, Pierpaolo
relatore Dott. Galletta, Letterio
Parole chiave
  • CFA
  • compiler
  • fsharp
  • IoT
  • IoT-Lysa
  • static analysis
  • type system
Data inizio appello
27/04/2018
Consultabilità
Completa
Riassunto
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.
File