On use of Satisfiability Modulo Theories approach for evaluation of Real-Time spacecraft control logic

Abstract

Use of SMT solvers is a very promising modern approach successful in different application domains. The paper is devoted to study how the functionality provided by SMT solver can be utilized for evaluation of key parameters of spacecraft's control logic. The modern spacecraft is a complicated complex of technical complexes should function in consistent matter like an 'orchestra'. Use of SMT in this problem domain is based on formal system of the real-time control and the semantic model of real-time control logic. A Formal specification of real-time control could be feasible or non-feasible on the defined basis of functional tasks (dependable on the parameters of the task, including duration). The feasibility can be checked using SMT approach. As an example, use of Z3 SMT Solver in specially developed Java application through API is discussed.