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

Размещено на http://allbest.ru

На правах рукописи

АВТОРЕФЕРАТ

диссертации на соискание ученой степени

доктора технических наук

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

по специальности 05.13.12 - Системы автоматизации проектирования

(в машиностроении)

Тюгашев Андрей Александрович

Самара - 2007

Работа выполнена на кафедре компьютерных систем ГОУ ВПО «Самарский государственный аэрокосмический университет имени академика С.П. Королева»

Научный консультант

доктор технических наук, профессор А.А. Калентьев

Официальные оппоненты:

доктор технических наук, профессор Н.А. Северцев

доктор технических наук, профессор Б.Е. Федунов

доктор технических наук, профессор А.Н. Коварцев

Ведущая организация: ФГУП «Научно-производственное объединение имени Лавочкина»

Защита состоится 9 ноября 2007 г. в ____ часов на заседании

диссертационного совета Д 212.215.05 в конференц-зале ГОУ ВПО «Самарский государственный аэрокосмический университет имени академика С.П. Королева» по адресу: г. Самара, Московское шоссе, 34.

С диссертацией можно ознакомиться в библиотеке ГОУ ВПО «Самарский государственный аэрокосмический университет имени академика С.П. Королева».

Автореферат разослан «___»_________ 2007 г.

Ученый секретарь диссертационного

совета, д.т.н., профессор А.А. Калентьев

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

Актуальность темы. Ключевую роль при управлении современными космическими аппаратами (КА) играют бортовые вычислительные системы (БВС), в состав которых входят одна или несколько бортовых цифровых вычислительных машин (БЦВМ). На них возлагаются задачи контроля работоспособности бортовой аппаратуры (БА), управления движением КА и навигации, выдачи управляющих воздействий на БА при решении КА целевых задач и др. Функции управления реализуются при этом бортовым программным обеспечением (БПО). Расширение спектра выполняемых на борту КА задач привело к созданию сложных структурированных комплексов БПО объемом в сотни тысяч и миллионы команд. В настоящее время создание и отладка БПО является одним из наиболее трудоемких и длительных видов работ среди всех видов деятельности, связанных с созданием КА.

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

Понятия качества и надежности программных средств (ПС) определяются международным (ISO 9126:1-4) и российскими (ГОСТ 28195-89, ГОСТ 28806-90) стандартами, где они задаются набором общих и детальных характеристик. Качество ПС определяется как его важнейшее свойство, характеризуемое несколькими группами показателей. При этом надежность рассматривается как одна из важнейших характеристик качества ПС наряду с корректностью (соответствием спецификации), эффективностью (временной эффективностью и использованием ресурсов), сопровождаемостью и переносимостью. Надежность, в свою очередь, определяется «уровнем завершенности (отсутствия ошибок)», устойчивостью и восстанавливаемостью.

Среди ошибок БПО значительное количество приходится на сбои синхронизации и согласования логики управления БА при одновременном функционировании ряда бортовых систем и программ БПО в рамках решения КА целевых задач (ошибки в управляющих алгоритмах реального времени - УА РВ).

Основными используемыми в настоящее время методами обеспечения надежности УА РВ для БВС КА являются тестирование и отладка, которые, однако, не могут гарантировать отсутствия ошибок. При этом, в связи с необходимостью отработки взаимодействия с БА при всех возможных ситуациях на борту КА (в т.ч. нештатных), их трудоемкость является наибольшей среди этапов жизненного цикла (ЖЦ) БПО и составляет, по экспертным оценкам, около 57% общей трудоемкости. Вследствие этого проблемы обеспечения надежности и сокращения сроков и трудоемкости разработки БПО оказываются неразрывно связанными.

Одним из наиболее эффективных методов повышения качества и надежности БПО является создание средств автоматизации проектирования и отладки программ. Значимый вклад в разработку теоретических основ такой автоматизации применительно к ПО реального времени внесли такие ученые, как Е.А. Микрин, В.А. Крюков, В.В. Липаев, А.К. Петренко, Я.А. Мостовой, А.А. Калентьев, Р.Л. Смелянский, Г. Хольцманн и др.

На большинстве предприятий ракетно-космической отрасли в нашей стране (ракетно-космической корпорации «Энергия» имени С.П. Королева, ГНПРКЦ «ЦСКБ-Прогресс», НПО имени Лавочкина и др.) и за рубежом используются средства автоматизации отдельных этапов ЖЦ БПО. При этом с целью снижения количества ошибок в программах и повышения производительности труда разработчиков практикуется применение языков программирования высокого уровня и специально разрабатываемых проблемно-ориентированных языков. Так, при создании программного обеспечения космической системы Space Shuttle был разработан язык программирования высокого уровня HAL/S, имеющий в своем составе, помимо иных специальных возможностей, средства для реализации управления в реальном времени. В Институте прикладной математики имени Келдыша при проектировании БПО многоразового космического корабля «Буран» были разработаны специализированные языки ПРОЛ2 и СИПРОЛ. Кроме того, используется комплексная отладка программ БПО совместно с программами моделей бортовой аппаратуры и факторов космического пространства, на специальном испытательном стенде.

Однако, перечисленные подходы ориентированы на верификацию уже созданных в рамках той или иной технологии программ и оставляют «за скобками» решение задач обеспечения корректности исходных требований к БПО и формальной верификации (доказательства) УА РВ.

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

