Computer-aided specification, verification and synshesis of control programmes on the basis of logical and algebraic approaches

Abstract

The paper deals with a complex of problems associated with real-time control program specification, verification and synthesis, carried out aboard a space vehicle. Approaches to solving these tasks on the basis of temporal logic and extended algebra of control processes are analysed. The structure of an instrumental programme complex of control programmes for space vehicles based on the approach proposed is described.