Title: Safe Compositional Equation-based Modeling of Constrained Flow Networks

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

Date: May 15, 2011


Abstract: 

Numerous domains exist in which systems can be modeled as
networks with constraints that regulate the flow of traffic. 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 certification of safety invariants becomes increasingly
costly. The NetSketch formalism and toolset introduce a lightweight
framework for constraint-based modeling and analysis of such flow
networks. 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. Furthermore, by
applying types to the modeled networks, 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. We describe the
NetSketch formalism and tool, a translation from an instantiation of
the NetSketch formalism to the equation-based modeling language
Modelica, and the development of an accompanying Haskell library,
HModelica, that enables the integration of NetSketch and the
OpenModelica modeling platform.