基于类型理论的领域数据建模和验证及案例
作者:
作者单位:

作者简介:

乌尼日其其格(1979-),女,内蒙古赤峰人,博士生,CCF学生会员,主要研究领域为软件形式化方法,类型系统;李小平(1979-),男,博士,高级工程师,CCF学生会员,主要研究领域为云计算,软件形式化方法;马世龙(1953-),男,博士,教授,博士生导师,主要研究领域为海量信息处理的计算模型,软件工程,形式化方法;吕江花(1975-),女,博士,副教授,CCF专业会员,主要研究领域为软件形式化方法,软件工程,安全苛刻系统自动化测试.

通讯作者:

吕江花,E-mail:jhlv@nlsde.buaa.edu.cn

中图分类号:

基金项目:

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


Type Theory Based Domain Data Modelling and Verification with Case Study
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (61003016, 61300007, 61305054); Base Research Foundation ofMinistry of Science and Technology of China (YWF-14-JSJXY-007); Independent Discovery Foundation of State Key Laboratory ofSoftware Development Environment of China (SKLSDE-2012ZX-28, SKLSDE-2014ZX-06)

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    Abstract:

    As the main object manipulated by a software system, data with a domain standard can contribute to the process of software design and data shareware between software systems. In this paper, focusing on domain data standardization, a domain data modelling language (DDML) and a domain data modelling method (DDMM based on the type theory are proposed. In DDML, the syntax and semantics of types and terms are defined to describe the structure of the domain data types and objects, and the typing rules are defined to process the judgement of t:T. For DDMM, the data modelling processes are presented with the data modelling of κ1 (atomic type), κ2 (data element), κ3 (data element directory) and the generation of typing rules in κ3. Furthermore, the definition of the data element directory sequences and the algorithms of checking its correctness are defined. Finally, 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 standard and its evaluation.

    参考文献
    相似文献
    引证文献
引用本文

乌尼日其其格,李小平,马世龙,吕江花.基于类型理论的领域数据建模和验证及案例.软件学报,2018,29(6):1647-1669

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2017-06-27
  • 最后修改日期:2017-09-01
  • 录用日期:2017-11-06
  • 在线发布日期: 2017-12-28
  • 出版日期:
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号