Еще больший интерес представляет разработка методов автоматизированного синтеза УА РВ, которые при этом гарантировали бы его корректность (соответствие спецификации). Важным преимуществом метода автоматизированного синтеза является также его инвариантность относительно используемого языка программирования и архитектуры БВС, что обеспечивает возможность быстрого перехода на новые БЦВМ и средства программирования при разработке перспективных КА.

Для спецификации и формальной верификации динамических управляющих систем в мире применяются подходы, основанные на темпоральной логике (в этой области известны работы А. Пнеули, З. Манна, А. Морценти, Д.В. Царькова, А. Эмерсона и др.), а также алгебры процессов (CCS Р. Милнера, CSP Э.Хоара, ACP Я. Бергстры и В. Клопа и др.), и графовые модели (в основном представленные различными разновидностями сетей Петри). В качестве модели семантики в темпоральных логиках обычно применяются модель Крипке или таймированные автоматы, основанные, как и сети Петри, на концепции состояний. Их использование применительно к исследованию реальных управляющих систем затруднено в связи с проблемой взрывного роста числа состояний, подлежащих моделированию. Говоря об известных алгебрах процессов, можно отметить, что имеющиеся в них операции в недостаточной степени соответствуют требованиям согласования работы бортовой аппаратуры во времени и с точки зрения логики управления. Кроме того, алгебры процессов, как правило, не ориентированы на решение задачи автоматизированной генерации управляющей программы.

Общим вопросам автоматизации различных этапов жизненного цикла ПО (CASE-средств) посвящены работы Г. Буча, Э. Хоара, Д. Румбаха, В.М. Глушкова, А.П. Ершова, С.С. Лаврова, В.В. Липаева, И.В. Вельбицкого, Г.Н. Калянова, А.Н. Коварцева, А.М. Вендрова и других ученых. В индустрии ИТ разработаны и широко используются комплексные методологии разработки программных средств (IBM Rational Unified Process, основанный на языке UML - Unified Modeling Language, Borland ALM, Microsoft Solutions Framework). При спецификации требований к телекоммуникационным системам используются специализированные языки SDL, LOTOS и др. Однако, возможности данных средств недостаточны для описания специфических свойств УА РВ для БВС КА. При этом даже в новейших расширениях упомянутых методов, имеющих некоторые возможности описания систем реального времени (UML2.0), построение логической структуры программы возлагается на разработчика, т.е. синтез УА РВ не предусматривается. вычислительный автоматизация космический программа

Таким образом, создание методов и средств автоматизации синтеза и верификации УА РВ для БВС КА является весьма актуальной задачей. Верификация означает проверку УА РВ на наличие у него требуемых свойств, которые при этом должны быть точно специфицированы. Поскольку спецификация должна быть непротиворечивой (а для случая управляющих алгоритмов, согласовывающих работу большого числа приборов и систем КА, обеспечение этого является самостоятельной непростой задачей), весьма актуальна и разработка методов верификации самих спецификаций. Решение задачи синтеза УА РВ также связано с необходимостью точной спецификации требований. Для этого требуется однозначное определение семантики УА РВ. Следует отметить, что при синтезе УА РВ одна и та же семантика может быть реализована алгоритмами с разной логико-временной структурой (схемой), и различными управляющими программами, что создает пространство выбора проектных решений, варьируя которыми можно управлять эффективностью получаемой программы. Таким образом, цепочка преобразований УА РВ при его автоматизированном синтезе выглядит как:

спецификация > семантика УА РВ > логико-временная схема алгоритма > управляющая программа.

В настоящее время существует ряд формализаций семантики программных средств, в основном относящихся к одному из трех направлений - операционному, аксиоматическому (деривационному) и денотационному. Существенный вклад в их развитие внесли такие ученые, как Дж. Мак-Карти, Г. Бекик, М. Маркотти, Д. Кнут, Р. Флойд, Э. Хоар, Д. Скотт, Я. де Баккер, С.С. Лавров и др. Однако, упомянутые формализации семантики в основном ориентированы на вычислительные программы. При этом они обычно интерпретируются в рамках фон-неймановской императивной модели вычислений. В связи с этим данные модели не могут адекватно описать УА РВ для БВС КА, основным содержанием которых является выдача в требуемое время команд управления на БА и запуск функциональных программ БПО в соответствии с требованиями целевой задачи и складывающейся на борту ситуацией.

Все вышеперечисленное обуславливает актуальность выбранной тематики диссертации, посвященной разработке формального математического аппарата для описания УА РВ и на этой основе - методов и средств их автоматизированного синтеза и верификации.

Объектом исследования в диссертационной работе являются управляющие алгоритмы реального времени для БВС КА, координирующие комплексное (согласованное во времени и с точки зрения логики управления БА) функционирование систем бортовой аппаратуры и программ комплекса БПО космического аппарата при решении им целевых задач.

Целью диссертационной работы является сокращение сроков и трудоемкости разработки, повышение надежности и качества управляющих алгоритмов реального времени для БВС КА на основе построения формального математического аппарата, методов и средств синтеза и верификации УА РВ, в том числе специального программного комплекса, обеспечивающего эффективную инструментальную поддержку процессов их проектирования и разработки.

Задачи исследования вытекают из поставленной цели и включают:

1.Исследование существующих подходов к синтезу и верификации динамических управляющих систем.

