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-20T05:00:34Z
dc.date.available2011-10-20T05:00:34Z
dc.date.issued2009-10-30en_US
dc.identifier.citationBestavros, Azer; Kfoury, Assaf; Lapets, Andrei; Ocean, Michael. "Safe Compositional Network Sketches: The Formal Framework", Technical Report BUCS-TR-2009-029, Computer Science Department, Boston University, October 1, 2009. [Available from: http://hdl.handle.net/2144/1753]en_US
dc.identifier.urihttps://hdl.handle.net/2144/1753
dc.description.abstractNetSketch is a tool for the specification of constrained-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 while retaining sufficient information about it to carry out 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. The compositional analysis is based on a strongly-typed Domain-Specific Language (DSL) for describing and reasoning about constrained-flow networks at various levels of sketchiness along with invariants that need to be enforced thereupon. In this 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. In a companion paper [6], we overview NetSketch, highlight its salient features, and illustrate how it could be used in two applications: 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).en_US
dc.description.sponsorshipNational Science Foundation (CNS-0952145, CCF-0820138, CSR-0720604, EFRI-0735974)en_US
dc.language.isoen_USen_US
dc.publisherBoston University Computer Science Departmenten_US
dc.relation.ispartofseriesBUCS Technical Reports;BUCS-TR-2009-029en_US
dc.titleSafe Compositional Network Sketches: The Formal Frameworken_US
dc.typeTechnical Reporten_US
dc.relation.isnodouble1524*


This item appears in the following Collection(s)

Show simple item record