Component Substitutability Analysis and Verification Based on Behavior Automata
基于行为自动机的构件可替换性分析与验证

This paper discusses component substitutability at the protocol level. Component behavior is modeled by Component behavior automaton (CBA), which is a special kind of nondeterministic finite automata (NFA). Based on CBA, a component substitutability analysis model is presented, which contains four substitutability types partitioned by two dimensions: component environment transparency and interaction similarity. This model can better ensure interaction compatibility than a traditional model based on subtype, and related verification algorithms are developed to automatically analyze component substitutability. In order to make component substitution more precise and increase component reuse, this model makes the behavior of component substituted for the actual interactive behavior that is expressed in the component environment. The reference behavior is formally defined by analyzing the actions by which the component substituted for is bound within the environment.