检索规则说明:AND代表“并且”;OR代表“或者”;NOT代表“不包含”;(注意必须大写,运算符两边需空一格)
检 索 范 例 :范例一: (K=图书馆学 OR K=情报学) AND A=范并思 范例二:J=计算机应用与软件 AND (U=C++ OR U=Basic) NOT M=Visual
机构地区:[1]安徽工程大学计算机与信息学院,安徽芜湖241000
出 处:《计算机工程》2011年第17期29-31,共3页Computer Engineering
基 金:安徽省自然科学基金资助项目(070412058)
摘 要:为提高网构软件的可信性,提出一种网构软件演化的业务一致性验证方法。基于接口自动机对由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.
关 键 词:网构软件 动态演化 业务一致性 接口自动机 体系结构描述语言
分 类 号:TP311.5[自动化与计算机技术—计算机软件与理论]
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在链接到云南高校图书馆文献保障联盟下载...
云南高校图书馆联盟文献共享服务平台 版权所有©
您的IP:216.73.216.171