2.Построение формального математического аппарата для представления УА РВ, адекватно описывающего их как сложные объекты, обладающие временными и логическими аспектами.

3.Разработку средств формальной спецификации УА РВ для БВС КА.

4.Создание методов и средств синтеза УА РВ, включая построение логико-временной схемы алгоритма и генерацию управляющей программы на параметрически задаваемом целевом языке программирования.

5.Разработку и анализ эффективности методов выбора проектных решений при автоматизированном синтезе УА РВ.

6.Разработку методов и средств верификации УА РВ на различных этапах жизненного цикла.

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

Научная новизна (личный вклад автора) работы заключается в следующем:

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

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

3.Построена формальная теория управляющих алгоритмов, позволяющая осуществлять спецификацию УА РВ, проводить их исследование и верификацию методами логического вывода и проверки на модели (model checking).

4.Разработан метод автоматизированного построения логико-временной схемы УА РВ, обеспечивающий гарантированное соответствие алгоритма заданной спецификации.

5.Разработаны методы и средства генерации управляющей программы, реализующей УА РВ, на параметрически задаваемом языке программирования.

6.Предложены методы структурной оптимизации УА РВ при его автоматизированном синтезе, обеспечивающие повышение его эффективности за счет уменьшения требований к ресурсам БВС.

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

Практическая ценность работы состоит в том, что:

1.Разработанные модели, методы и инструментальный программный комплекс позволяют снизить трудоемкость и сократить сроки разработки УА РВ для БВС КА на 20-30%, повысить их надежность и качество.

2.Практическую значимость имеют следующие методы решения частных проектных задач:

*метод визуального конструирования семантики УА РВ;

*метод визуального конструирования логико-временной схемы алгоритма;

*методы и средства автоматизированного синтеза УА РВ и генерации управляющей программы;

*методы и средства построения таблицы вариантов УА РВ и генерации отладочных заданий для каждого варианта.

3.Разработанная технология применима не только для синтеза и верификации бортовых управляющих алгоритмов, но и при создании программ моделей систем БА, используемых на этапе комплексных испытаний КА.

Апробация работы проводилась в ходе выступлений и обсуждений на 31 научно-технической конференции, семинарах и симпозиумах, включая Всесоюзные Туполевские чтения (г. Казань, 1990 г.), Гагаринские чтения (г. Москва, 1991, 1992 и 2001 гг.), Всероссийскую научную школу по компьютерной алгебре, логике и интеллектному управлению (г. Иркутск, 1994 г.), 5-ю межвузовскую научную конференцию по математическому моделированию и краевым задачам (г. Самара, 1995 г.), 1-ю Поволжскую научно-техническую конференцию по научно-исследовательским разработкам и высоким технологиям двойного применения, VII, VIII, IX, X, XI и XII Всероссийские семинары по управлению движением и навигации летательных аппаратов (г. Самара, 1995, 1997, 1999, 2001, 2003, 2005 гг.), Международные научно-технические конференции и симпозиумы «Актуальные проблемы анализа и обеспечения надежности и качества приборов, устройств и систем» и «Надежность и качество» (г. Пенза, 1995, 1996, 1999, 2001, 2003, 2004, 2007 гг.), научную конференцию по перспективным информационным технологиям, посвященную 20-летию факультета информатики СГАУ (г. Самара, 1995 г.), Международную космическую конференцию, посвященную 40-летию первого полета человека в космос «Космос без оружия - арена мирного сотрудничества в XXI веке» (г. Москва, 2001 г.), 8-ю, 9-ю 10-ю и 11-ю Международные научно-технические конференции «Системный анализ и управление аэрокосмическими комплексами» (г. Евпатория, 2003-2006 гг.).

Реализация результатов связана с использованием:

-Технологии автоматизации синтеза и верификации бортовых управляющих алгоритмов в ходе работ над перспективными космическими аппаратами в Государственном научно-производственном ракетно-космическом центре «ЦСКБ-Прогресс». Работа выполнялась в рамках хоздоговоров с ЦСКБ (1994-2005 гг.), ее результаты отражены в 14 научно-технических отчетах, подготовленных либо автором лично, либо при его непосредственном участии. Результаты внедрены на предприятии, что отражено в Приложении к диссертации.

-Методов разработанной автоматизированной технологии при построении программы модели бортовой телеметрической системы, используемой при комплексных испытаниях на наземном отладочном стенде, в ГНПРКЦ «ЦСКБ-Прогресс».

-Разработанных моделей, концепций и методик в учебном процессе Самарского государственного аэрокосмического университета имени академика С.П. Королева в курсах «Математические модели объектов авиационно-технической техники», «Языки программирования», в курсовом и дипломном проектировании, учебно-исследовательской работе студентов.

Научные результаты диссертационной работы являются обобщением научно-производственной деятельности диссертанта в период 1988-2007 гг.

Публикации. По материалам проведенных исследований опубликовано 57 работ, включая монографию, 35 статей в центральных и региональных научных журналах и сборниках научных трудов (в том числе девять публикаций в изданиях, рекомендуемых ВАК), а также тезисы докладов научно-технических конференций. 23 работы выполнены автором единолично.

Структура и объем диссертации. Диссертация состоит из введения, пяти глав, заключения и приложений. Общий объем работы 312 страниц машинописного текста, включая 59 рисунков, список использованных источников содержит 215 наименований.

