Verification and online updating of decision making control logic for onboard real-time control systems

The errors during the decision making process in the control system of a modern complex technical system such as a ship, a plane, a spaceship or a power station can lead to unacceptable consequences. Meanwhile, decision making is based on so-named “control logic” described in dedicated specification documents and then implemented by the hardware and software in the real time mode. There are some problems in this process, caused by contradictions and incompletenesses in the specification documents written in natural language, and misunderstanding between specialists in onboard systems, operational engineers, and programmers. In this paper, two practical examples of verification and online updating of spacecraft control logic are described. The approaches we used allow avoiding the mentioned problems. The theoretical basis for verification is Real-Time Control Algorithms Logic RTCAL. Using this, we have developed and successfully applied software tools and domain-specific languages used at the design and operational stages of spacecraft control. The ongoing work includes introducing SMT solvers into our approach, and automatic generation of valid control logic.