Article | Proceedings of the 4th International Workshop on Equation-Based Object-Oriented Modeling Languages and Tools; Zurich; Switzerland; September 5; 2011 | Safe Compositional Equation-based Modeling of Constrained Flow Networks

Title:
Safe Compositional Equation-based Modeling of Constrained Flow Networks
Author:
Nate Soule: Department of Computer Science, Boston University, USA Azer Bestavros: Department of Computer Science, Boston University, USA Assaf Kfoury: Department of Computer Science, Boston University, USA Andrei Lapets: Department of Computer Science, Boston University, USA
Download:
Full text (pdf)
Year:
2011
Conference:
Proceedings of the 4th International Workshop on Equation-Based Object-Oriented Modeling Languages and Tools; Zurich; Switzerland; September 5; 2011
Issue:
056
Article no.:
005
Pages:
35-44
No. of pages:
10
Publication type:
Abstract and Fulltext
Published:
2011-11-03
ISBN:
978-91-7519-825-5
Series:
Linköping Electronic Conference Proceedings
ISSN (print):
1650-3686
ISSN (online):
1650-3740
Publisher:
Linköping University Electronic Press; Linköpings universitet


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.

Keywords: Flow networks; Network analysis; Safety verification; Constraint based modeling

Proceedings of the 4th International Workshop on Equation-Based Object-Oriented Modeling Languages and Tools; Zurich; Switzerland; September 5; 2011

Author:
Nate Soule, Azer Bestavros, Assaf Kfoury, Andrei Lapets
Title:
Safe Compositional Equation-based Modeling of Constrained Flow Networks
References:

[1] Modelica Association. Modelica Language Specification 3.2. Technical report; Modelica Association; 2010. http://www.modelica.org/documents/ModelicaSpec32.pdf.


[2] Modelica Association. Modelica and the Modelica Association. https://www.modelica.org/; May 2011.


[3] Azer Bestavros; Adam Bradley; Assaf Kfoury; and Ibrahim Matta. Typed Abstraction of Complex Network Compositions. In Proceedings of the 13th IEEE International Conference on Network Protocols (ICNP’05); Boston; MA; November 2005.


[4] Azer Bestavros; Assaf Kfoury; Andrei Lapets; and Michael Ocean. Safe Compositional Network Sketches: Formalism. Technical report; Department of Computer Science; Boston University; Boston; MA; USA; 2009. Tech. Rep. BUCSTR- 2009-029; October 1; 2009.


[5] Azer Bestavros; Assaf Kfoury; Andrei Lapets; and Michael Ocean. Safe Compositional Network Sketches: Tool and Use Cases. Technical report; Department of Computer Science; Boston University; Boston; MA; USA; 2009. Tech. Rep. BUCS-TR-2009-028; October 1; 2009.


[6] Gérard Boudol. The -calculus in direct style. In Conf. Rec. POPL ’97: 24th ACM Symp. Princ. of Prog. Langs.; pages 228–241; 1997.


[7] Adam Bradley; Azer Bestavros; and Assaf Kfoury. Systematic Verification of Safety Properties of Arbitrary Network Protocol Compositions Using CHAIN. In Proceedings of ICNP’03: The 11th IEEE International Conference on Network Protocols; Atlanta; GA; November 2003.


[8] Hackage Community. Hackagedb. http://hackage.haskell.org; May 2011.


[9] GNU Project Developers. GLPK GNU Project. http://www.gnu.org/software/glpk/; January 2011.


[10] Matthew Elder and Jeremy Shaw. Happstack - A Haskell Web Framework. http://happstack.com/index.html; January 2011.


[11] Komei Fukuda. cdd and cddplus homepage. http://www.ifor.math.ethz.ch/fukuda/cdd_home/cdd.html; January 2011. Swiss Federal Institute of Technology.


[12] Andy Gill and Simon Marlow. Happy - The Parser Generator for Haskell. http://www.haskell.org/happy/; January 2011.


[13] Hugo Herbelin. A -calculus structure isomorphic to Gentzen-style sequent calculus structure. In "Proc. Conf. Computer Science Logic"; volume 933 of LNCS; pages 61–75. Springer-Verlag; 1994.


[14] Andrei Lapets; Assaf Kfoury; and Azer Bestavros. Safe Compositional Network Sketches: Reasoning with Automated Assistance. Technical report; Department of Computer Science; Boston University; Boston; MA; USA; 2010. Tech. Rep. BUCS-TR-2009-028; January 19; 2010.


[15] Francois Margot. Francois Margot Homepage.http://wpweb2.tepper.cmu.edu/fmargot/; January 2011. Carnegie Mellon.


[16] Henrik Nilsson. Type-based structural analysis for modular systems of equations. In Proceedings of the 2nd International Workshop on Equation-Based Object-Oriented Languages and Tools; July 2008.


[17] Open Source Modelica Consortium (OSMC). Welcome to OpenModelica. http://www.openmodelica.org/; May 2011.


[18] Lawrence C. Paulson. Isabelle: A Generic Theorem Prover; volume LNCS 828. Springer-Verlag; 1994.


[19] Tomas Rehorek. JavaScript Graphics Library (JSGL) official homepage. http://www.jsgl.org/doku.php; January 2011.


[20] Alberto Ruiz. HackageDB: hmatrix-glpk-0.2.1. http://hackage.haskell.org/package/hmatrix-glpk; January 2011.


[21] Sencha. Sencha - Ext JS - Client-side Javascript Framework. http://www.sencha.com/products/js/; January 2011.


[22] Nate Soule; Azer Bestavros; Assaf Kfoury; and Andrei Lapets. Safe Compositional Equation-based Modeling of Constrained Flow Networks. Technical report; Department of Computer Science; Boston University; Boston; MA; USA; 2011. Tech. Rep. BUCS-TR-2011-014; June 5; 2011.


[23] Nate Soule; Azer Bestavros; Assaf Kfoury; and Andrei Lapets. Use Cases for Compositional Modeling and Analysis of Equation-based Constrained Flow Networks. Technical report; Department of Computer Science; Boston University; Boston; MA; USA; 2011. Tech. Rep. BUCSTR- 2011-019; July 5; 2011.

Proceedings of the 4th International Workshop on Equation-Based Object-Oriented Modeling Languages and Tools; Zurich; Switzerland; September 5; 2011

Author:
Nate Soule, Azer Bestavros, Assaf Kfoury, Andrei Lapets
Title:
Safe Compositional Equation-based Modeling of Constrained Flow Networks
Note: the following are taken directly from CrossRef
Citations:
No citations available at the moment