基于行为自动机的构件可替换性分析与验证

在交互协议层面讨论构件的可替换性，采用非确定性有限状态自动机(nondeterministic finite automata，简称NFA)来建模构件的交互行为，在保证交互兼容性的前提下，提出了按构件环境的透明度和构件交互的变化度两维划分的可替换性模型，给出了4类可替换性的形式化定义及其之间的关系，并基于NFA理论给出了相关的验证算法。另外，该模型以构件的替换行为而不是其全部行为作为构件替换的参照，从而使替换时有更多的候选构件可供使用，提高了构件复用的几率。

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.