基于范畴论的业务目标模型形式化  

To formalize business goal model based on category theory

作　　者：李宗花[1,2] 李必信 Li Zonghua;Li Bixin(School of Computer Science&Technology,Huaiyin Normal University,Huai’an Jiangsu 223300,China;School of Computer Science&Engineering,Southeast University,Nanjing 211189,China)

机构地区：[1]淮阴师范学院计算机科学与技术学院,江苏淮安223300 [2]东南大学计算机科学与工程学院,南京211189

出　　处：《计算机应用研究》2020年第5期1445-1449,共5页Application Research of Computers

基　　金：江苏省高校自然科学研究面上项目(18KJB520006);国家自然科学基金资助项目(61902141,41471425);教育部人文社会科学研究青年基金项目(19YJCZH095);淮安市科技计划资助项目(HABZ201701)。

摘　　要：面向目标需求语言(goal-oriented requirement language,GRL)模型聚焦于待定的需求,被广泛地应用于业务系统的初始需求建模,其模型的正确性影响到业务系统的开发质量。鉴于业务目标模型的形式化可以验证模型的正确性,提出了一种利用范畴论形式化GRL模型的方法。首先,依据GRL元模型结构,应用范畴论中的态射机制形式化描述GRL模型中目标与目标、目标与任务以及任务与任务等节点之间的关系;然后,通过增加范畴模型中的初始对象和终止对象,设计紧邻序列来表示多个目标与任务实施的因果关系;最后,设计业务目标模型系统的正确性结构性质。应用Web Payment系统实验表明,形式化业务范畴模型能够验证GRL模型的正确性,提高目标建模的质量。The goal-oriented requirement language(GRL)focuses on the undetermined requirement,which has been widely used to capture initial requirement of the business system.The correctness of the GRL model is a key to influencing the development quality of the business system.Based on graph category,this paper proposed a model formalization approach to verify the correctness of the GRL model.Firstly,according to the meta-model of the GRL model,it applied the morphism mechanism of the category theory to describe the relationship between goal node and task node,one goal node and the other goal node,one task node and the other task node.Then,it added the initial object and terminal object of the category model,and designed the neighborhood sequence to represent the causation between the multiple goals and the task implementations.Finally,it designed the correctness structure properties of the business objective model system.The Web Payment system was applied to demonstrate the result of the formalization analysis and correctness verification.It shows that the graph category model can verify the correctness of GRL model and improve the quality of goal modeling.

关 键 词：GRL模型 范畴论 模型形式化 模型正确性验证 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]