微信服务号

微信订阅号

2025年7月15日 1:43 星期二
首页 > 过刊浏览>2020年第31卷第8期 >2309-2335. DOI:10.13328/j.cnki.jos.005963
PDF HTML阅读 XML下载 导出引用 引用提醒
高阶类型化可验证应用系统体系结构建模及案例
作者:
作者简介:

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

通讯作者:

乌尼日其其格,E-mail:qiqige.wuniri@nlsde.buaa.edu.cn

基金项目:

国家自然科学基金（61305054，61300007，61003016）；科技部基本科研业务费重点科技创新类项目（YWF-14-JSJXY-007）


High-order Typed Verifiable Application System Architecture Modelling and Its Case
Author:
Fund Project:

National Natural Science Foundation of China (61305054, 61300007, 61003016); Basic Research Foundation of Ministry of Science and Technology of China for Key Scientific and Technological Innovation Projects (YWF-14-JSJXY-007)

  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [47]
    • |
  • 相似文献 [20]
    • | | |
  • 文章评论
    摘要:

    随着应用软件体系结构风格变化和规模变大，其运行环境变得日趋复杂，对应用系统体系结构的设计及其正确性验证提出了新的挑战.现有的应用系统体系结构设计关于需求满足性验证在建模与验证中需要多种工具的支持.应用系统体系结构在设计阶段的需求满足验证，有助于客观评价应用系统部署方案和系统如期上线以及主动运维.面向应用系统体系结构设计及其验证，在模型驱动的软件工程背景下提出一种高阶类型化可验证应用系统体系结构建模语言（VASAML）与可验证应用系统体系结构建模方法（VASAMM）.VASAML语言通过定义类型和项的语法和语义，描述构成应用系统体系结构的类型和对象的结构，通过定义两种类型规则及其类型检查算法，判定Γ|-t：T和Γ|-R（T1，T2）是否成立，其中，结构类类型规则用于描述应用系统体系结构中的组成部分，关系类类型规则用于描述组成部分之间的关系和配置.VASAMM方法给出了应用系统体系结构建模过程，包括构建Mbd（基本数据类型）、Mbti（基本接口类型）、Mdev（设备类型）和Mfrwk（应用系统框架）这4层，以及自动生成层内与层间类型之间关系对应的类型规则，同时定义了设备类型服务调用图（GDSI）用以刻画部署要求，定义了类型序列及其正确性用以刻画需求期望性质，并给出了相应的基于类型检查的验证算法.设计实现了基于该方法的原型工具系统VASAMS，其中，建模编辑环境支持应用系统部署方案的设计过程，验证环境支持设计是否满足需求的自动验证.通过一个实际案例完成了某行业较大规模应用系统体系结构的建模和验证.

    Abstract:

    As the application software's architecture style changes and its scale enlarges, the running environment of the application software turned out to be more complex than before. This prompts the verification of the application system architecture as early as in design phase to evaluate the deployment plan objectively and to contribute to the active maintenance of the system, while the existing methods of modelling and verification of the application system architecture needs the support of kinds of tools. In this paper, under the background of MDSE (model driven software engineering), a higher-order typed verifiable application system architecture modelling language (VASAML) and verifiable application system architecture modelling method (VASAMM) are proposed. In the VASAML language, the syntax and semantics of types and terms are defined to describe the structure of the system compositions' types and objects, the typing rules and its type checking algorithms are defined to process the judgement of Γ|-t:T and Γ|-R(T1,T2). In the VASAMM method, the system architecture modelling process is presented, which are the modelling of Mbd (basic data type), Mbti (basic interface type), Mdev (device type), and Mfrwk (framework type). In each layer, modelling of the types and the relations of the types are needed, while the typing rules corresponding to the type relations are automatically generated. Furthermore, the device service invocation graph (GDSI) is defined to describe the deployment requirements and the type sequences and its correctness are defined to describe the properties of user requirements, with the related verification algorithms. The prototype of the verifiable application system architecture modelling system (VASAMS) as a modelling and verifying tool is developed, to which support to the design process by modelling and the automatic verification of the design regarding to the requirements. Finally, the method is applied to a real case of large scale by the design of an application system architecture and it is well verified.

    参考文献
    [1] Gregory T. The economic impacts of inadequate infrastructure for software testing. Technical Report, RTI02-3, National Institute of Standards & Technology, 2002. 15-125.
    [2] Bézivin J. On the unification power of models. Software & Systems Modeling, 2005,4(2):171-188.
    [3] Miller J, Mukerji J, Burt C, Cummins F, Dsouza D, Duddy K, Oya M, Soley R. MDA Guide Version 1.0 Copyright © 2003 OMG. 2003. 15-57.
    [4] Kappel G, Proll B, Reich S, Retschitzegger W. Web engineering:The discipline of systematic development of Web applications. Proc. of the ICWE LNCS, 2006,41(3):457-464.
    [5] Kraus A. Model driven software engineering for Web applications. Dissertation, Ludwig-Maximilians-Universität München, 2007. 3-72.
    [6] Wang J, Zhan NJ, Feng XY, Liu ZM. Overview of formal methods. Ruan Jian Xue Bao/Journal of Software, 2019,30(1):33-61(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5652.htm[doi:10.13328/j.cnki.jos.005652]
    [7] Clarke EM, Wing JM. Formal methods:State of the art and future directions. ACM Computing Surveys, 1996,28(4):626-643.
    [8] Zhang GQ. Introduction to Formal Methods. Beijing:Tsinghua University Press, 2015. 77-225(in Chinese).
    [9] Wuniri QQG, Li XP, Ma SL, Lü JH. Type theory based domain data modelling and verification with case study. Ruan Jian Xue Bao/Journal of Software, 2018,29(6):1647-1669(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5460. htm[doi:10.13328/j.cnki.jos.005460]
    [10] Wuniri QQG, Li XP, Ma SL, Lü JH, Zhang SQ. Modelling and verification of high-order typed software architecture and case study. Ruan Jian Xue Bao/Journal of Software, 2019,30(7):1916-1938(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5749.htm[doi:10.13328/j.cnki.jos.005749]
    [11] Pierce BC. Types and Programming Languages. Cambridge:MIT Press, 2002. 23-200.
    [12] Fowler M. Domain Specific Languages. Addison-Wesley Professional, 2010. 67-113.
    [13] Greenfield J, Short K. Software factories:Assembling applications with patterns, models, frameworks and tools. In:Proc. of the 18th Annual ACM Conf. on Object-oriented Programming, Systems, Languages and Applications. Anaheim, 2003. 16-27.
    [14] Cook S, Jones G, Kent S, Wills A. Domain-specific Development with Visual Studio DSL Tools. Addison-Wesley Professional, 2007. 11-85.
    [15] Hall RS, Heimbigner D, Wolf AL. A cooperative approach to support software deployment using the software dock. In:Proc. of the 1999 Int'l Conf. on Software Engineering (IEEE Cat. No.99CB37002). 1999. 174-183.
    [16] Pahl C, Jamshidi P, Microservices:A systematic mapping study. In:Proc. of the CLOSER 20166th Int'l Conf. on Cloud Computing and Services Science. Rome, 2016. 137-146.
    [17] Balalaie A, Heydarnoori A, Jamshidi P. Microservices architecture enables DevOps:An experience report on migration to a cloud-native architecture. IEEE Software, 2016,33(3):42-52.
    [18] US Department of Commerce. Static analysis is not enough:The role of architecture and design in software assurance. Crosstalk the Journal of Defense Software Engineering, 2014,27(1):1-11.
    [19] Gamma E, Helm R, Johnson R, Vlissides J. Design patterns. Elements of Reusable Object-Oriented Software, 1995,49(2):241-276.
    [20] Ginige A, Murugesan S. Web Engineering:A methodology for developing scalable, maintainable Web applications. Cutter IT Journal, 2001,14:24-35.
    [21] Cosmo RD, Lienhardt M, Treinen R, Zacchiroli S, Zwolakowski J, Eiche A, Agahi A. Automated synthesis and deployment of cloud applications. In:Proc. of the 29th ACM/IEEE Int'l Conf. on Automated Software Engineering. 2014. 211-222.
    [22] Dolstra E, De Jonge M, Visser E. Nix:A safe and policy-free system for software deployment. In:Proc. of the 18th Conf. on Systems Administration (LISA 2004). Atlanta, 2004. 79-92.
    [23] Burg SVD, Dolstra E. Disnix:A toolset for distributed deployment. Science of Computer Programming, 2014,79:52-69.
    [24] Ebert C, Gallardo G, Hernantes J, Serrano N. DevOps. IEEE Software, 2016,33(3):94-100.
    [25] Bass L, Weber I, Zhu L. DevOps:A Software Architect's Perspective. Addison-Wesley Professional, 2015. 65-213.
    [26] Ghezzi C. Formal methods and agile development:Towards a happy marriage. In:Gruhn V, Striemer R, eds. Proc. of the Essence of Software Engineering. Cham:Springer Int'l Publishing, 2018. 25-36.
    [27] Baresi L, Ghezzi C, Ma X, Manna VPL. Efficient dynamic updates of distributed components through version consistency. IEEE Trans. on Software Engineering, 2017,43(4):340-358.
    [28] Newcombe C, Rath T, Zhang F, Munteanu B, Brooker M, Deardeuff M. How Amazon Web services uses formal methods. Communications of the ACM, 2015,58(4):66-73.
    [29] Medvidovic N, Rosenblum DS, Taylor RN. A type theory for software architectures. Technical Report, UCI-ICS-98-14, 1998. 1-10.
    [30] Yin BL, He ZQ, Xu GH, Tan FQ. Discrete Mathematics. 3rd ed., Beijing:Higher Education Press, 2011. 270-279(in Chinese).
    [31] Clerc X. OCaml-Java:OCaml on the JVM. In:Proc. of the TFP 201213th Int'l Symp. on Trends in Functional Programming. St. Andrews, 2012. 167-181.
    [32] Benson T, Akella A, Shaikh A, Sahu S. CloudNaaS:A cloud networking platform for enterprise applications. In:Proc. of the ACM Symp. on Cloud Computing. 2011. 1-13.
    [33] Lin C, Li Y, Wan JX. Optimization approach for QoS in computer networks:A survey. Chinese Journal of Computers, 2011,34(1):1-14(in Chinese with English abstract).
    [34] Fan GC, Zhong H, Huang T, Feng YL. A survey on Web application servers. Ruan Jian Xue Bao/Journal of Software, 2003,14(10):1728-1739(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/14/1728.htm
    [35] Silberschatz A, Gagne G, Galvin PB. Operating System Concepts. 9th ed., Wiley, 2018. 27-55.
    [36] Elmasri R, Navathe S. Fundamentals of Database Systems. 7th ed., Pearson, 2017. 33-56.
    [37] Li Y, Chen M. Software-defined network function virtualization:A survey. IEEE Access, 2015,3:2542-2553.
    [38] Wang WYH, Yeo HN, Zhu YL, Chong TC, Chai TY, Zhou L, Bitwas J. Design and development of Ethernet-based storage area network protocol. Computer Communications, 2006,29(9):1271-1283.
    [39] Birrell AD. Implementing remote procedure calls. ACM Trans. on Computer Systems, 1984,2(5):39-59.
    附中文参考文献:
    [6] 王戟,詹乃军,冯新宇,刘志明.形式化方法概貌.软件学报,2019,30(1):33-61. http://www.jos.org.cn/1000-9825/5652.htm[doi:10.13328/j.cnki.jos.005652]
    [8] 张广泉.形式化方法导论.北京:清华大学出版社,2015.77-225.
    [9] 乌尼日其其格,李小平,马世龙,吕江花.基于类型理论的领域数据建模和验证及案例.软件学报,2018,29(6):1647-1669. http://www.jos.org.cn/1000-9825/5460.htm[doi:10.13328/j.cnki.jos.005460]
    [10] 乌尼日其其格,李小平,马世龙,吕江花,张思卿.高阶类型化软件体系结构建模和验证及案例.软件学报,2019,30(7):1916-1938. http://www.jos.org.cn/1000-9825/5749.htm[doi:10.13328/j.cnki.jos.005749]
    [30] 尹宝林.离散数学.第3版,北京:高等教育出版社,2011.270-279.
    [33] 林闯,李寅,万剑雄.计算机网络服务质量优化方法研究综述.计算机学报,2011,34(1):1-14.
    [34] 范国闯,钟华,黄涛,冯玉琳.Web应用服务器研究综述.软件学报,2003,14(10):1728-1739. http://www.jos.org.cn/1000-9825/14/1728.htm
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

李小平,乌尼日其其格,马世龙,吕江花.高阶类型化可验证应用系统体系结构建模及案例.软件学报,2020,31(8):2309-2335

复制
相关视频

分享
文章指标
  • 点击次数:2776
  • 下载次数: 8149
  • HTML阅读次数: 3460
  • 引用次数: 0
历史
  • 收稿日期:2019-08-31
  • 最后修改日期:2019-11-02
  • 在线发布日期: 2020-04-20
  • 出版日期: 2020-08-06
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第20234377位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号