利用 Maude 追踪 UML 与 OCL 模型的属性
软件工程
2011-07-04 v1 计算机科学中的逻辑
摘要
本文的出发点是一个以 UML 类图形式描述的系统，其中系统状态由 OCL 不变式刻画，系统转换由 OCL 前置与后置条件定义。我们方法的目标是帮助开发者了解所描述系统状态与转换的后果，以及显式给出的属性在形式上的蕴含关系。我们提出通过将 UML 与 OCL 模型翻译到基于重写逻辑的代数规约语言及系统 Maude 中，从而对所陈述的约束进行推理。本文将重点利用 Maude 的状态搜索能力。Maude 的状态搜索提供了描述系统初始配置并探索所有可通过重写到达的配置的可能性。该搜索可通过为允许的状态和允许的转换制定需求来加以调整。
引用
@article{arxiv.1107.0068,
title = {Tracing Properties of UML and OCL Models with Maude},
author = {Francisco Durán and Martin Gogolla and Manuel Roldán},
journal= {arXiv preprint arXiv:1107.0068},
year = {2011}
}
备注
In Proceedings AMMSE 2011, arXiv:1106.5962