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 (V_ASAML) and verifiable application system architecture modelling method (V_ASAMM) are proposed. In the V_ASAML 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(T₁,T₂). In the V_ASAMM method, the system architecture modelling process is presented, which are the modelling of M_bd (basic data type), M_bti (basic interface type), M_dev (device type), and M_frwk (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 (G_DSI) 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 (V_ASAMS) 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.