UML活动图到形式化规范的自动映射以支持包含性检查

业务分析师和领域专家经常使用技术无关和平台无关的高层模型来勾勒软件系统的行为。开发人员将用技术细节来细化和丰富这些高层模型。因此，随着时间的推移，细化后的模型可能会偏离原始模型，特别是当两种模型独立演化时。在此背景下，我们关注行为模型；即，我们旨在确保细化的低层行为模型符合相应的高层行为模型。基于现有的形式化验证技术，我们提出包含性检查（containment checking）作为一种手段，来评估低层模型描述的系统行为是否满足高层模型中的规定。主要障碍之一是如何减轻创建行为模型的形式化规范以及一致性约束的负担，手动完成这些工作既繁琐又容易出错。本文提出的方法旨在通过将行为模型视为验证输入，并设计将行为模型自动映射到可直接被模型检查器使用的形式化属性和描述，来缓解上述挑战。我们讨论了该方法中的各种挑战，并通过示例场景展示了其适用性。