JavaScript is disabled for your browser. Some features of this site may not work without it.
    View Item 
    •   OpenBU
    • College of Arts and Sciences
    • Computer Science
    • CAS: Computer Science: Technical Reports
    • View Item
    •   OpenBU
    • College of Arts and Sciences
    • Computer Science
    • CAS: Computer Science: Technical Reports
    • View Item

    Verification with Natural Contexts: Soundness of Safe Compositional Network Sketches

    Thumbnail
    Download/View
    2009-030-verif...pdf (359.4Kb)
    Date Issued
    2009-10-01
    Author
    Lapets, Andrei
    Kfoury, Assaf
    Share to FacebookShare to TwitterShare by Email
    Export Citation
    Download to BibTex
    Download to EndNote/RefMan (RIS)
    Metadata
    Show full item record
    Permanent Link
    https://hdl.handle.net/2144/1754
    Citation
    Lapets, Andrei; Kfoury, Assaf. "Verification with Natural Contexts: Soundness of Safe Compositional Network Sketches", Technical Report BUCS-TR-2009-030, Computer Science Department, Boston University, October 1, 2009. [Available from: http://hdl.handle.net/2144/1754]
    Abstract
    In research areas involving mathematical rigor, there are numerous benefits to adopting a formal representation of models and arguments: reusability, automatic evaluation of examples, and verification of consistency and correctness. However, accessibility has not been a priority in the design of formal verification tools that can provide these benefits. In earlier work [30] we attempt to address this broad problem by proposing several specific design criteria organized around the notion of a natural context: the sphere of awareness a working human user maintains of the relevant constructs, arguments, experiences, and background materials necessary to accomplish the task at hand. In this report we evaluate our proposed design criteria by utilizing within the context of novel research a formal reasoning system that is designed according to these criteria. In particular, we consider how the design and capabilities of the formal reasoning system that we employ influence, aid, or hinder our ability to accomplish a formal reasoning task – the assembly of a machine-verifiable proof pertaining to the NetSketch formalism. NetSketch 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. It provides capabilities for compositional analysis based on a strongly-typed domain-specific language (DSL) for describing and reasoning about constrained-flow networks and invariants that need to be enforced thereupon. In a companion paper [13] we overview NetSketch, highlight its salient features, and illustrate how it could be used in actual applications. In this paper, we define using a machine-readable syntax major parts of the formal system underlying the operation of NetSketch, along with its semantics and a corresponding notion of validity. We then provide a proof of soundness for the formalism that can be partially verified using a lightweight formal reasoning system that simulates natural contexts. A traditional presentation of these definitions and arguments can be found in the full report on the NetSketch formalism [12].
    Collections
    • CAS: Computer Science: Technical Reports [584]

    Contact Us | Send Feedback | Help
     

     

    Browse

    All of OpenBUCommunities & CollectionsIssue DateAuthorsTitlesSubjectsThis CollectionIssue DateAuthorsTitlesSubjects

    Deposit Materials

    LoginNon-BU Registration

    Statistics

    Most Popular ItemsStatistics by CountryMost Popular Authors

    Contact Us | Send Feedback | Help