计算机科学与探索 ›› 2008, Vol. 2 ›› Issue (2): 198-205.

• 学术研究 • 上一篇    下一篇

构件式系统的建模与验证

曾红卫+,缪淮扣   

  1. 上海大学 计算机工程与科学学院,上海 200072
  • 收稿日期:1900-01-01 修回日期:1900-01-01 出版日期:2008-04-20 发布日期:2008-04-20
  • 通讯作者: 曾红卫

Modeling and verification of component-based system

ZENG Hongwei+, MIAO Huaikou   

  1. College of Computer Engineering and Science, Shanghai University, Shanghai 200072, China
  • Received:1900-01-01 Revised:1900-01-01 Online:2008-04-20 Published:2008-04-20
  • Contact: ZENG Hongwei

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

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

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