| 基于类型理论的领域数据建模和验证及案例 |
| |
| 引用本文： | 乌尼日其其格,李小平,马世龙,吕江花.基于类型理论的领域数据建模和验证及案例[J].软件学报,2018,29(6):1647-1669. |
| |
| 作者姓名： | 乌尼日其其格 李小平 马世龙 吕江花 |
| |
| 作者单位： | 北京航空航天大学软件开发环境国家重点实验室, 北京 100191,北京航空航天大学软件开发环境国家重点实验室, 北京 100191,北京航空航天大学软件开发环境国家重点实验室, 北京 100191,北京航空航天大学软件开发环境国家重点实验室, 北京 100191 |
| |
| 基金项目： | 国家自然科学基金（61003016，61300007，61305054）；科技部基本科研业务费重点科技创新类项目（YWF-14-JSJXY-007）；软件开发环境国家重点实验室自主探索基金（SKLSDE-2012ZX-28，SKLSDE-2014ZX-06） |
| |
| 摘 要： | 数据作为软件系统的主要处理对象，其规范性有助于软件系统的设计开发和软件系统之间的数据交换。本文面向行业数据规范及其验证，提出了一种基于类型理论的领域数据建模语言（DDML）和领域建模方法（DDMM）。DDML语言通过定义类型和项的语法和语义，描述领域数据类型和对象的结构，通过定义类型规则及其类型检查算法判定任意项t：T?。DDMM给出了领域数据建模的方法，即构建K1（原子类型）、K2（数据元）、K3（数据元目录）三层框架，生成表示K3层数据元目录之间关系的类型规则。在此基础上，给出了数据元目录序列的定义及其正确性判定算法。基于上述方法，实现了一种领域数据建模工具原型系统，并通过领域数据建模与自动验证的一个实际案例，完成了一个较大规模行业数据规范的制定与验证。
|
| 关 键 词： | 类型理论 类型检查 类型规则 领域数据建模 数据规范 |
| 收稿时间： | 2017/6/27 0:00:00 |
| 修稿时间： | 2017/9/1 0:00:00 |
Type Theory Based Domain Data Modelling and Verification with Case Study |
| |
| WUNIRI Qi-Qi-Ge,LI Xiao-Ping,MA Shi-Long and L&#; Jiang-Hua.Type Theory Based Domain Data Modelling and Verification with Case Study[J].Journal of Software,2018,29(6):1647-1669. |
| |
| Authors: | WUNIRI Qi-Qi-Ge LI Xiao-Ping MA Shi-Long and L&#; Jiang-Hua |
| |
| Affiliation: | State Key Laboratory of Software Development Environment, Beihang University, Beijing 100191, China,State Key Laboratory of Software Development Environment, Beihang University, Beijing 100191, China,State Key Laboratory of Software Development Environment, Beihang University, Beijing 100191, China and State Key Laboratory of Software Development Environment, Beihang University, Beijing 100191, China |
| |
| Abstract: | As the main object manipulated by a software system, the Datawith adomainstandard cancontributeto the process of the thesoftware design and the data shareware between thesoftware systems. In this paper, with the background of domain data staderdization, a Domain Data Modelling Language(DDML) andaDomainDataModelling Method(DDMM), which are based on the type theory,are proposed. In the DDML language, the syntaxandsemantics of types and terms are defined to describe thestructureof thedomain data types and objects, the typing rules are defined to process the judgement of t:T. In the DDMM method, the data modelling processes are presented,whicharethe data modelling of K1(atomic type),K2(data element),K3(data element directory) and the generation of typing rules in K3. Futhermore the definition of the Data Element DirectorySequences and the algorithsm of checkingits correctnessare defined.Based on the above, a prototype of the domain data modelling system as a modelling tool is developed and applied to a real case of large scale by the generation of the domain data standerd and its elvalueation. |
| |
| Keywords: | type theory type checking typing rules domaindata modelling data standard |
|
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|
