Abstract: Composition and safety checking of components give rise to the challenges in component-based system development process. A new model， component message automaton， is proposed to model interaction behavior of components. The model is an extended automaton that is designed to preserve all the interaction properties of components to provide a rich base for further verification. Then synchronous product operation is employed to combine multiple components into a single complex component. Based on controllability from supervisory control theory， the algorithm verifying safety properties of component-based system is developed. A simple example through this paper is studied in detail to illustrate how to apply the proposed approach.

Key words: component message automaton, controllability, verification, component composition

摘要： 构件的组合与安全性是构件式系统开发的一个挑战性问题。提出了一种新的描述构件交互行为的模型－构件消息自动机，其特点是保留了构件的所有交互特性以便进一步进行构件的验证。给出了使用同步积操作将多个构件组合成单个复杂的组合构件的方法。基于监控理论的可控性概念，设计了一个验证构件系统安全性质的算法。为了说明论文建议的方法，详细讨论了一个简单的、贯穿整个论文的示例系统。

关键词: 构件消息自动机, 可控性, 验证, 构件组合