Formal models for qualitative and quantitative analysis of mobile ad hoc and sensor networks

Le reti ad hoc (MANETs) sono sistemi di dispositivi mobili che comunicano tra loro usando collegamenti wireless, senza alcuna infrastruttura prestabilita. L’assenza di una infrastruttura centrale e la natura eterogenea dei dispositivi rendono questa rete particolarmente adatta a gestire situazioni critiche, come ad esempio le comunicazioni in caso di disastri naturali, o nei campi di battaglia. La connettivit`a, il consumo energetico e l’interferenza nelle comunicazioni sono aspetti chiave nella gestione delle reti ad hoc, date le caratteristiche dinamiche dei dispositivi che le costituiscono. In questa tesi proponiamo un modello formale per l’analisi di queste problematiche. In particolare introduciamo un modello non deterministico che ci permette di definire e provare alcune importanti propriet`a legate alla connettivit`a delle reti. Proponiamo poi due differenti estensioni probabilistiche del calcolo introdotto, volte ad un’analisi sia qualitativa che quantitativa delle reti ad hoc. In particolare questa tesi si concentra sullo studio del consumo energetico e del livello di interferenza. Infine, grazie alla tecnica del model checking, viene fornito uno strumento per valutare in modo automatico le prestazioni delle reti ad hoc rispetto alle metriche proposte.