基于类型理论的领域数据建模和验证及案例

来源：软件学报杂志2018年第6期北京时间：

作者：乌尼日其其格,李小平,马世龙,吕江花

单位：乌尼日其其格，软件开发环境国家重点实验室(北京航空航天大学), 北京 10008311,李小平，软件开发环境国家重点实验室(北京航空航天大学), 北京 10008302,马世龙，软件开发环境国家重点实验室(北京航空航天大学), 北京 10008303,吕江花，软件开发环境国家重点实验室(北京航空航天大学), 北京 10008304

摘要：数据作为软件系统的主要处理对象，其规范性有助于软件系统的设计开发和软件系统之间的数据交换.面向行业数据规范及其验证，提出了一种基于类型理论的领域数据建模语言（DDML）和领域建模方法（DDMM）.DDML语言通过定义类型和项的语法和语义，描述领域数据类型和对象的结构，通过定义类型规则及其类型检查算法判定任意项t：T?.DDMM给出了领域数据建模的方法，即构建κ1（原子类型）、κ2（数据元）、κ3（数据元目录）三层框架，生成表示κ3层数据元目录之间关系的类型规则.在此基础上，给出了数据元目录序列的定义及其正确性判定算法.基于上述方法，实现了一种领域数据建模工具原型系统，并通过领域数据建模与自动验证的一个实际案例，完成了一个较大规模行业数据规范的制定与验证.

关键词：类型理论;类型检查;类型规则;领域数据建模;数据规范

基金资助：国家自然科学基金（61003016，61300007，61305054）；科技部基本科研业务费重点科技创新类项目（YWF-14-JSJXY-007）；软件开发环境国家重点实验室自主探索基金（SKLSDE-2012ZX-28，SKLSDE-2014ZX-06）