Research On The Formal Method Of The Relationship Between Aerospace Information Push System Construction And Resource Allocation

China’s aerospace technology is constantly advancing to a high level,and the complexity of information software is deepening,so improving the reliability of information software in the field of aerospace has become an important task.However,in view of the reliable,autonomous and controllable development needs of aerospace information software in China,there is a lack of a complete standard method for software and hardware resource allocation,which makes aerospace information software face problems such as semantic inaccuracy and structural confusion in the process of construction,operation and maintenance,thus causing software failures.Formal method is a method based on strict mathematical theory and abstract system specification.By using formal method to model software and using mathematical theory to verify the reliability of abstract model,ambiguity and errors caused by informal description can be effectively avoided.In view of the above background and research problems,this thesis established a set of formal framework from methods,tools,modeling to verification,and takes the "Aerospace Information Push System" project as the background case to study,aiming at forming a complete set of specifications to ensure the reliability of aerospace information software.The main research work and innovations of this thesis are as follows:(1)Research on the methodology of CPN & Z,a new method of integrated formalization.By integrating Color Petri Net(CPN)and Z method,a new formal method,CPN & Z method,with both static precise semantics and dynamic reliable structure is defined.The correctness of CPN & Z model relative requirements specification is proved by reasoning its post-condition.CPN & Z tool is designed and implemented based on PIPE and Z specification generator,which simplifies graphic editing and text specification in modeling process.An auxiliary modeling method,tree structure(CPN & Z-SV),is proposed,which uses the sub-nodes of the tree to represent different resource states and operation behaviors,and uses the structural topology to represent the relationship between resource states and operation behaviors.It is used to assist the construction of CPN & Z model of the aerospace information push system,realizing the transition from natural language to formal specification language and model,and reducing the difficulty of using CPN & Z method by staff.(2)Research on aerospace information push platform and application of CPN-Z method.According to the recommended national standard(GB / T)and the national military standard(GJB),the aerospace information push system is studied in depth,and the system construction framework including the composition structure,environmental configuration,interface and key technologies is summarized.The content of the framework is analyzed and designed.For high concurrency,three-dimensional display of space objects,data and computing persistence technology solutions;aiming at the complex problem of the components of the system visualization module,the three key elements of ’ user set,scene set and data set ’ are taken as the focus to avoid the missing elements.The CPN & Z method is used to model the above content,which solves the ambiguity problem and unclear structure in the process of demand analysis and design.At the same time,it provides the basis for the realization of the system and provides a model case for the subsequent verification work.(3)Verification of the rationality about the aerospace information push system model and implementation of the Aerospace Information Push System.Combined with the basic properties of ordinary network model and the concept of rationality of formal model,the conditions to meet the rationality of CPN & Z model are proposed.Based on the reachability tree and correlation matrix,the proof strategies for the rationality verification of CPN & Z model are proposed respectively,and the reachability tree and correlation matrix of CPN & Z model,the visualization module of aerospace information push system,are constructed.The results show that the visual module CPN & Z model reachable tree M0 can reach the new mark state through different paths,and the initial mark resource can directly or indirectly trigger any behavior operation.The element values of all leaf nodes in the tree are 1 or 0,and no other values appear.When the correlation matrix value of the CPN & Z model of the visualization module is less than 0,the subvector of any To＿vector has a value greater than or equal to 0,and the correlation matrix W can express the relationship between all resource state elements and behavioral operation elements.Based on the above research,it is proved that the CPN & Z model of the system visualization module is reasonable.The research has been used in China’s space projects to provide support for space debris monitoring missions.Finally,this thesis describes the implementation of some functions of the Aerospace Information Push System,which provideed examples to prove the correctness and rationality of all the methods and models in this thesis,and achieved the desired goal.