Abstract: Addressing the trustworthiness of internetware, this paper proposes an approach to verify business consistency of internetware evolution. The approach gives the semantic interpretation of system described by XYZ/ADL and defines the transformation rules from XYZ/ADL to interface automata, and presents three rules for verifying system business consistency. An example is incorporated to instantiate the application of these rules. Spin model-checker is used to prove that the approach can be used to verify the business consistency of internetware evolution.

Key words: internetware, dynamic evolution, business consistency, interface automata, Architecture Description Language(ADL)

摘要： 为提高网构软件的可信性，提出一种网构软件演化的业务一致性验证方法。基于接口自动机对由XYZ/ADL描述的系统进行语义解释，定义XYZ/ADL到接口自动机的转换规则，给出检验系统业务一致性的3个规则，结合实例给出业务一致性的检验过程。通过模型检测器Spin证明该方法能够验证网构软件演化的业务一致性。

关键词: 网构软件, 动态演化, 业务一致性, 接口自动机, 体系结构描述语言

CLC Number: 

• TP311.5