Checking Format Compatibility of Programs Using Automata
Abstract
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 counter example 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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 01, 2013
- Accession Number
- AD1165875
Entities
People
- Evan E. Driscoll
Organizations
- University of Wisconsin–Madison