Proposal Title: Genericity in Network Software: Using Type Systems and Formal Methods to Harness Diverse Theories and Calculi for Scalable and Safe Compositions of Network Services
Principal Investigators: Assaf Kfoury, Azer Bestavros, and Abraham Matta
This research defines and implements a generic formal framework for writing compositional network specifications and programs; the latter can capture constraints on the contents, form, and representation of communications and interactions. The project contributions include the design of a polymorphic flow language and accompanying algorithms for type-inference and type-checking. Concrete type spaces are defined with which to instantiate this generic framework, reflecting sufficient bounds to ensure correctness of composing systems that can be specified in the framework; examples of such type spaces reflect useful results in coding theory, scheduling theory, control theory, network calculus (among several other disciplines) in which behaviors and properties can be structured into both qualitative and quantitative hierarchies and bounding sets. The result environment will enable network programmers to leverage useful results from valuable but less accessible (to the average network programmer) approaches to the safety and verification of composite software systems, and will integrate these approaches into familiar specification and programming practices.
