This dissertation describes methods for automatically analyzing programs to determine compatibility of software components. Complex systems today are made up of many communicating programs or program components. It is vitally important to ensure that the messages that one component sends to another are understood by the receiving component, otherwise runtime errors will occur.

The techniques described model two software components that are designed to work together, one as a producer of messages and one as a consumer of them, using three forms of automata from formal language theory. Each model's language is an approximation of the messages that the underlying component can either write (for the producer) or read (for the consumer). Once the models are created, they can be checked for compatibility by testing whether the language of the producer's model is a subset of the language of the consumer's. A counterexample to language inclusion represents a message that the producer is able to emit that the consumer is not prepared to accept (or perhaps a spurious counterexample due to the approximation).

We looked at three forms of automata to play the role of the program models: standard finite automata, nested-word automata (NWAs, originally defined by Alur and Madhusudan), and extended finite automata (XFAs, originally defined by Smith, Estan, and Jha). NWAs and XFAs both bring separate precision benefits to the table, letting us model the programs and their formats more precisely.

As part of the dissertation, we also make several new theoretical contributions to both NWAs and XFAs. For example, for NWAs we found an easy-to-correct but significant error in Alur and Madhusudan's description of the the Kleene star construction, and we describe new issues related to introducing epsilon transitions to NWAs. We view XFAs as weighted finite automata (WFAs), and describe a new algorithm for WFAs language inclusion that we use for XFA language inclusion, and describe how to use other ideas from the literature to improve the performance of WFA/XFA language-inclusion testing.

(Click here to access the paper: PDF.)