SysML/KAOS领域模型的形式化表示（完整版）
软件工程
2017-12-21 v1
摘要
如今，形式化语言在确保需求一致性方面的效用已得到充分确立。本文工作是为关键复杂系统定义一种基于形式化基础的、基于模型的的需求工程方法的一部分。需求通过SysML/KAOS方法获取，目标形式化规约使用Event-B方法编写。首先，由SysML/KAOS目标模型提供的目标层次生成Event-B骨架。随后第二步，由系统应用领域属性导出的Event-B规约补全该骨架，从而得到系统结构。考虑到领域是通过SysML/KAOS领域模型方法借助本体论表示的，是否可能自动生成系统Event-B模型的结构部分？本文提出一组通用规则，将SysML/KAOS领域本体翻译为Event-B规约。这些规则已通过Rodin工具使用Event-B方法进行了表达、验证与确认，并以起落架系统案例研究加以说明。我们的方案使得能够从以本体形式表示的系统应用领域自动获得Event-B规约的结构部分，该部分将用于形式化验证系统需求的一致性。
引用
@article{arxiv.1712.07406,
title = {Formal Representation of SysML/KAOS Domain Model (Complete Version)},
author = {Steve Tueno and Régine Laleau and Amel Mammar and Marc Frappier},
journal= {arXiv preprint arXiv:1712.07406},
year = {2017}
}
备注
54 pages