A domain-specific language for the incremental and modular design of large-scale verifiably-safe flow networks
Assaf J. Kfoury · OpenBU (Boston University) · 2011
Flow networks are inductively defined, assembled from small networks or modules to produce arbitrarily large ones, with interchangeable functionally-equivalent parts. We carry out this induction formally using a domain-specific language (DSL). Associated with our DSL is a typing system (or static semantics), a system of formal annotations that enforce desirable properties of flow networks as invariants across their interfaces. A prerequisite for a type theory is a formal semantics, i.e., a rigorous definition of the entities that qualify as feasible flows through the networks, possibly restricted to satisfy additional efficiency or safety requirements. We carry out this in two ways, as a denotational semantics and as an operational (or reduction) semantics.