Show simple item record

dc.contributor.authorSkowyra, Richard Williamen_US
dc.date.accessioned2016-03-08T19:13:33Z
dc.date.available2016-03-08T19:13:33Z
dc.date.issued2014
dc.identifier.urihttps://hdl.handle.net/2144/15116
dc.description.abstractSoftware-Defined Networking (SDN) has become increasing prevalent in both the academic and industrial communities. A new class of system built on SDNs, which we refer to as SDN-Enabled, provide programmatic interfaces between the SDN controller and the larger distributed system. Existing tools for SDN verification and analysis are insufficiently expressive to capture this composition of a network and a larger distributed system. Generic verification systems are an infeasible solution, due to their monolithic approach to modeling and rapid state-space explosion. In this thesis we present a new compositional approach to system modeling and verification that is particularly appropriate for SDN-Enabled systems. Compositional models may have sub-components (such as switches and end-hosts) modified, added, or removed with only minimal, isolated changes. Furthermore, invariants may be defined over the composed system that restrict its behavior, allowing assumptions to be added or removed and for components to be abstracted away into the service guarantee that they provide (such as guaranteed packet arrival). Finally, compositional modeling can minimize the size of the state space to be verified by taking advantage of known model structure. We also present the Verificare platform, a tool chain for building compositional models in our modeling language and automatically compiling them to multiple off-the-shelf verification tools. The compiler outputs a minimal, calculus-oblivious formalism, which is accessed by plugins via a translation API. This enables a wide variety of requirements to be verified. As new tools become available, the translator can easily be extended with plugins to support them.en_US
dc.language.isoen_US
dc.subjectComputer scienceen_US
dc.subjectVerificationen_US
dc.subjectSoftware-defined networkingen_US
dc.titleVerificare: a platform for composable verification with application to SDN-Enabled systemsen_US
dc.typeThesis/Dissertationen_US
dc.date.updated2016-01-22T18:58:57Z
etd.degree.nameDoctor of Philosophyen_US
etd.degree.leveldoctoralen_US
etd.degree.disciplineComputer Scienceen_US
etd.degree.grantorBoston Universityen_US


This item appears in the following Collection(s)

Show simple item record