Soule, Nate2015-06-242015-06-242011-12-30Soule, Nate. "Safe Compositional Modeling And Analysis Of Constrained Flow Networks (MA Thesis)", Technical Report BUCS-TR-2011-030, Computer Science Department, Boston University, December 30, 2011. [Available from: http://hdl.handle.net/2144/11387]https://hdl.handle.net/2144/11387Constrained flow network models represent systems where flows exists between nodes, and constraints exist to regulate those flows. Smart grids, vehicular road travel, computer networks, and cloud-based resource distribution, among other domains all have natural representations in this manner. As these systems grow in size and complexity, traditional analysis and certification of safety invariants becomes increasingly costly. In addition today's techniques require the system to be fully specified in order to perform meaningful analysis. The NetSketch formalism and toolset introduce a lightweight framework for modeling and analysis of constrained flow networks that overcomes these issues. NetSketch offers a processing method based on type-theoretic notions that enables large scale safety verification by allowing for compositional, as opposed to whole-system, analysis. By inferring types for sub-graphs of the modeled networks, not only can cost of analysis be greatly reduced, but analysis of composite modules containing incomplete or underspecified components can be conducted. The NetSketch tool exposes the power of this formalism in an intuitive web-based graphical user interface. This work describes the formalism, a type system, as well as an implementation. In addition potential use cases for this type of modeling and analysis are investigated, and connections are drawn to existing modeling tools and techniques.en-USTechnical Report