Il tool e linguaggio PRISM è uno standard di fatto per la modellazione, simulazione e verifica di sistemi probablistici e stocastici, e può quindi essere utilizzato per l'analisi di sistemi informatici di tipo auto-organizzante, ispirati alla biologia, e per ambienti pervasivi. Tuttavia il linguaggio PRISM è di basso livello, e quindi non consente la specifica ad alto-livello dei sistemi di interesse.
L'obbiettivo della tesi è quello di concepire un linguaggio di alto livello per la descrizione di sistemi informatici relativemente ai contesti di cui sopra, e implementare un traduttore verso PRISM in modo da supportarne l'analisi. In ultima istanza, questa testi avrà lo scopo di promuovere l'uso di tecniche di modelchecking probabilistico per sistemi informatici moderni.
