An Extended Type System for Component-Based Design

Researchers: Yuhong Xiong
Advisor:Edward A. Lee
Type systems in modern programming languages are the most widely used and effective semiformal 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 a type system problem, that of ensuring consistent data typing, and supporting (polymorphic) type inference. But the infrastructure is designed to be extensible to more sophisticated uses.

The 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 subtyping relation among types, and use inequalities defined over the type lattice to specify type constraints within components and between components. The system of inequalities can be solved efficiently, with existence and uniqueness of a solution guaranteed by fixed-point theorems. This type system supports both the base types, such as int, double, and strings, and structured types such as array and record types. For structured types, we allow the elements of arrays and records to contain data tokens of arbitrary types, including structured types, and we are able to specify type constraints on them. This system increases the safety and flexibility of the design environment, promotes component reuse, and helps simplify component development and optimization.

An innovative (and speculative) extension to the type system 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 characterize different communication protocols as types and describe these types using a light-weight formalism called interface automata. In addition, we describe the behavior of components using interface automata, and check the compatibility of the components with the communication types through automata composition. Furthermore, we have organized the communication types into a system-level type lattice using the alternating simulation relation among automata. This lattice provides significant insight into the relation among various protocols and helps the design and verification of polymorphic components that can work with multiple protocols. For example, The alternating simulation relations can be viewed as the subtyping relation among the communication types. According to a theorem in interface automata, if a component is compatible with a certain communication type in the lattice, it is also compatible with its subtypes. This is analogous to the subtyping polymorphism in object-oriented languages.

Last updated 11/18/02