The project belongs to the field of ldquo; Computer Science and Technology rdquo;. Control software is the core hub of major industrial equipment. Problems with such software can have catastrophic consequences, such as the recent two Boeing 737 MAX8 crashes. How to ensure the security and credibility of control software is an internationally recognized major challenge, and it is also an urgent problem in my country's economic transformation and upgrading. Supported by projects such as the National Fund Commission ldquo; Basic Research on Trusted Software rdquo; Major Research Plan, the project leader focuses on software security and trustworthy assurance technology. After more than ten years of research and collaborative innovation with enterprises, it has overcome the three major problems of software security and trustworthy assurance technology, namely, correctness ldquo; difficulty in verification rdquo;, difficulty in ensuring rdquo; and difficulty in analysis rdquo;. The project team adopted core technologies such as formal analysis, testing and verification to realize a development and verification tool chain covering the entire software life cycle, effectively ensuring the safety and credibility of the development of core control software for major industrial equipment. The project's technical innovations are as follows: 1. Pioneering formal unified modeling theory and multi-dimensional verification technology: In response to the open question raised by two Turing Award winners about whether the concurrent models CCS and CSP are consistent, a unified model framework for concurrent programs has been established., solving the problem that has plagued the international academic community for more than 20 years. The multi-dimensional verification technology proposed based on this theory supports accurate description and strict verification of software systems, and solves the problem of formal modeling and consistency verification of large-scale complex requirements. Microsoft Chief Scientist Bjorner commented that some of the results are the foundational results of ldquo; correlating CCS and CSP trace semantics rdquo;. The results have been applied to the core software development process of systems such as the Fengyun-4 meteorological satellite and the Chang'e-3 reentry and return vehicle. 2. A multi-level simulation and testing technology for token fusion has been built: Aiming at the problems of low test efficiency of typical information-physical fusion systems such as rail transit, a multi-level simulation and testing technology has been built, which has effectively improved the test efficiency and quality of the control system. This technology shortens the integrated test cycle of Casco's subway signaling system (ranked first in China) from one month to one week, supporting it to become the first signaling system in China to receive the highest international safety certification SIL4. This technology provides guarantees for the development of key software products of China Comac, Eighth Aerospace Academy and other units. 3. Invented multi-attribute quantitative evaluation and analysis technology in uncertain environments: Aiming at key attributes such as real-time performance of the control system, comprehensive quantitative analysis technologies such as software multi-attribute quantitative evaluation, real-time measurement, and failure estimation in uncertain environments were established for the first time, solving the problem of accurate quantitative analysis of software complexity. Professor Yakovlev, an academician of the IEEE, commented that ldquo; quantitative performance evaluation technology is better than traditional methods. The results have been applied to major tasks such as the country's first unmanned line (Shanghai Line 10) and the docking mission of Tiangong-1 and Shenzhou-8. 4. Realizing a development and verification tool chain that supports the entire software life cycle: Facing the industry's lack of ldquo; efficiently available rdquo; and ldquo; independently controllable rdquo; software development and verification environments, we independently developed a tool chain that supports the entire software life cycle., filling a number of technical gaps, replacing some similar foreign products and surpassing them in several key technical links, tool sales in the past three years have reached 150 million. The project authorized 27 invention patents, obtained 62 soft works, formulated 2 industry standards, published 1 English monograph, and published 60 high-level papers; won 6 awards at or above the provincial and ministerial levels; new sales in the past three years were 1.42 billion yuan., an added profit of 210 million yuan. The first person to complete the project serves as the chief scientist of the major research program of the NSFC, basic research on trusted software, and supports 107 projects from national scientific research institutes, effectively enhancing the international competitiveness of my country's trusted software research and greatly promoting the transformation and application of software trusted technology in the industry.