An Extended Type System for Component-Based Design

Researchers: Yuhong Xiong
Advisor:Edward A. Lee
Type systems in modern programming language are the most widely used and effective (semi)formal verification tools for software. The theory underlying type systems is simple, robust, and extremely powerful, based on fixed-point theorems in topology. The mathematical structure of a set of types is abstractly a lattice, and the theory can be applied to any property of the software that can be characterized using a lattice. It need not be restricted to classical data types.

In view of this, we have designed a set of Java classes in Ptolemy II that provide support for any type system that can be represented using such a lattice. This generic infrastructure has been first applied to the basic type system problem, that of ensuring consistent data typing, and supporting (polymorphic) type inference. But the infrastructure is designed to be extended to more sophisticated uses.

The basic type system combines static typing with run-time type checking. It supports polymorphic typing of system components, and allows automatic lossless type conversion at run-time. To achieve this, we use a lattice to model the lossless type conversion relation among types, and use inequalities defined over the type lattice to specify type constraints in components and across components. The system of inequalities can be solved efficiently, with existence and uniqueness of a solution guaranteed by fixed-point theorems. This type system increases the safety and flexibility of the design environment, promotes component reuse, and helps simplify component development and optimization.

We are currently developing two extensions. One extension is to add support for structured types such as array and record types. The goal is to allow the elements of arrays and records to contain data tokens of arbitrary types, including structured types, and be able to specify type constraints on them. Type constraints and type inference must propagate transparently across operators that construct and disassemble such structures. One of the major difficulties in this extension is that the type lattice becomes infinite, which raises questions on the convergence of type checks and inference.

A more innovative (and speculative) extension is to process-level types. These types represent dynamic properties of an application, rather than the static data types traditionally dealt with in a type system. One of the dynamic properties we have studied is communication protocol. We have attempted to characterize different communication protocols as types and describe these types using automata. Furthermore, we have organized these types into a system-level type lattice using the simulation relation. This lattice provides significant insight into the relation between various protocols and may help design polymorphic components that can work with multiple protocols. For example, we can specify the behavior of a polymorphic component using a non-deterministic automaton. If this automaton simulates the automata of some specific protocols, the component will be able to work with those protocols.

Last updated 11/02/00