В работе описываются проблемы создания корректных алгоритмов для управления космическими аппаратами. Приводится математическая модель управляющих алгоритмов реального времени, выявляются проблемы верификации требований к ним и определяются возможные методы автоматической верификации....