Software components [17] are supposed to make software less fragile and more reliable. In practice, however, part of the fragility is merely shifted from the component artifacts to the connectors and the composition process. When the composition is unreliable, component systems are just as fragile and unreliable as monolithic software. Improving the theoretical and practical foundation of third-party composition techniques [21] is thus essential to improving overall component software reliability.
In this paper, we make initial steps toward a new component model which supports behavioral interoperability and is based on the use of temporal logic and automata to specify and reason about concurrent component systems. Unlike other temporal logic and automata-based methods for software components, our work avoids using exhaustive state-space enumeration, which quickly runs up against the state-explosion problem where the number of global states of a system is exponential in the number of its components.
We present formal analysis and synthesis techniques that address issues of behavioral compatibility amongst components, and enable reasoning about the global behavior (including temporal behavior, i.e., safety and liveness) of an assembly of components. By avoiding state-explosion, our technique is not restricted to small, unrealistic applications.