Safe Compositional Network Sketches
MetadataShow full item record
Citation (published version)Lapets, Andrei; Kfoury, Assaf; Bestavros, Azer. "Safe Compositional Network Sketches", Technical Report BUCS-TR-2010-001, Computer Science Department, Boston University, January 19, 2010. [Available from: http://hdl.handle.net/2144/3780]
NetSketch is a tool for the specification of constrained-flow networks (CFNs) and the certification of desirable safety properties imposed thereon, conceived to assist system integrators in modeling and design. It provides compositional analysis capabilities based on a strongly-typed domain-specific language (DSL) for describing and reasoning about CFNs and relevant invariants. Users can model or design individual network components and perform manual or automated whole-system analysis of the properties thereof. Users can also assemble many instances of these components into larger networks, relying on NetSketch's less precise but more tractable compositional analysis capabilities. This ability to trade "precision of analysis" for "feasibility of analysis" according to available resources is among the novel features of NetSketch. In earlier work we illustrated how NetSketch is applied to actual domains, and provided a formal definition of its underlying formalism. While the NetSketch DSL provides automatic compositional analysis capabilities for modeling and designing entire networks, users may need to employ a wider variety of tools and techniques when modeling and designing individual network components. These can include common tools for reasoning about systems of constraints of various classes (such as linear constraints, quadratic constraints, and so on), as well as logical systems and ontologies that deal with concepts relevant to the application domain. We integrate the "aartifact" lightweight automated assistant for formal reasoning (which has also been applied in proving the soundness of the NetSketch formalism) as a tool for modeling and designing individual network components. We present several use cases within an example application of the NetSketch DSL to demonstrate how the automated assistant provides NetSketch users with both an interface for reasoning formally about constraints, and a straightforward way to implicitly employ a rich domain-specific ontology of logical propositions. This allows users to verify common properties of constraints and constraint sets, and to reason about constraint relationships using automatically verifiable algebraic manipulations.