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 article
Published in: Proceedings of the 4th International Workshop on Equation-Based Object-Oriented Modeling Languages and Tools;
Zurich; Switzerland; September 5; 2011
Linköping Electronic Conference Proceedings 56:5, p. 35-44
Published: 2011-11-03
ISBN: 978-91-7519-825-5
ISSN: 1650-3686 (print), 1650-3740 (online)
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.
[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.
