Abstract:As the application softwares 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.

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.

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.