UML活动图到支持包容性检查的形式规范的自动映射
Automated Mapping of UML Activity Diagrams to Formal Specifications for Supporting Containment Checking
摘要：
业务分析师和领域专家经常使用与技术和平台无关的高级模型来勾画软件系统的行为。开发人员将用技术细节来完善和丰富这些高级模型。因此，随着时间的推移，细化的模型可能会偏离原始模型，特别是当两种模型独立演化时。在这种情况下，我们专注于行为模型;也就是说，我们的目标是确保细化的低级别行为模型符合相应的高级别行为模型。基于现有的形式化验证技术，我们提出包含检查作为一种手段，以评估系统的行为所描述的低级别模型是否满足已指定的高级别同行。主要障碍之一是如何减轻创建行为模型的正式规范以及一致性约束的负担，这是一项手动完成的繁琐且容易出错的任务。本文提出的方法旨在通过将行为模型视为验证输入，并将行为模型自动映射到可直接由模型检查器使用的形式属性和描述上，来缓解上述挑战。我们讨论了我们的方法中的各种挑战，并展示了我们的方法在说明性场景中的适用性。
英文摘要：
Business analysts and domain experts are often sketching the behaviors of a software system using high-level models that are technology- and platform-independent. The developers will refine and enrich these high-level models with technical details. As a consequence, the refined models can deviate from the original models over time, especially when the two kinds of models evolve independently. In this context, we focus on behavior models; that is, we aim to ensure that the refined, low-level behavior models conform to the corresponding high-level behavior models. Based on existing formal verification techniques, we propose containment checking as a means to assess whether the system's behaviors described by the low-level models satisfy what has been specified in the high-level counterparts. One of the major obstacles is how to lessen the burden of creating formal specifications of the behavior models as well as consistency constraints, which is a tedious and error-prone task when done manually. Our approach presented in this paper aims at alleviating the aforementioned challenges by considering the behavior models as verification inputs and devising automated mappings of behavior models onto formal properties and descriptions that can be directly used by model checkers. We discuss various challenges in our approach and show the applicability of our approach in illustrative scenarios.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