На защиту выносятся:

1.Математический аппарат для описания управляющих алгоритмов реального времени, в том числе модель семантики УА РВ, логико-временная схема и многовариантная модель УА РВ.

2.Алгебраический подход к УА РВ, обеспечивающий конструктивное построение и исследование УА РВ с использованием операций и предикатов многоосновной алгебраической системы УА РВ.

3.Формальная теория УА РВ и ее применение в качестве средства спецификации и верификации важнейших свойств УА РВ.

4.Методы и средства автоматизированного синтеза логико-временной схемы УА РВ и параметрической генерации текста управляющей программы на заданном языке.

5.Методы выбора проектных решений при синтезе УА РВ для БВС КА.

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

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

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

На современных космических аппаратах функции управления и контроля работоспособности БА возлагаются на бортовое программное обеспечение. При решении КА целевых задач на одном отрезке времени согласованно должны функционировать различные системы, приборы и агрегаты бортовой аппаратуры. Поскольку особую важность при этом имеет синхронизация, т.е. корректное согласование работы приборов БА и программ БПО во времени, в состав БВС и бортовой операционной системы включаются соответствующие механизмы. Таким образом, УА РВ для БВС КА представляют собой динамическую управляющую систему реального времени.

В диссертации представлен обзор современного состояния моделей подобных систем, используемых при решении задач их спецификации и верификации. В настоящее время наиболее широко применяются подходы, основанные на временномй (темпоральной) логике, алгебрах процессов (CCS, CSP, ACP), и сетях Петри. Рассмотрено развитие данных методов, начиная с их зарождения в середине 1960-х годов XX века, проведен анализ присущих им особенностей и ограничений. На основе анализа трудов Х.Б. Керри, Г. Бекика, В.М. Глушкова, Р. Милнера, Э. Хоара, К. Петри, Я. Бергстры, А. Пнуели, З. Манны проведена классификация существующих подходов. Показано их несоответствие без соответствующей модификации задачам синтеза и верификации управляющих алгоритмов реального времени для БВС КА.

Создание комплекса программ БПО для современных космических аппаратов представляет собой сложный процесс с большим количеством участников. Организационный сетевой график работ включает в себя сотни ключевых вершин, часто в нем содержится критический путь графика работ по созданию КА в целом. В разработке задействуются десятки алгоритмистов и программистов, как создающих программы управления конкретной бортовой аппаратурой, так и разрабатывающих алгоритмы комплексного функционирования, обеспечивающие согласованную работу ряда систем и подсистем КА в рамках решения важных целевых задач (УА РВ).

При традиционном методе в качестве исходных данных для построения УА РВ используется описание логики управления подсистемами КА и требуемых временных соотношений на естественном языке, например: «При проведении операции O1 система С1 должна быть приведена в исходное состояние выдачей команд К1,..,К5. Перед пуском КА необходимо после выполнения программы П2 проверить условия A1,A2. В случае ложности условия A1 необходимо осуществить переход в режим нештатной работы вызовом программы П11.

В случае ложности A2 необходимо повторно вызвать программу П2 для формирования массива X. Непосредственно перед моментом t0 необходимо обеспечить функционирование П1. За 360 сек до t0 требуется включить режим Р0 системы С1. При этом необходимо обеспечить выполнение ограничений: интервал между выдачей команд К2,..,К5 должен быть не менее 1 сек. Интервал между К1 и К2 составляет не менее 2 мин». На этой основе разработчик УА РВ формирует таблицу условий (глобальных переменных), определяющих необходимость выполнения алгоритмом тех ли иных действий, и затем вручную строит временную диаграмму алгоритма (документ, отражающий логико-временную схему УА). Затем он осуществляет написание и отладку управляющей программы, реализующей временную диаграмму, на заданном языке программирования. При этом ответственность за непротиворечивость исходных требований, за соответствие формируемой логико-временной схемы алгоритма спецификации и за корректность управляющей программы ложится на человека.

В настоящее время срок разработки комплекса БПО для нового космического аппарата составляет от двух до четырех лет (из них 44% приходится на этапы анализа требований и проектирования). Самым трудоемким является обеспечение требуемого уровня надежности бортовых программ, в основе которого лежит многоэтапное тестирование.

На основании этого в качестве актуальных задач, возникающих при разработке управляющих программ, выделены автоматизация процесса формирования требований (спецификации), разработка методов формальной верификации, позволяющих, в отличие от тестирования и отладки, строго доказывать соответствие программы требованиям аналитическими средствами, создание методов автоматизированного синтеза УА РВ, гарантированно соответствующего спецификации. Решение перечисленных задач, в свою очередь, требует построения модели семантики УА РВ.

Приведен обзор существующих методов описания семантики программ. Наиболее общий характер, абстрагированный от деталей реализации, имеет аксиоматическая модель семантики (Флойд, Хоар). Поэтому с точки зрения описания семантики УА РВ наибольший интерес представляет именно это направление. Однако в своем традиционном виде аксиоматическая семантика направлена на описание последовательных вычислительных программ, что не соответствует предметной области УА РВ для БВС КА, где основным содержанием алгоритма являются не вычисления, а своевременная выдача управляющих воздействий на бортовую аппаратуру.

Делается вывод о том, что решение задач синтеза и верификации УА РВ для БВС КА возможно на основе построения модели семантики УА РВ и ее использования совместно с соответствующим образом адаптированными и интегрированными принципами алгебраического и логического подходов.

