UML行为图的转换以支持软件模型检查
软件工程
2014-04-04 v1
摘要
统一建模语言（UML）目前被接受为（面向对象）软件建模的标准，并且在航空航天工业中的使用正在增加。根据UML开发的复杂软件的验证和确认并非易事，因为软件本身复杂，并且可以使用多种不同的UML模型/图来建模软件的行为和结构。本文提出了一种方法，将多达三种不同的UML行为图（顺序图、行为状态机和活动图）转换为一个单一的转换系统，以支持根据UML开发的软件的模型检查。在我们的方法中，基于用例描述形式化属性。转换是针对NuSMV模型检查器进行的，但我们认为也可以使用其他模型检查器，如SPIN。我们工作的主要贡献是将非形式化语言（UML）转换为形式化语言（NuSMV模型检查器的语言），以促进形式化方法在软件开发中的实际应用。
引用
@article{arxiv.1404.0855,
title = {Transformation of UML Behavioral Diagrams to Support Software Model Checking},
author = {Luciana Brasil Rebelo dos Santos and Valdivino Alexandre de Santiago Júnior and Nandamudi Lankalapalli Vijaykumar},
journal= {arXiv preprint arXiv:1404.0855},
year = {2014}
}
备注
In Proceedings FESCA 2014, arXiv:1404.0436