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

To formalize business goal model based on category theory

面向目标需求语言(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.