Traffic is a domain specific language that facilitates specification, programming, and maintenance of distributed applications over a network. The acronym stands for Typed Representation and Analysis of Flows For Interoperability Checks.
Mission Statement
It is difficult to develop correct, efficient, and resilient systems, especially in open context in which they will interact with dynamic and unpredictable environments, peers, and adversaries. The heterogeneity and open nature of network systems make analysis of component composition quite challenging, so we aim to make design and implementation of robust network services accessible to the average programmer.
We accomplish this by breaking down the specification of a network system into two parts: specification of flows and specification of types.
- Specification of flows describes the topology and composition of the network system, and how individual components are connected to each other. We expect this part to be accessible by any average programmer.
- Specification of types is to formalize properties of a network in terms of some concrete syntax that can be understood and analyzed by our type system. This is more difficult to specify, but the efforts of a limited number of experts can be shared.
Brief History of Research
The first Traffic features a type system with simple subtyping relation. When network flows are connected to each other, correctness is determined by whether the type of an output signal is a subtype of (i.e., satisfies) the type of signal input. This system is first motivated in [BUCS-TR-2004-021] and further refined in [BBKM:ICNP05].
The soundness of the Traffic type system is shown in [BUCS-TR-2005-015], which also presents a syntax-directed type checking algorithm. A more advanced “compositional analysis” algorithm is given in [BUCS-TR-2005-033] that can incrementally verify a flow with missing pieces. As we gain more information about these missing pieces, the algorithm may reject a flow because it causes inconsistency with existing subtyping assumptions. The notion of subtyping constraints and type variables are first introduced in this paper. This work is featured in our online demonstration.
Orthogonal to our main line of work with Traffic, we also considered indeterministic placement of flows by means of multiple-choice let binding in [BUCS-TR-2005-034]. We examined three type systems of increasing accuracy at the cost of more complexity and compared their strengths.
Finally, our most recent work [BUCS-TR-2006-029] results in Traffic(X), which adds first-order for-all quantification over flow types with constraints, so types of a flow can be parameterized in terms of some type variable, generalized, yet restricted in some way. The “X” is a placeholder that signifies the possibility of utilizing different constraint systems. Traffic(X) allows more precise expression of underlying network properties. This paper presents syntax-directed rules that can form the basis of a syntax-directed type checking algorithm, but our future research is on working out a compositional analysis algorithm.
Getting Started
For a graphical overview of Traffic, you may want to view the
slides of Azer's wonderful presentation [Best06].
Before you try our system, you may also want to read the
![[.pdf]](/traffic/icons/pdf.png){kind=icon}
GFC User Manual.