Во второй главе строится формальный математический аппарат для описания УА РВ, и на этой основе - методы и средства синтеза и верификации УА РВ для БВС КА.

В отличие от вычислительных программ, применительно к УА РВ для БВС КА, с одной стороны, неправильно вести речь об исходных данных, не претерпевающих изменений в процессе исполнения программы. С другой стороны, о корректности работы УА РВ недостаточно судить по состоянию программной памяти в момент его завершения. Основной функцией УА РВ является реализация требуемых управляющих воздействий в заданные моменты времени, в зависимости от решаемой целевой задачи и текущего состояния КА и внешней среды.

Модель семантики УА РВ может быть построена как набор кортежей (четверок) Фi:

(1)

где fi - идентификатор функциональной задачи (ФЗ); ti - момент начала выполнения ФЗ (целое неотрицательное число); ?i - длительность ФЗ (целое неотрицательное число); - логический вектор, обуславливающий ФЗ.

Каждый кортеж Фi описывает одно действие (функциональную задачу), производимое управляющим алгоритмом. Фi обычно подразумевает работу какого-то прибора или агрегата, входящего в состав БА, или выполнение функциональной программы из комплекса БПО. При этом функциональная задача может выполняться не мгновенно, а на протяжении интервала времени ti, начиная с момента ti. Осуществление тех или иных действий не носит безусловного характера, а должно соответствовать текущей ситуации на борту КА, которая описывается набором значений логических переменных <a1,…ak>, формирующих логический вектор. Таким образом, выполнению ФЗ в момент времени ti сопоставляется логический вектор, обуславливающий данное действие. Значение каждой из логических переменных (ЛП), обуславливающих выполнение ФЗ, принадлежит множеству {1, 0, Н}. Здесь 1 обозначает ИСТИНУ, 0 - ЛОЖЬ, Н в соответствующей компоненте логического вектора подразумевает, что выполнение ФЗ не зависит от значения данной логической переменной. По своему смыслу логические переменные ak, входящие в состав логического вектора либо отражают показания некоторого датчика, входящего в состав БА, либо значение «флага» в памяти БЦВМ, устанавливаемого программой БПО, либо сложное условие, формируемое относительно текущей информации в заданной области программной памяти.

Предлагаемая модель семантики УА РВ является альтернативной по отношению к известным моделям, используемым в темпоральных логиках. К ним, прежде всего, относятся таймированные системы переходов и таймированные автоматы. Данные модели семантики схожи между собой и базируются на концепции состояний.

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

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

Кроме того, принятый подход позволяет затем рассматривать реализации одной и той же семантики УА РВ различными логико-временнымми схемами, за счет чего открывается возможность выбора предпочтительных с точки зрения эффективности проектных решений при синтезе УА РВ.

Затем в диссертации строится многоосновная алгебраическая система УА РВ:

АУА = < {UA, LV, Z?0}, ЩF, ЩP, >,

основными множествами (носителями) которой являются:

UA - множество УА РВ в виде наборов кортежей (1),

LV - множество логических переменных {ak},

Z?0 - множество моментов времени (неотрицательные целые числа, соответствующие возможным показаниям дискретного бортового датчика времени КА).

Множество операций ЩF = ЩFТ U ЩFL включает операции во временном пространстве ЩFT = {CH, СК, ®} и логические операции ЩFL={¬,Ю}.

Множество отношений, определенных на элементах множества UA, включает в себя ЩP = {<<, <, <>, <l>, CH, СК, ®}. Символы отношений отличаются от одноименных символов операций гарнитурой и курсивным начертанием шрифта.

Отношение СН имеет место, если два УА начинаются в одно и то же время. Отношение СК имеет место, если два УА РВ завершаются в одно и то же время, отношение ® - если непосредственно в момент завершения выполнения некоторого алгоритма начинается выполнение другого управляющего алгоритма.

Иными словами, с точки зрения интерпретации параметров УА РВ на временной оси:

Т1 СН Т2 Ы tТ1= tТ2

Т1 СК Ы tТ1+ tТ1= tТ2+ t Т2

Т1® Т2 Ы tТ1+ tТ1=tТ2

Здесь tТ1 и tТ2 - моменты начала выполнения алгоритмов Т1 и Т2 соответственно, tТ1 и?t Т2 - длительности их исполнения. Кроме того, в рассмотрение вводятся дополнительные отношения:

*простого временного предшествования <: (Т1 < Т2) Ы tТ1< tТ2

* «строгого» временного предшествования <<: (Т1 << Т2) Ы tТ1+t Т1< tТ2

*наложения во времени H: (Т1 H Т2) Ы (tТ1+ tТ1? tТ2) V (tТ2+ tТ2 ? tТ1)

*несовместности <>: (Т1 <> Т2) Ы (tТ1+ tТ1< tТ2) V (tТ2+tТ2< tТ1), может быть определен как отрицание предиката H

*несовместности по логике <l>: (Т1 <l> Т2) Ы lT1 # lT1, т.е. логический вектор, обуславливающий выполнение Т1, несовместен с логическим вектором, обуславливающим выполнение Т2. Понятие логической несовместности логических векторов означает, что в них в качестве значений одной и той же ЛП ak присутствуют в одном ИСТИНА, в другом - ЛОЖЬ.

