Show simple item record

dc.contributor.authorBestavros, Azeren_US
dc.contributor.authorKfoury, Assafen_US
dc.contributor.authorLapets, Andreien_US
dc.contributor.authorOcean, Michaelen_US
dc.date.accessioned2011-10-20T04:59:26Z
dc.date.available2011-10-20T04:59:26Z
dc.date.issued2009-10-01
dc.identifier.citationBestavros, Azer; Kfoury, Assaf; Lapets, Andrei; Ocean, Michael. "Safe Compositional Network Sketches: Tool and Use Cases", Technical Report BUCS-TR-2009-028, Computer Science Department, Boston University, October 1, 2009. [Available from: http://hdl.handle.net/2144/1752]
dc.identifier.urihttps://hdl.handle.net/2144/1752
dc.description.abstractNetSketch is a tool that enables the specification of network-flow applications and the certification of desirable safety properties imposed thereon. NetSketch is conceived to assist system integrators in two types of activities: modeling and design. As a modeling tool, it enables the abstraction of an existing system so as to retain sufficient enough details to enable future analysis of safety properties. As a design tool, NetSketch enables the exploration of alternative safe designs as well as the identification of minimal requirements for outsourced subsystems. NetSketch embodies a lightweight formal verification philosophy, whereby the power (but not the heavy machinery) of a rigorous formalism is made accessible to users via a friendly interface. NetSketch does so by exposing tradeoffs between exactness of analysis and scalability, and by combining traditional whole-system analysis with a more flexible compositional analysis approach based on a strongly-typed, Domain-Specific Language (DSL) to specify network configurations at various levels of sketchiness along with invariants that need to be enforced thereupon. In this paper, we overview NetSketch, highlight its salient features, and illustrate how it could be used in applications, including the management/shaping of traffic flows in a vehicular network (as a proxy for CPS applications) and in a streaming media network (as a proxy for Internet applications). In a companion paper, we define the formal system underlying the operation of NetSketch, in particular the DSL behind NetSketch's user-interface when used in "sketch mode", and prove its soundness relative to appropriately-defined notions of validity.en_US
dc.language.isoen_US
dc.publisherBoston University Computer Science Departmenten_US
dc.relation.ispartofseriesBUCS Technical Reports;BUCS-TR-2009-028
dc.titleSafe Compositional Network Sketches: Tool & Use Casesen_US
dc.typeTechnical Reporten_US
dc.relation.isnodouble1527


This item appears in the following Collection(s)

Show simple item record