Title: Use Cases for Compositional Modeling and Analysis of Equation-based Constrained Flow Networks

Authors: Nate Soule, Azer Bestavros, Vatche Ishakian, Assaf Kfoury, and Andrei Lapets

Date: July 15, 2011

Abstract: 

Numerous domains exist in which systems can be modeled as networks
with constraints that regulate the ow of trac. Smart grids, vehicular
road travel, computer networks, and cloud- based resource
distribution, among others all have natural representations in this
manner. As these systems grow in size and complexity, analysis and
certication of safety invariants becomes increasingly costly. The
NetSketch formalism and toolset introduce a lightweight framework for
constraint-based modeling and analysis of such ow networks. NetSketch
oers a processing method based on type-theoretic notions that enables
large scale safety verication by allowing for compositional, as
opposed to whole-system, analysis. Furthermore, by applying types to
the modeled networks, analysis of composite modules containing
incomplete or underspecied components can be conducted. Here we
describe various use cases for such modeling tasks, and walk through
the development of appropriate NetSketch models.