The mission of air traffic management (ATM) is to effectively maintain and promote air traffic safety, maintain air traffic order and ensure smooth air traffic. For different environments and different aircraft types, ATM systems need to be designed differently. Now that the Concorde has been out of service for more than 20 years, there is a lack of supersonic aircraft in the civil aviation market. However, as a new type of aircraft, supersonic aircraft need to be introduced into the ATM system. Based on the above background, the Model-Based Systems Engineering (MBSE) approach in systems engineering approach is introduced. By using the multi-architecture modeling language KARMA and the multi-architecture modeling tool Airdraw, the metamodels are designed under the GOPPRR method, and the architectural models of ATM system are designed using these metamodels. After building the models, the comprehensiveness of the modeling design for the ATM system can be tested using the SMT checker in the modeling tool. Through this method, we found that this architecture model is functionally compliant with the ATM System requirements as defined by the ICAO through annexes and other documents.