Safe Compositional Specification of Networking Systems: TRAFFIC The Language and Its Type Checking
Date
2005-05-01
DOI
Authors
Liu, Likai
Kfoury, Assaf J.
Bestavros, Azer
Bradley, Adam D.
Gabay, Yarom
Matta, Ibrahim
Version
OA Version
Citation
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.