Constructing Large Complex Systems via Tractable Pairwise Composition of Software Components

The objective of the project is to produce useful and practical methods for the development of large complex software systems. The research will address the problem of composing software components into large systems that have guaranteed correctness properties. State-explosion (the exponential growth of the number of possible system behaviors with the number of the system's components) is avoided by analyzing interactions among every pair of components separately, rather than inspecting the interaction of all components at once. This local approach nevertheless enables us to prove that the overall system behaves as desired. Since the number of behaviors that have to be analyzed is much smaller, the amount of effort needed to rigorously analyze and verify large systems is greatly reduced. The main activities are: 1. Develop techniques for the precise description of the required behavior of a software component. 2. Develop practical methods for reasoning about the behavior that results when a set of components are connected to form a large system. The benefit of this research is to reduce the cost of creating realistic size software systems that have demonstrable correctness properties.