Genericity in Network Software: Using Type Systems and Formal Methods to Harness Diverse Theories and Calculi for Scalable and Safe Compositions of Network Services

提案编号：0820138提案题目：网络软件中的通用性：使用类型系统和形式化方法为网络服务的可扩展和安全组合验证各种理论和演算主要研究者：Assaf Kfoury，Azer Bestavros和Abraham Matta本研究定义并实现了一个通用的形式化框架，用于编写组合网络规范和程序;后者可以捕获对通信和交互的内容、形式和表示的约束。该项目的贡献包括设计一个多态流语言和相应的算法类型推理和类型检查。定义了具体类型空间来实例化这个通用框架，反映了足够的边界以确保可以在框架中指定的组成系统的正确性;这种类型空间的例子反映了编码理论，调度理论，控制理论，网络演算（其他学科）其中行为和属性可以被构造成定性和定量的层次结构和边界集。结果环境将使网络程序员能够利用有用的结果，从有价值的，但不太容易（平均网络程序员）的方法的安全性和复合软件系统的验证，并将这些方法集成到熟悉的规范和编程实践。

Proposal Number: 0820138Proposal Title: Genericity in Network Software: Using Type Systems and Formal Methods to Harness Diverse Theories and Calculi for Scalable and Safe Compositions of Network ServicesPrincipal Investigators: Assaf Kfoury, Azer Bestavros, and Abraham MattaThis 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.