| The space embedded operating system is the necessary basic software of the space aircraft,which determines whether the space vehicle can complete the space flight mission reliably and securely.At present,various means have been adopted to ensure their reliability and security,but there are still some undiscovered defects.The formal verification method has been well applied in some industrial fields,and the reliability and security of the verified systems are much higher than the unverified system.Therefore,the use of formalized method to verify the space embedded operating system is imperative to ensure its correctness and make it more reliable and secure.The storage subsystem is an important part of the space embedded operating system,including memory management and file management.Among them,memory management is a key part of the operating system kernel.It is an inherent requirement of the space embedded operating system to ensure its reliable and secure operation.In addition,more and more data are generated by space missions,and file system is needed in the space embedded operating system.Therefore,it is necessary to develop a reliable and secure file system for space applications.This dissertation takes the space embedded operating system Space OS2 as the object to study the embedded storage subsystem for space applications.The research work is summarized in the following three aspects.(1)Aiming at the problem of how to verify the requirement,design and implement of complex software,this dissertation first uses mathematical methods to prove that adopting the three-layer verification framework can significantly reduce the workload of verification.Then,a specific verification method is proposed for each layer.For the requirement layer,this dissertation proposes a formal verification method of system instantiation.For the design layer,a formal verification method based on the property of global variables is proposed for the design flow chart.For the implement layer,an operation-oriented formal verification method is proposed for the specific implementation code.(2)Under the three-layer verification framework of " requirement-design-implement",the formal verification research of the memory management module of Space OS2 is carried out.In the requirement layer,a formal verification method of memory state based on induction and deduction is proposed to solve the problem that the memory state is too large and difficult to verify.We extract the invariant properties in the process of memory state transformation,and use the inductive mathematical form to calculate the changes between memory states.And we complete the verification works in requirement layer by proving that the properties of memory states are satisfied before and after memory operations,so as to avoid verifying the correctness of all memory states one by one.The design layer and the implement layer use the corresponding proof method to complete the formal verification work respectively.(3)Aiming at the problem of how to develop a reliable and secure file system,this dissertation applies the "requirement-design-implement" hierarchical verification framework,and adopts the method of verification while design to realize a file system dedicated to the space operating system.In addition,in order to solve the problem that the flash memory file system occupies too much memory space,this dissertation proposes a task-based fine-grained file directory index method,and the file data inverse linked list index method based on the single linked list structure.Through those methods,we reduce the memory occupancy of the flash memory file system,and form a task-oriented space dedicated flash memory file system. |
PDF Full Text Request