К основным операциям над УА РВ во времени относятся:

*операция совмещения по времени начала выполнения (СН),

*совмещения по концу (СК),

*непосредственного следования (®).

Логическая операция (a1)ЮT1 означает, что в логическом векторе, обуславливающем выполнение алгоритма T1 компонента, соответствующая ЛП ?1 принимает значение 1, операция (¬a1)ЮT1 - значение 0.

Добавление в описание множества неотрицательных целых чисел Z?0 позволяет расширить алгебраическую систему УА РВ операциями, аргументами которых будут, с одной стороны, элементы множества УА РВ, а с другой - числа из Z?0:

Н (T1, T2, x) - операция над алгоритмами и числом x, означающая наложение выполнения T2 на выполнение T1, со сдвигом начала выполнения T2 по отношению к T1, равным x.

ЗА (T1, T2, x) - операция, означающая образование нового УА с началом выполнения T2 в момент времени, отстоящий на интервал x от момента окончания выполнения алгоритма T1.

@ (T, x) - операция привязки старта алгоритма T к абсолютному значению времени x.

Свойства объектов алгебраической системы УА РВ могут записываться и исследоваться с помощью формальной теории УА РВ.

Теория УА РВ позволяет производить спецификацию управляющих алгоритмов реального времени с точки зрения их свойств (временных и логических), и осуществлять логические рассуждения (выводы) о них. Это дает возможность проводить формальную верификацию спецификаций УА РВ. Основным используемым при этом методом является дополнение базовых аксиом теории набором аксиом, соответствующих спецификации конкретного управляющего алгоритма, и поиск противоречий.

Алфавит теории включает предметные символы Ti для обозначения функциональных задач, входящих в состав УА РВ, предикатные символы СН, СК, ®, H, <, <<, <>, <l>, символ отрицания ~, круглые скобки ( и ). Правильно построенные формулы имеют вид Ti $ Tj или ~(Ti $ Tj), где $ используется для обозначения произвольного символа отношения. Одновременная выводимость формулы Ф и ее отрицания, т.е. ~(Ф), считается недопустимой. Это позволяет проводить анализ спецификаций УА РВ, записанных на языке формальной теории, на непротиворечивость.

Формальная теория УА РВ содержит следующие аксиомы (схемы аксиом, т.е. вместо символов Ti, Ti и Tk могут быть подставлены любые предметные символы, обозначающие ФЗ) и правила вывода (схемы правил вывода):

Аксиомы

Правила вывода

Помимо приведенного варианта, в диссертации приводится формулировка теории УА РВ как прикладного исчисления предикатов первого порядка. Благодаря этому, теория «погружается» в среду языка Пролог, что дает возможность использования встроенного в него механизма логического вывода для исследования свойств управляющих алгоритмов. Этот вопрос подробно освещается в специальном подразделе второй главы, посвященном использованию Пролога для решения задач верификации УА РВ.

Формулы теории УА РВ интерпретируются в рамках многоосновной алгебраической системы УА РВ. Так, формула fi СН fj будет означать, что в кортежах, описывающих ФЗ fi и fj в данном управляющем алгоритме, ti = tj, т.е. моменты запуска соответствующих функциональных задач совпадают. Формула fi СК fj будет означать, что в четверках, описывающих ФЗ f i и fj в данном УА, ti + ti= tj + tj, т.е. времена окончания выполнения функциональных задач совпадают. Формула fi ® fj означает, что в четверках, описывающих вхождения функциональных задач fi и fj в данном УА РВ, ti + ti= tj. Формула (ak) => fi означает, что соответствующая компонента логического вектора, входящего в кортеж, описывающий вхождение ФЗ fi в данный УА РВ, должна иметь значение 1 (ИСТИНА).

В диссертации доказана теорема о том, что алгебраическая система УА РВ является моделью формальной теории УА РВ.

Набор формул может быть интерпретирован на некотором управляющем алгоритме, имеющем конкретные значения длительностей для каждой из функциональных задач. В образующемся таким образом «возможном мире» каждая из формул теории УА РВ принимает истинностное значение. Аксиомы при этом сохраняют свою общезначимость. Это дает возможность проводить верификацию свойств УА РВ, записанных с помощью формул теории УА РВ, не только путем логического вывода, но и путем проверки на модели (метод model checking).

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

В соответствии с изложенным, становится возможной постановка задачи «разрешения спецификации», т.е. определения значений длительностей ФЗ, при которых заданная спецификация будет выполнима. Единственное решение эта задача будет иметь в том случае, если известны длительности и логические вектора всех ФЗ, кроме одной (неизвестной), и необходимо определить, при каких параметрах искомой ФЗ спецификация будет выполнимой. В остальных случаях имеется множество решений, тем не менее, возможно определение границ области решений (области выполнимости в пространстве параметров). Решение задачи производится путем перехода от формул теории УА РВ к уравнениям и неравенствам на множестве целых чисел. Для дальнейшего их решения можно применить любой известный метод, в том числе, осуществив описание семантики УА РВ средствами системы Пролог можно использовать для поиска значений неизвестных параметров ФЗ встроенную в Пролог машину логического вывода. Вопросам применения среды логического программирования Пролог при работе с представлениями УА РВ для БВС КА посвящен специальный подраздел главы.

