软件组件装配的验证：应用于 UML2.0 和 Ugatze 组件模型
软件工程
2012-08-01 v1
摘要
组件方法旨在通过一致且易于操作的组件装配来实现复用。然而，获得一致的组件装配并非易事。为此，我们提倡一种契约式方法，区分不同的语法、结构、语义、同步和服务质量契约。我们已成功将此方法应用于两种半形式化契约组件模型：UML2.0 和 Ugatze。具体而言，我们提出了两种方法：VerifComponentUML2.0 和 VerifComponentUgatze。VerifComponentUML2.0 方法旨在通过两种形式化组件模型 Acme/Armani 和 Wright，验证 UML2.0 组件装配上的语法、结构、同步和服务质量契约。VerifComponentUML2.0 包含两个工具：Wr2fdr 和 Wright2Ada。工具 Wr2fdr 允许将 Wright 表达式转换为 CSP 契约，以便使用模型检测器 FDR 验证同步性。工具 Wright2Ada 是一个 IDM 工具，允许将 Wright 代码转换为 Ada，从而为 UML2.0 开放与 Ada 关联的静态分析和动态工具。VerifComponentUgatze 方法提供了一个框架，允许通过 Acme/Armani 检查 Ugatze 组件装配的语法和结构契约。
引用
@article{arxiv.1207.7121,
title = {V\'erification d'assemblages de composants logiciels : Application aux mod\`eles de composants UML2.0 et Ugatze},
author = {Mourad Kmimech},
journal= {arXiv preprint arXiv:1207.7121},
year = {2012}
}
备注
arXiv admin note: substantial text overlap with arXiv:1207.6831 by different author