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