摘要
为提高网构软件的可信性,提出一种网构软件演化的业务一致性验证方法。基于接口自动机对由XYZ/ADL描述的系统进行语义解释,定义XYZ/ADL到接口自动机的转换规则,给出检验系统业务一致性的3个规则,结合实例给出业务一致性的检验过程。通过模型检测器Spin证明该方法能够验证网构软件演化的业务一致性。
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.
出处
《计算机工程》
CAS
CSCD
北大核心
2011年第17期29-31,共3页
Computer Engineering
基金
安徽省自然科学基金资助项目(070412058)
关键词
网构软件
动态演化
业务一致性
接口自动机
体系结构描述语言
internetware
dynamic evolution
business consistency
interface automata
Architecture Description Language(ADL)