使用时序图对交互概览图的层次化使用进行形式化与验证
软件工程
2014-01-23 v1 计算机科学中的逻辑
摘要
统一建模语言(UML)凭借其图形化表示和简洁性,尽管语义仍非形式化,却已成为工业界和学术界事实上的标准与广泛使用的语言。交互概览图(IOD)在 UML2 中引入,允许以层次化方式规约行为。本文是对 UML2 形式化动态语义的一项贡献。我们首先对 IOD 的层次化使用进行形式化,随后利用时间着色 Petri 网(timed CP-net)将 IOD、序列图和时序图映射到层次化着色 Petri 网(HCPN)。我们的方法有助于设计者在两个以上的层次级别上同时受益于抽象与精化,从而降低验证复杂性。
引用
@article{arxiv.1401.5612,
title = {Formalization and Verification of Hierarchical Use of Interaction Overview Diagrams Using Timing Diagrams},
author = {Aymen Louati and Chadlia Jerad and Kamel Barkaoui},
journal= {arXiv preprint arXiv:1401.5612},
year = {2014}
}
备注
8 pages, 6 figures