一种网构软件体系结构中的纵横验证机制*

如何在开放、动态、复杂的Internet环境下开发网构软件是软件技术领域一个挑战性课题。从网构软件整个生命周期入手,对网构软件的形式化模型,在简单介绍抽象状态机(ASM)的基础理论之后,刻画了网构软件的构件模型,并对构件模型进行了基于ASM的形式化描述,在此基础上,将粗粒度抽象构件的精化问题转换为求解构件组合方案的问题,并在体系结构元层,提出一种双向验证方法对不同抽象程度的组合方案进行横向和纵向的验证,以保证目标系统的正确性和求精过程的正确性。以上形式化建模和双向验证方法尽可能地避免和消除了软件设计早期的错误。通过系统实验验证可以看出,该方法对网构软件的开发具有一定指导意义。

Approach of vertical and horizontal verification in internetware architecture

It is a topic of challenge for how to develop internetware in an open, dynamic, complex Internet environment. Formal model of internetware, refinement theory, and formal verification are researched from the life cycle of the internetware. First of all introduced basic theory of ASM, and then proposed the model of component that oriented internetware, and formally described the model of component with abstract state machine. On that basis, translated the problem of coarse-grained abstract component mapping to entity component into the refinement of connector. It proposed a bidirectional verification approach of composition scheme, which made the final system correct, in meta level of architecture. On the whole, the research mentioned above can help to find and fix the errors at as early stage as possible. It is the right way to develop internetware.