| In recent years,with the rapid development of information technology,automatic control theory,artificial intelligence technology and the increasing demand,the research and production of unmanned system has attracted the attention and support of many coun-tries.The research results of unmanned systems are widely used in military and civil fields.As an extension of human sensory and behavioral capabilities,the research,devel-opment and application of unmanned systems greatly liberate people’s productivity and avoid unnecessary personnel losses in high-risk work to a great extent.The development of unmanned system is of great significance to a country’s high-tech industry,intelligent economy industry and national living standards.However,in practical application,the execution environment of unmanned system is complex and changeable.Unmanned system itself is also an cyber physical system with complex software and hardware.How to ensure system reliability is an inseparable prob-lem of unmanned system development.As the brain of unmanned system,the reliability and security of control program is the top priority of unmanned system security.The func-tion of the control program is to guide the unmanned system to make real-time decisions in complex external environment,and guide the system to make appropriate behavior to complete the goals of the system.In traditional methods,the control program is manually written by designers,and the complete process of program design,writing,debugging and deployment is cumbersome and error prone.In recent years,with the development of automatic program generation method,the application of program synthesis theory based on formal method in automatic program generation of unmanned system control has also attracted the attention of many researchers.The reactive system model in the formal method can be well combined with un-manned system,but the existing control program synthesis methods still have the prob-lems of single specification mode,insufficient ability to deal with complex dynamic en-vironment and high possibility of unsynthesizable.In order to improve the reliability of unmanned system in complex environment,we study the automatic generation method of unmanned system control program.Aiming at unsynthesizable specification problem in specific scenarios with the characteristics of multi-system dependence and unexpected changes,this paper puts forward a set of theory,technology and framework of specifica-tion,program synthesis and evolution for unmanned system control program generation,and studies the cases with practical background to illustrate the effectiveness of the work in this paper.On the one hand,the work of this paper can effectively prevent the hidden dangers in the control program of unmanned system and improve the reliability in the pro-cess of system operation.On the other hand,it can effectively deal with the uncertainty and security threats brought by complex environment,so that unpredictable external at-tacks and abnormal operations in the development process can be prevented outside the set of security behaviors.Specifically,the research content and innovation of this paper are divided into the following aspects:(1)Iterative control program synthesis for multi-robot system.In the scenario of multi-system,the behavior description of other systems in the system requirements specification is often cumbersome.The incompleteness of the specification description will lead to the increase of the comprehensive complexity of the control program,and in serious cases,the specification can not be synthesized.In order to improve the efficiency and success rate of control program synthesis,this paper establishes the dependency rela-tionship between unmanned systems in multi-system scenario,and studies how to extract effective information from the generated system security control program and automat-ically generate the environmental constraints of the system,so that the control program can be generated more easily? The dependency graph of multiple systems is established,the nodes in the graph are divided into strongly connected components,and the process of information extraction and specification generation within and between components is effectively organized to ensure the optimality of each system security control program.(2)Hierarchical specification based on security requirements.In the traditional control program synthesis method,the specification is static and not hierarchical,which makes the specification often accompanied by unsynthesizable problems in a dynamic and complex environment.In order to improve the work efficiency of specification designers and improve the adaptability of unmanned system in complex and changeable environ-ment,the system specification is divided hierarchically according to the security level.Based on different security requirements,the system specification is divided into high security part and low security part,so that the synthesized control program can strictly meet the high security specification.At the same time,low security specification is fully utilized in the process of control program synthesis.(3)Control program synthesis for hierarchical specification.After the traditional specification is divided according to the security level,the traditional control program synthesis algorithm will no longer be applicable.In order to make the hierarchical speci-fication can be effectively and fully utilized and synthesized to obtain an effective control program,this paper studies the characteristics of unsynthesizablity,and combined with the calculation method of the minimum unsynthesizable set of the specification,a com-prehensive calculation method of the control program for the hierarchical specification is proposed from two ideas: on the basis of strictly meeting the high security requirements,finding the largest subset of low security specification that can synthesize the control pro-gram? firstly,an control model satisfying the high security specification is synthesized to guide the system to reach the winning state on the premise that some low security spec-ification are allowed to be violated,and then the behavior is executed according to the guidance of the control model strictly satisfying the complete specification.(4)Generation and evolution of control program for unmanned system.The traditional program synthesis method has poor dynamic adaptability to environmental changes.When the environmental changes exceed the scope described by the existing regulations,the winning strategy generated by the environment and system game may make the system unable to be effectively followed up,resulting in that the security con-trol program based on this strategy will no longer be able to strictly ensure that it meets the security nature.This paper puts forward the method of specification evolution and re-synthesis of security control program for environmental change,studies the specification evolution method when some propositions fail,and puts forward corresponding counter-measures to complex environmental changes such as map topology information change combined with automation methods such as runtime verification and specification learn-ing.Combined with the research contents of synthesis for hierarchical specification and iterative synthesis for multi-robot system,the method of control program re-synthesis is proposed. |