Вторая глава содержит также подраздел, посвященный сравнению описываемого в диссертации подхода с существующими. С одной стороны, предложенный подход во многом подобен применению темпоральных логик и алгебр процессов, с другой стороны, у него имеется ряд принципиальных отличий. Так, он изначально предназначался для описания процессов реального времени, и в отличие, например, от интервальной логики Аллена описывает не только качественные, но и количественные характеристики соотношений между исполняемыми процессами. При этом построенная модель включает как относительное, так и абсолютное время за счет присутствия операции @. Применение описанной модели семантики УА РВ (фактически представляющей статическое описание динамического исполнения УА РВ) позволяет отказаться от пошагового моделирования состояний алгоритма при проверке формул теории УА РВ. Коренным отличием от подхода, присущего временным логикам является, кроме того, предоставление не только способов описания свойств существующего УА РВ, но и конструктивных возможностей для построения управляющих алгоритмов на некотором базисе элементарных ФЗ. Это роднит его с алгебрами процессов (BPA, ATP, ACP, CSP и др.). В то же время, предлагаемая система обладает более богатыми изобразительными возможностями, чем большинство алгебр процессов. При представлении различных вариантов поведения системы в них обычно имеется способ лишь самым общим образом описать альтернативную композицию двух процессов. В отличие от этого, предлагаемый подход позволяет сопоставить каждой функциональной задаче, выполняемой управляющим алгоритмом, логический вектор, который может включать в свой состав целый набор логических переменных. Кроме того, при описании параллельного исполнения процессов обычно отсутствует возможность точной синхронизации моментов их начала и окончания, в то время как в рамках алгебраической системы УА РВ присутствуют специальные связки СН, СК и Н.

Во второй главе также содержится описание многовариантной модели и логико-временной схемы УА РВ.

Рассмотрим набор кортежей (1), задающий семантику УА РВ. Зафиксируем какое-то конкретное значение логического вектора. В результате кортеж из четырех значений преобразуется в тройку Wi:

MWM = { Wi}, Wi = < fi, ti, ti >, i= .

Полученная модель описывает один из возможных вариантов исполнения управляющего алгоритма. При этом в отличие от операционно-логической истории программы указывается не просто последовательность шагов, а точные значения времени начала и длительности выполнения отдельных действий. Диссертация содержит процедуру преобразования данного представления в графовую модель, описывающую структуру конкретной реализации управляющего алгоритма. Под «входом» при этом понимается включение (получение управления) управляющего алгоритма в некоторый момент времени ti, в который он должен осуществить запуск некоторой функциональной задачи fi (или нескольких функциональных, если в УА имеется несколько ФЗ с одинаковым временем запуска). С точки зрения программной реализации это соответствует одной из точек входа управляющей программы, по которой производятся некоторые действия, после чего осуществляется возврат в бортовую операционную систему. Список базовых действий включает занесение запросов на включение программ БПО по истечении заданного временного интервала, для чего используются специальные возможности БВС и бортовой операционной системы. В том числе возможно занесение запроса на включение следующего входа данного УА РВ, что формирует косвенную передачу управления.

Сопоставляя каждому включению (входу) управляющего алгоритма вершину графа и соединяя их дугами в случае наличия передачи управления между входами, мы получаем граф, соответствующий траектории во времени (включениям) одного варианта УА. Дугам графа при этом приписываются веса, соответствующие интервалам времени между входами.

Возможно также построение расширенной модели, отражающей все варианты исполнения алгоритма. В этом случае первый шаг (фиксация значения логического вектора и отбрасывание несоответствующих ему кортежей в модели семантики УА) не производится, и все входящие в алгоритм различающиеся моменты времени, в которые включаются функциональные задачи, отображаются во входы модели. Такая расширенная многовходовая модель фактически представляет собой логико-временнумю схему алгоритма. Логико-временная схема является аналогом управляющего графа последовательной программы, в котором, помимо дуг, обозначающих передачу управления от одного оператора программы другому, имеются особые дуги - дуги с приписанными им весами. Взвешенная дуга обозначает передачу управления между входами УА РВ не непосредственно, а по истечении интервала времени, соответствующего весу дуги. Вершинам сопоставляются элементарные действия (запуски функциональных задач и проверки значений логических переменных) УА РВ. Дуги без весов соответствуют простой передаче управления в традиционном алгоритмическом смысле (следование действий). В логико-временной схеме присутствуют, кроме того, «терминальные» вершины, соответствующие завершению работы УА РВ (передаче управления из управляющей программы программе-диспетчеру бортовой операционной системы).

Поскольку в описание УА РВ сразу несколько функциональных задач могут входить с одним и тем же временем запуска, они будут принадлежать одному входу. В связи с этим для каждого входа можно построить традиционный управляющий граф программы с вершинами, соответствующими операторам (запусками ФЗ) и вершинами, сопоставляемыми проверкам условий. Таким образом, вход будет иметь собственную внутреннюю структуру (возможно, достаточно сложную). Кроме того, в общем случае каждый вход может передавать управление не одному, а нескольким входам.

В процессе исполнения алгоритма обеспечивается реализация некоторой семантики УА РВ. На рисунке 1 приведен пример соответствия между логико-временной схемой и семантикой УА РВ.

Рис. 1. Переход от семантики УА РВ к логико-временной схеме алгоритма

Рис. 1. Переход от семантики УА РВ к логико-временной схеме алгоритма

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

