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

АВТОРЕФЕРАТ диссертации на соискание ученой степени доктора технических наук Синтез и верификация управляющих алгоритмов реального времени для бортовых вычислительных систем космических аппаратов по специальности 05.13.12 - Системы автоматизации проектирования Работа выполнена на кафедре компьютерных систем ГОУ ВПО «Самарский государственный аэрокосмический университет имени академика С.П. Научный консультант доктор технических наук, профессор А.А. Защита состоится 9 ноября 2007 г. в ____ часов на заседании диссертационного совета Д 212.215.05 в конференц-зале ГОУ ВПО «Самарский государственный аэрокосмический университет имени академика С.П.На них возлагаются задачи контроля работоспособности бортовой аппаратуры (БА), управления движением КА и навигации, выдачи управляющих воздействий на БА при решении КА целевых задач и др. Расширение спектра выполняемых на борту КА задач привело к созданию сложных структурированных комплексов БПО объемом в сотни тысяч и миллионы команд. При управлении изделиями космической техники одной из важнейших является также проблема обеспечения безопасности, напрямую связанная с надежностью и качеством БПО. Среди ошибок БПО значительное количество приходится на сбои синхронизации и согласования логики управления БА при одновременном функционировании ряда бортовых систем и программ БПО в рамках решения КА целевых задач (ошибки в управляющих алгоритмах реального времени - УА РВ). При этом даже в новейших расширениях упомянутых методов, имеющих некоторые возможности описания систем реального времени (UML2.0), построение логической структуры программы возлагается на разработчика, т.е. синтез УА РВ не предусматривается. вычислительный автоматизация космический программаПоскольку особую важность при этом имеет синхронизация, т.е. корректное согласование работы приборов БА и программ БПО во времени, в состав БВС и бортовой операционной системы включаются соответствующие механизмы. На этой основе разработчик УА РВ формирует таблицу условий (глобальных переменных), определяющих необходимость выполнения алгоритмом тех ли иных действий, и затем вручную строит временную диаграмму алгоритма (документ, отражающий логико-временную схему УА). Затем в диссертации строится многоосновная алгебраическая система УА РВ: АУА = , основными множествами (носителями) которой являются: UA - множество УА РВ в виде наборов кортежей (1), LV - множество логических переменных {ak}, Z?0 - множество моментов времени (неотрицательные целые числа, соответствующие возможным показаниям дискретного бортового датчика времени КА). Отношение СК имеет место, если два УА РВ завершаются в одно и то же время, отношение ® - если непосредственно в момент завершения выполнения некоторого алгоритма начинается выполнение другого управляющего алгоритма. Добавление в описание множества неотрицательных целых чисел Z?0 позволяет расширить алгебраическую систему УА РВ операциями, аргументами которых будут, с одной стороны, элементы множества УА РВ, а с другой - числа из Z?0: Н (T1, T2, x) - операция над алгоритмами и числом x, означающая наложение выполнения T2 на выполнение T1, со сдвигом начала выполнения T2 по отношению к T1, равным x.2.Построен формальный математический аппарат для описания УА РВ, в том числе впервые построена модель семантики УА РВ с адекватным отражением их временных и логических аспектов в виде набора кортежей, описывающих выполнение функциональных задач в заданные моменты времени: 3.Разработаны языки и средства формальной спецификации УА РВ, в том числе с применением визуального конструирования. •методы и средства параметрической генерации управляющей программы, реализующей требуемую семантику УА РВ, на целевом языке программирования (включая ассемблер БЦВМ и язык Си). 5.Сформулированы критерии, предложены методы выбора проектных решений при синтезе УА РВ (структурной оптимизации) и проведено исследование их эффективности, в том числе: •методов эквивалентных преобразований спецификаций УА РВ; Таким образом, в диссертации решена актуальная научная проблема, имеющая важное народнохозяйственное значение - проблема сокращения сроков и трудоемкости разработки, повышения надежности и качества УА РВ для БВС КА на основе разработки формального математического аппарата, методов и средств синтеза и верификации УА РВ в рамках автоматизированной технологии, поддерживаемой инструментальным программным комплексом. Разработанные в диссертации модели, методы синтеза и верификации УА РВ, инструментальный программный комплекс могут использоваться в различных отраслях народного хозяйства, в которых встает задача управления сложными техническими системами в реальном времени - таких, как телекоммуникации, транспорт, энергетика, химические и нефтехимические производства, и т.п.

ОСНОВНОЕ СОДЕРЖАНИЕ РАБОТЫ