Modelling and Verification of High-order Typed Software Architecture and Case Study
Author:
Affiliation:

Clc Number:

TP311

Fund Project:

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

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    Abstract:

    According to the authoritative statistics, more than 70% of software errors during the test are introduced in requirements gathering and analysis or architectural design. The design and verification of the software architecture is essential to improve the quality of application software. The existing application software design methods do not support the verification of requirements, and they usually need the support of other verification tools. In this study, with the background of Web application architecture design and verification, a software architecture modelling and verification language (SAML) and a software architecture modelling and verification method (SAMM), which are based on the higher-order type theory, are proposed. In the SAML language, the syntax and semantics of the types, the ordinary terms as well as the type terms are defined to describe the structure of types and objects, the typing rules are defined to process the judgments of Γ|-t:T and Γ|-R(T1,T2). In the SAMM method, the software architecture modelling paradigm is presented, of which is consisted of the five layers of modelling including Mcls (interface type layer), Mcmpt (component layer), Mcont (container layer), Mfrm (frame layer), and Mfrwk (framework layer). 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 method invocation graph (GSA) is defined to describe the design requirements and the type sequences and its correctness are defined to describe the properties of user requirements, and the related checking algorithms are given. The prototype of the software architecture modelling and verification system 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 software architecture and its verification and evaluation.

    Reference
    Related
    Cited by
Get Citation

乌尼日其其格,李小平,马世龙,吕江花,张思卿.高阶类型化软件体系结构建模和验证及案例.软件学报,2019,30(7):1916-1938

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:July 10,2018
  • Revised:September 28,2018
  • Adopted:
  • Online: April 03,2019
  • Published:
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063