Design And Implementation Of Formal Verification System Based On Flask

In the field of computer science and software engineering,software engineers use the method of software testing to verify the correctness of computer hardware and software system.Such testing is a conventional way,but sometimes it costs a lot.Engineers will also use formal verification technology to verify the correctness.Formal verification is to verify the correctness of hardware and software system by strict mathematical methods according to some mathematical formal specifications.Based on mathematical logic,it is suitable for most of the software and hardware systems,such as aerospace,medical,artificial intelligence and blockchain systems.This paper comes from the Institute of software research,Chinese Academy of Sciences,and employs experts from foreign well-known universities to lead the project,so as to develop a formal verification tool with independent intellectual property rights.At present,there is a lack of self-developed verification tools for its use in China.In the use of interactive verification system tools developed abroad,users are required to conduct a large number of tedious text coding operations,which makes the cost and time cost of team training and verification operations very high.In the process of participating in the development of the project,the author first clarifies the project requirements,carries out feasibility analysis and clarifies the overall objectives.Secondly,in the outline design,the author designs the overall architecture of the system and the division of each module according to the platform requirements analysis,and draws the relevant flow chart and architecture chart.Based on the outline design,the author Vue.js Framework,hol system design principle,AJAX asynchronous interaction technology,lark parsing tools,etc.are used to design and develop all modules of the system.In the process of developing the main interface of system functions,the author actively collected and learned the latest technical data in related fields.The author has learned and mastered the principle and implementation of Ajax asynchronous interaction technology,and designed and implemented the system logic layer based on flask,which makes the system run more quickly.In the data definition module,according to the hol system principle and hall logic principle,the author designs and implements the computer program to verify the data type.In the data processing module,the author uses lark analysis tool,which makes the process of data analysis and matching accurate and clear.In this verification system,there are five modules:verification interface implementation,verification data interaction,verification datadefinition,verification data processing,and verification data management.The author mainly participated in the realization of verification interface,the definition of proof data,the interaction of proof data and the processing of proof data.At present,the system has been able to complete the basic procedures and theorem verification,later will have other more complete functions to add in.