Safe compositional modeling and analysis of constrained flow networks
Embargo Date
Indefinite
OA Version
Citation
Abstract
Constrained 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.
Description
Thesis (M.A.)--Boston University
PLEASE NOTE: Boston University Libraries did not receive an Authorization To Manage form for this thesis or dissertation. It is therefore not openly accessible, though it may be available by request. If you are the author or principal advisor of this work and would like to request open access for it, please contact us at open-help@bu.edu. Thank you.
PLEASE NOTE: Boston University Libraries did not receive an Authorization To Manage form for this thesis or dissertation. It is therefore not openly accessible, though it may be available by request. If you are the author or principal advisor of this work and would like to request open access for it, please contact us at open-help@bu.edu. Thank you.