Title: Safe Compositional Specification of Networking Systems: TRAFFIC The Language and Its Type Checking

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

Date: May 12, 2005

Abstract: 

This paper formally defines the operational semantic for TRAFFIC, a
specification language for flow composition applications proposed in
BUCS-TR-2005-014, and presents a type system based on desired safety
assurance. We provide proofs on reduction (weak-confluence,
strong-normalization and unique normal form), on soundness and
completeness of type system with respect to reduction, and on
equivalence classes of flow specifications. Finally, we provide a
pseudo-code listing of a syntax-directed type checking algorithm
implementing rules of the type system capable of inferring the type of
a closed flow specification.