В работе описываются проблемы создания корректных алгоритмов для управления космическими аппаратами. Приводится математическая модель управляющих алгоритмов реального времени, выявляются проблемы верификации требований к ним и определяются возможные методы автоматической верификации.
В мире научных открытий. 2010. № 4-11. С. 62-64. ISSN 2072-0831

доклад о верификации требований
Труды международного симпозиума "Надежность и качество". 2009. Т. 1. С. 42-43.ISSN 2220-6418

о верификации требований к управляющим алгоритмам реального времени с проверкой выполнимости и непротиворечивости
сб.докладов международного симпозиума "Надежность и качество". 2010. Т. I. С. 54-55. ISSN 2220-6418

Рассматривается комплекс проблем спецификации, верификации и синтеза управляющих программ реального времени, исполняемых на борту космического аппарата. Анализируются подходы к решению этих задач на основе временной логики и применения расширенной алгебры управляющих процессов. Описывается структура основанного на приведенном подходе инструментального программного комплекса разработки управляющих программ для космических аппаратов.
Мехатроника, автоматизация, управление. 2007. № 7. С. 46-51.

доклад
сб. [науч.] тр. X Всерос. науч. -техн. семинара по упр. движением и навигации летательных аппаратов (Самара, 26-27 июня 2001г.) / Самар. гос. аэрокосм. ун-т им. С. П. Королева, Гос. науч. -произв. ракет.-косм. центр "ЦСКБ - Прогресс" и др. - Самара, 2002. - С. 156-159 . - ISBN 5-93424-060-9

верификация управляющих алгоритмов методом логического вывода
Сборник трудов Международного семинара "Семантика, спецификация и верификация программ: теория и приложения" Казань, 2010. С.117-123

Описание
Известия Российской академии наук. Теория и системы управления. 2006. № 2. С. 128-141.

по заказу ГНПРКЦ "ЦСКБ-Прогресс"
Полет. Общероссийский научно-технический журнал Декабрь 2005

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

Предложен метод верификации протоколов информационного обмена на основе использования Е-сетей и формальных грамматик. Метод позволяет уменьшить размерность модели, тем самым уменьшая эффект «комбинаторного взрыва».
Дуравкин Евгений Владимирович, Коровченко Елена Борисовна Формализация поведения протоколов информационного обмена, представленных моделями на основе аппарата Е-сетей // Проблеми телекомунікацій, Vol. 2011, Issue 1, 2010, pp. 28-38