На основе модели семантики УА РВ можно построить также многовариантную модель УА РВ, играющую важную роль, в частности, при отладке управляющих программ, когда требуется точный набор возможных вариантов выполнения. Если зафиксировать в семантике УА РВ некоторый момент времени (вход), то получится набор:

Данное представление включает в себя описание для каждой функциональной задачи обуславливающего ее выполнение в исследуемый момент времени логического вектора. Если устранить в ней все строки, в которых логические вектора совпадают, т.е. дубли, и отбросить первые два компонента каждой триады, то фактически получается таблица возможных вариантов исполнения данного входа. Если же применить операцию простого отбрасывания компоненты времени запуска в формирующих семантику УА РВ кортежах, то получается расширенная многовариантная модель всего управляющего алгоритма (на основе которой нетрудно построить таблицу возможных вариантов исполнения, имеющую важное значение с точки зрения исследования и тестирования УА РВ).

В таблице 1 приводится перечень основных описываемых в диссертации моделей УА РВ и задачи, при решении которых они используются.

Таблица 1.

Разновидность модели	Использование
Модель семантики УА РВ	Визуальное конструирование УА РВ, оптимизация плана управления, контроль соответствия (верификация) семантики УА РВ спецификации, проверка спецификации УА РВ на выполнимость
Многоосновная алгебраическая система УА РВ	Визуальное конструирование УА РВ, проверка спецификации УА РВ на выполнимость, построение множества возможных вариантов исполнения УА.
Формальная теория УА РВ	Спецификация требований к УА РВ. Верификация спецификаций УА РВ, проверка спецификации УА РВ на выполнимость.
Многовариантная модель УА РВ	Построение множества вариантов исполнения УА, генерация отладочных заданий для вариантов.
Логико-временная схема УА РВ	Синтез и верификация логико-временной схемы УА РВ, построение документации на УА РВ, генерация управляющей программы.

Третья глава посвящена описанию методов выбора проектных решений (структурной оптимизации) на различных этапах автоматизированного синтеза УА РВ для БВС КА.

На этапе спецификации аксиомы и правила вывода формальной теории УА РВ делают возможным проведение эквивалентных преобразований формул, в том числе - сокращающих общую длину формулы. Таким образом, задача оптимизации на этом этапе ставится как:

NF(S) ® min, при S = const,

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

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

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

Наиболее практически обоснованными при этом будут два критерия:

1.Снижение количества одновременно выполняемых в каждый момент времени на борту КА процессов (оптимизация по критическому сечению).

2.Сокращение общей продолжительности исполнения УА РВ (оптимизация по длительности). В этом случае задача оптимизации при синтезе конкретного плана управления (семантики УА РВ) ставится как TS?УА??® min, при условии выполнения всех формул спецификации, где TS?УА? - общая продолжительность исполнения УА, или NФЗ(t) ® min, t О [0,T], где NФЗ(t) - количество параллельно исполняемых в момент времени t функциональных задач, [0,T] - продолжительность исполнения УА РВ.

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

Следующим этапом синтеза УА РВ является генерация логико-временной схемы алгоритма, реализующей построенную семантику. На этом этапе открывается еще одна возможность оптимизации. В качестве целевой функции, значение которой подлежит минимизации, фигурирует число логических вершин графа логико-временной схемы (вершин, в которых происходит ветвление) NL, и задача оптимизации ставится как: NL(УА)® min, при сохранении реализуемой семантики УА.

В диссертационной работе приводится описание двух типов структурной оптимизации при синтезе логико-временных схем УА РВ. Первый касается преобразований структуры отдельного входа УА. Второй относится к оптимизации на основе учета связей между входами. Оптимизация внутренней логической структуры входа основывается на упорядочении логических переменных их «весу» - количеству зависимых от них ФЗ, и может давать достаточно существенный выигрыш по количеству логических ветвей в алгоритме. Идея заключается в том, что проверка переменных, от которых меньше всего зависит выполнение ФЗ, производится в последнюю очередь. При синтезе логико-временной схемы наихудший по количеству ветвей вариант оценивается величиной 2M-1, где M - количество фигурирующих в управляющем алгоритме логических переменных. Число же ветвлений в наилучшем (оптимизированном) варианте будет стремиться к M. Таким образом, уже для случая семи переменных по сравнению с наихудшим случаем достигается выигрыш, более чем в десять раз. Потенциал оптимизации первого рода в зависимости от M иллюстрируется рисунком 2.

Рисунок 2. Эффективность оптимизации структуры входа УА РВ

На рисунке 3 показана сущность второго метода оптимизации, основанного на построении «цепочек» одинаково обусловленных входов УА.

Представлена структура алгоритма, включающего несколько входов, между которыми заданы временныме интервалы. Изображенные на рисунке логико-временные схемы УА могут быть описаны одной и той же семантикой УА (зададим для определенности длительности ФЗ tf1=100, tf2=200, tf3=50, tf4=150): УА ={<{f1, 0, 100,(a1=0)>, <f2, 0, 200, (a1=1)>,<f3, 0, 10,(a1=0)>, <f4,0, 210,(a1=1)>}.

Рис.3. Оптимизирующее преобразование логико-временной схемы УА

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

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

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

1.?t0, когда значение переменной может меняться, но актуальным является ее значение в некоторый момент времени t0 (часто это момент начала исполнения УА), и последующие изменения не должны влиять на логику УА РВ;

...