摘要：构件的插拔与替换是CBSD实现组装开发、支持定制和演化的基本机制,基于行为协议的构件替换性分析与验证是CBSD的核心研究课题。基于有穷自动机理论和面向服务软件构件的特点,提出了构件行为自动机模型以描述构件的行为协议,定义了构件行为替换性的概念体系,以增进软件构件的复用,开发了构件行为替换性的验证方法,以支持构件行为替换性验证的自动执行。

关键词：基于构件的软件工程 构件替换性 构件自动机 形式化分析 形式化验证 

单位：上海海事大学信息工程学院计算机科学与技术系 上海200433