Safe Compositional Specification of Networking Systems: A Compositional Analysis Approach
Date
2005-12-28
DOI
Authors
Liu, Likai
Kfoury, Assaf J.
Bestavros, Azer
Gabay, Yarom
Bradley, Adam D.
Matta, Ibrahim
Version
OA Version
Citation
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 [2]—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 [3]. We also show that this algorithm runs efficiently, i.e., in low-degree polynomial time.