A Domain-Specific Language for Incremental and Modular Design of Large-Scale Verifiably-Safe Flow Networks
Source: Boston University
The authors define a Domain-Specific Language (DSL) to inductively assemble flow networks from small networks or modules to produce arbitrarily large ones, with interchangeable functionally-equivalent parts. Their small networks or modules are "Small" only as the building blocks in this inductive definition (there is no limit on their size). Associated with their DSL is a type theory, a system of formal annotations to express desirable properties of flow networks together with rules that enforce them as invariants across their interfaces, i.e., the rules guarantee the properties are preserved as they build larger networks from smaller ones.