Bestavros – Computer Science
Options: Volunteer Basis, Independent Funding Available, Potential for UROP Funding, Potential for Work-Study Potential for Academic Credit
Formal Modeling of Networks
Expected number of students: 2-4
With the advent of software-defined networking architectures like OpenFlow, a large variety of novel networks roles and designs have arisen. This project concerns formal modeling of several such networks using the SPIN and ALLOY tools. Students will model the logic behind a variety of network types (e.g. mobile, ad-hoc, overlay, virtual etc.), focusing on their declarative (i.e. what happens, not how it happens) specification, on guarantees they provide to services running on them, and on the assumptions they rely on to function correctly.