Title: Safe Compositional Specification of Networking Systems: A Compositional Analysis Approach

Authors: Likai Liu, Assaf Kfoury, Azer Bestavros, Adam D. Bradley, Yarom Gabay, and Ibrahim Matta

Date: December 28, 2005

Abstract: 

We present a type inference algorithm, in the style of compositional
analysis, for the language TRAFFIC---a specification language for flow
composition applications proposed in BUCS-TR-2005-014---and prove that
this algorithm is correct: the typings it infers are principal
typings, and the typings agree with syntax-directed type checking on
closed flow specifications. This algorithm is capable of verifying
partial flow specifications, which is a significant improvement over
syntax-directed type checking algorithm presented in BUCS-TR-2005-015.
We also show that this algorithm runs efficiently, i.e., in low-degree
polynomial time.