Verification of the software source code of the spacecraft onboard equipment using temporal logic

The article proposes a method for verifying the source code of the spacecraft onboard equipment software based on the mathematical apparatus of temporal logic. An overview of various software verification methods using deductive proof and model checking is provided. An analysis of the use of the model checking method for software verification at an early stage of the software development process in order to improve quality is given. The aim of the study is to develop a method for verifying the source code of the spacecraft onboard equipment software using temporal logic. Based on the research results, it was found that the existing methods for verifying the onboard equipment software do not fully cover the issues of checking asynchronous or multithreaded versions of software. In order to solve this problem, the authors propose a method for verifying this class of software using temporal logic, and provide restrictions for the main functional software blocks using linear temporal logic formulas. Reliability and quality of software are of great importance for spacecraft. Further evolutionary development of verification methods for the created systems is possible due to the expansion of the use of verification models for various classes of onboard equipment programs, which will improve the quality of the created software.