We have presented a methodology for designing components so that they can be composed in a pairwise manner, and their temporal behavior properties verified without state-explosion. Our method specifies the externally visible behavior of each component as several behavioral interface automaton, one for each of the other components which interacts directly with. Finite-state automata are widely used as a specification formalism, and so our work in compatible with the mainstream of component-based software engineering.
Ensuring the correct behavior of large complex systems is the key challenge of software engineering. Due to the ineffectiveness of testing, formal verification has been regarded as a possible approach, but has been problematic due to the expense of carrying out large proofs by hand, or with the aid of theorem provers. One proposed approach to making formal methods economical is that of automatic model checking [6]: the state space of the system is mechanically generated and then exhaustively explored to verify the desired behavioral properties. Unfortunately, the number of global states is exponential in the number of components. This state-explosion problem is the main impediment to the successful application of automatic methods such as model-checking and reachability analysis. Our approach is a promising direction in overcoming state-explosion. In addition to the elevator problem, the pairwise approach has been applied successfully to the two-phase commit problem [1] and the dining and drinking philosophers problems [2].
Large scale component-based systems are widely acknowledged as a promising approach to constructing large-scale complex software systems. A key requirement of an successful methodology for assembling such systems is to ensure the behavioral compatibility of the components with each other. This paper presents a first step towards a practical method for achieving this.