APICe » Theses » Class » toPRISM

Analisi alto-livello di sistemi in PRISM  


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.


Mirko Viroli (Supervisor)
Matteo Casadei (Co-supervisors)