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

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

ТЮГАШБВ Андрей Александрович

СИНТЕЗ И ВЕРИФИКАЦИЯ УПРАВЛЯЮЩИХ АЛГОРИТМОВ РЕАЛЬНОГО ВРЕМЕНИ ДЛЯ БОРТОВЫХ ВЫЧИСЛИТЕЛЬНЫХ СИСТЕМ КОСМИЧЕСКИХ АППАРАТОВ

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

АВТОРЕФЕРАТ диссертации на соискание ученой степени доктора технических наук

Самара - 2007

003066486

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

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

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

доктор технических наук, профессор Северцев Николай Алексеевич доктор технических наук, профессор Федунов Борис Евгеньевич доктор технических наук, профессор Коварцев Александр Николаевич

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

Защита состоится 9 ноября 2007 г в 10 часов на заседании диссертационного совета Д 212 215 05 в конференц-зале Самарского государственного аэрокосмического университета по адресу г Самара, Московское шоссе, 34

С диссертацией можно ознакомиться в библиотеке Самарского государственного аэрокосмического университета

Автореферат разослан 7 сентября 2007 г

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

совета, д т н , профессор

А А Калентьев

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ Актуальность темы

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

• методы и средства автоматизированного синтеза УА РВ и 1енерации

управляющей программы,

• методы и средства построения таблицы вариантов УА РВ и генерации

отладочных заданий для каждого варианта

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-ле1ию факультета информатики СГАУ (г Самара, 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 Методы выбора проектных решений при синтезе УА РВ для БВС КА

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

УА РВ = { Ф, }, Ф, = < 1„ т, Т,>, N , (1)

где Г, - идентификатор функциональной задачи (ФЗ), I, - момент начала выполнения ФЗ (целое неотрицательное число), т, - длительность ФЗ (целое

неотрицательное число), /( - логический вектор, обуславливающий ФЗ

Каждый кортеж Ф, описывает одно действие (функциональную задачу), производимое управляющим алгоритмом Ф, обычно подразумевает работу какого-то прибора или агрегата, входящего в состав БА, или выполнение функциональной программы из комплекса БПО При этом функциональная задача может выполняться не мгновенно, а на протяжении интервала времени т„ начиная с момента I Осуществление тех или иных действий не носит безусловного характера, а должно соответствовагь текущей ситуации на борту КА, которая описывается набором значений логических переменных <ссь <Х)>, формирующих

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

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

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

Затем в диссертации строится многоосновная алгебраическая система

УА РВ

АУА = < {иА, ЬУ, г>0}, Пр, Пр, >, основными множествами (носителями) которой являются

иА - множество У А РВ в виде наборов кортежей (1), ЬУ - множество логических переменных {ак},

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

Множество операции — и включает операции во временном пространстве Г2[т = {СН, СК, н>} и логические операции

Множество отношений, определенных на элементах множества иА, включает в себя = {«, < <>, </>, СН, СК, ->} Символы отношений отличаются от одноименных символов операций гарнитурой и курсивным начертанием шрифта

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

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

Т1 СН Т2 о 1)]= 1)2 Т, С/СсМп+Тп^а+ттг Т]-^ Т2<=> 1п+ Тт1='т2

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

• простого временно!о предшествования < (Т) < Т2) 01п< ^

• «строгого» временного предшествования << (Т| « Т2) <=> ¡¡< ^

• наложения во времени Н (Т, Н Т2) <=> (1:п + гТ1< 1Г1) V (Ьп+ 1тг 2 ^,)

• несовместности <> (Т) <> Т2) <=> тТ1< ^ V (Ъп+ътг^ может быть определен как отрицание предиката Н

• несовместности по логике </> (Т) </> Г2) <=> /п # Ни т е логический вектор, обуславливающий выполнение Ть несовместен с логическим вектором, обуславливающим выполнение Т2 Понятие логической несовместности логических векторов означает, что в них в качестве значений одной и той же ЛП ак присутствуют в одном ИСТИНА, в другом - ЛОЖЬ

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

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

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

• непосредственного следования (—>)

Логическая операция (а,)^>Т| означает, что в логическом векторе, обуславливающем выполнение алгоритма Т) компонента, соответствующая ЛП а) принимает значение I, операция (-,а])=>Т1 - значение О

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

Н (Т), Т2, х) - операция над алгоритмами и числом х, означающая наложение выполнения Т2 на выполнение Ть со сдвигом начала выполнения Т2 по отношению к Ть равным .V

ЗА (Т|, Т2, х) - операция, означающая образование нового УА с началом выполнения Т2 в момент времени, отстоящий на интервал х от момента окончания выполнения алгоритма Т)

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

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

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

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

->, Н, <, «, <>, </>, символ отрицания круглые скобки ( и ) Правильно построенные формулы имеют вид Т, $ Tj или ~(Т, $ Т,), где $ используется для обозначения произвольного символа отношения Одновременная выводимость формулы Ф и ее отрицания, т е ~(Ф), считается недопустимой Это позволяет проводить анализ спецификаций У А РВ, записанных на языке формальной теории, на непротиворечивость

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

Аксиомы

А01 Т, CHT, А02 Т, CKТ, АОЗ ~(Т, ->Т,) А04 Т, НУ,

А05 ~(Т, < Т,) А06 ~(Т, « Т,) А07 ~(Т, <> Т,) А08 ~(Т, </> Т,)

Правша вывода

П1 Т. СН Tj П2 Т, СК1\ ПЗ Т, СН Tj,. Тх СН Т|Л14 Т, CK Tj. Tj СКЪ

Т]СН1\ У, CHT, ' Т, СН1\ ' Т, СКЛ\

П5 Т. СН Tj П6 Т, СКТ\ П7 Т, -> Т,_П8 Т, ~>Tj

~(Т, ^ Tj) -(T.-^Tj) чт;^ ~(T,CKTj)

П9 T.CHTj П10 Т, СКУ1 ГШ Т, ->Tj П12 Т, -»Т,

Т, Н Tj Т, WTj -(tjWT.) T;<TJ

П14 Т. «Tj П15 Т, Н Tj П16 Т, Н'1\ П17, Т, «Tj

Т| < Tj TjHT, ~ (Т,о Tj) Т,о Т|

П18 Т, о Tj П19 'Г, <l> Tj П20 Т, о Т, Г121 Т,Н'\\

Т>Т, Tj </> т, ~(Т, Н lj) -(T.-^Tj)

П22 Т.«. « Т., П23 Т, < 'I; , Тх < Ту_П24 (а,,)=эТ,

" Т,«Тк ~ " Т,<Тк ~ ((~чхк)=>Т|)

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

Формулы теории УА РВ интерпретируются в рамках многоосновной алгебраической системы УА РВ Так, формула ^ СН ^ будет означать, что в кортежах, описывающих ФЗ £ и 1] в данном управляющем алгоритме, (, = Хр т е моменты запуска соответствующих функциональных задач совпадают Формула £ СК^ будет означать, что в четверках, описывающих ФЗ Г, и ^ в данном УА, 1,+ т,= I, + те времена окончания выполнения функциональных задач совпадают Формула £ -> £ означает, что в четверках, описывающих вхождения функциональных задач Г, и ^ в данном УА РВ, I,4-1,= Формула (ак) => £ означает,

что соответствующая компонента логического вектора, входящего в кортеж, описывающий вхождение ФЗ / в данный УА РВ, должна иметь значение 1 (ИСТИНА)

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

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

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

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

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

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

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

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

М\УМ = { \¥,}, \У, = < 1„ т, >, 1= 1, N

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

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

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

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

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

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

20

180

220

вкл ^ вкл г3

20 _

а, =И„

Д60 вкл* шои.

=Л

40

180

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

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

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

МВМ = { < т„

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

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

Таблица 1

Разновидность модели Использование

Модель семантики УА РВ Визуальное конструирование УА РВ, оптимизация плана управления, контроль соответствия (верификация) семантики УА РВ спецификации, проверка спецификации УА РВ на выполнимость

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

Формальная теория УА РВ Спецификация требований к УА РВ Верификация спецификаций УА РВ, проверка спецификации УА РВ на выполнимость

Многовариантная модель УА РВ Построение множества вариантов исполнения УА, генерация отладочных заданий для вариантов

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

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

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

Nr(S) -» min, при S = const,

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

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

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

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

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

2 Сокращение общей продолжительности исполнения УА РВ (оптимизация по длительности) В этом случае задача оптимизации при синтезе конкретного плана управления (семантики УА РВ) ставится как ТЕ(УА)-> min, при условии выполнения всех формул спецификации, где Т2(УА) - общая продолжительность исполнения УА, или N<w(t) —> min, t е [0,Т], где N®3(t) -количество параллельно исполняемых в момент времени t функциональных задач, [0,Т] - продолжительность исполнения УА РВ

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

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

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

логических переменных. .Число же ветвлений в наилучшем (оптимизированном) варианте будет стремиться к М Таким образом, уже для случая семи переменных по сравнению с наихудшим случаем достигается выигрыш, более чем в десять раз. Потенциал оптимизации первого роли в зависимости от М иллюстрируется рисунком 2

- ♦■■ Наихудший вариант —Полностью оптимизированный вариант

2 3 4 5 6 7 8

Количество логических переменных

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

Па рисунке 3 покачана сущность второго метода оптимизации, основанного на построении «цепочек» одинаково обусловленных входов УЛ. I ¡рсдставлена структура алгоритма, включающего несколько входов, между которыми заданы временны! 1с интервалы Изображенные на рисунке ЛОГИКО-временные схемы УЛ могут быть описаны одной и той же семантикой УЛ (зададим для Определенности длительности ФЗ тГ|Н00, тп-200, тп=50, тг4= 150) УЛ ={<{!',, 0, 100,(<*!=#)>, <Г2, 0, 200, (а|-=1)>,<Гз, 0, 10,(а,=0)> <£,,0,210,(<Хг»1)>}. В то же время, во втором случае выполняется на две проверки логических условий меньше, что приводит к упрощению структуры. Это достигается за счст выноса операции занесения временной уставки на включение соответствующего входа, в одну из ветвей, расположенных после проверки значения логической переменной. В примере фигурирует только одна переменная - аь но принцип опт имизации не меняется и для более сложных комбинаций проверок логических условий

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

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

2. когда значение логической переменной не претерпевает изменений в процессе исполнения УА.

3. и (У), когда требуется учитывать значение логической переменной в текущий момент времени I, и с течением времени значение ЛП может меняться.

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

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

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

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

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

Nk(yri)->mm, S = const,

где Nk(yrT) - общее количество строк в генерируемой управляющей программе, S - семантика УА РВ В диссертации описывается машинно-зависимая оптимизация, опирающаяся на особенности реализации конкретной архитектуры бортовой вычислительной системы и синтаксис команд ассемблера БЦВМ, задаваемый с помощью специальных параметрических файлов формата XML

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

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

—#—Число пропер о к оптимизированное —■—Число Е1роеерок, Р=10 -•-А—Число проверок. Р=40 - х- Число проасрок, Р=20

25000 1 20000 | 15000

£4

0

§ 10000

У

X

1 5000

0

123456789 Количество логических переменных

Рис. 4. Число проверок логических условий с оптимизацией и без оптимизации

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

В качестве выводов третьей главы констатируется, что применение описашшх методов выбора предпочтительных проектных решений при синтезе УЛ РВ на различных стадиях жизненной} цикла может' давать существенный выигрыш в эффективности алгоритма с точки зрения требуемых ресурсов (времени, памяти и производительности ВВС)

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

Можно выделить следующие основные задачи, решаемые в рамках разработанной автоматизированной технологии:

• Формальная спецификация требований к УА РВ с использованием проблемно-ориентированного языка, основанного па языке формальной теории УА РВ иди визуального интерактивного языка

• Построение Семантики управляющего алгоритма, соответствующей спецификации

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

• 11остроение логико-временной схемы УА РВ

• Генерация технической документации на УА РВ в составе временноРй диаграммы и блок-схемы алгоритма

• Генерация управляющей программы БЦВМ, реализующей управляющий алгоритм, на параметрически задаваемом языке программирования

• Генерация отладочных заданий (на языке технологической среды отладки БПО) для каждого возможного варианта исполнения УА РВ

• Генерация таблиц входных и выходных информационных и управляющих связей программы

Проектировщики и разработчики УА РВ взаимодействуют при этом с несколькими интерфейсными модулями Это в первую очередь - интегрированная среда, являющаяся аналогом IDE современных систем программирования Borland С++ Builder, MS Visual Studio, Eclipse, IDEA Она объединяет все модули программного комплекса в единое целое и позволяет получить из единого центра доступ к любой функции системы графическому конструктору управляющих алгоритмов, графическому редактору временны Пх диаграмм, генераторам управляющей программы и отладочных заданий, редактору описаний ФЗ и ЛП Благодаря этому, интегрированная оболочка инструментального программного комплекса может в некоторой степени рассматриваться, как аналог PDM-средства, интегрирующего различные электронные модели изделия в традиционных пакетах САПР Как известно, интерфейс пользователя в PDM-системе обычно предусматривает возможность одновременного просмотра разных представлений проектных данных в нескольких окнах На рисунке 5 представлен экран компьютера при работе с одновременно открытыми окнами, содержащими различными виды представления управляющего алгоритма, что иллюстрирует наличие подобных возможностей разработанного программного комплекса

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

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

2.1

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

... '-у РЩР ■ ----------—........... Jl..

Рис. 5. Многооконный интерфейс инструментального программного комплекса

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

OF = [ <f„ т„ Тх„ Pr„ Typ!, GP,> (,

LP = {<а„ Тх„ Ргг, Typ,, GPi>}, где f, - идентификатор ФЗ, otj - имя ЛП, т, - длительность исполнения ФЗ; Тур, — тип функциональной задачи или логической переменной, Тур, е {ТуpL} - {«выдать команду ни RA», «занести запрос па включение программы Б ПО», «открыть капал», «опросить сигнал», «проверить переменную».. ) - тип действия, каждому типу соответствует свой шаблон фрагмента управляющей программы; Тх, -параметры конкретной ФЗ или ЛГ(; Рг, - текстовое описание ФЗ (примечание); GP| - код графическою примитива, отражающего ФЗ на временной диаграмме УА PB.

Описание ФЗ и ЛИ проводится с помощью специального модуля программного комплекса. Параметрическая генерация управляющей программы в рамках автоматизированной технологии позволяет значительно ускорить процесс программирования и облегчить переход от одних целевых языков программирования и архитектур БВС к другим.

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

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

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

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

Структура инструментального программного комплекса, поддерживающего разработанную автоматизированную технологию, представлена на рисунке б

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

Рис. 6 Структура инструментального программного комплекса

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

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

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

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

РТВе ЛИГ • ЛИ :

■ —т------sfcr

Н^П IWriU

- ^ШЛ—— --------- ^ ----

шЯ ив

ял.............¡8—......-ШШ.....-

Ж ш..... Ш

__t__ ИИ__Ш^Ш

Спецификация Программирование и Общая трудоемкость

АО

Рис. 7, Снижение трудоемкости при применении автоматизированной технологии

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

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

Питая глава посвящена описанию практического использования разработанной автоматизированной технологии и программного комплекса.

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

Кроме того, демонстрируется применимость автоматизированной технолог ии к задачам построения Программ моделей бортовой аппаратуры КЛ па примере бортовой информационно-телеметрической системы (БИТС).

Важным с точки зрения анализа жизненного цикла КЛ и его БПО является то, ЧТО при создании комплекса БПО, помимо собственно бортовых управляющих программ, необходимо разработать комплекс программ моделей бортовой аппаратуры, движения КЛ и факторов внешней среды Программы моделей используются в процессе комплексной отладки БПО и испытаний КЛ в качестве замены натурных приборов н агрегатов^ что позволяет сократить сроки разработки При этом программа модели проходит практически те же стадии жизненного никла, что и УЛ !JB, а се суть состоит в реализации циклограммы функционирования бортовой аппаратуры в различных режимах

100 80 60 40 20 0

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

Таким образом, применение описанного в диссертационной работе подхода дает возможность использовать так называемое совмещенное проектирование (concurrent design), являющееся характерной отличительной чертой современных CALS-технологий в промышленности и позволяющее сократить временны Пе затраты путем перекрытия по времени фаз жизненного цикла (операций, процедур или этапов), при традиционном подходе выполняемых последовательно

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

Показано, как по результатам графического конструирования автоматизированно формируется текст спецификации алгоритма модели на проблемно-ориентированном языке, а затем генерируется программа на языке программирования Си Таким образом, демонстрируется практическая применимость предлагаемого подхода для программ моделей бортовой аппаратуры, используемых при комплексной отладке БПО При этом переход от генерации управляющей программы на языке ассемблера БЦВМ к генерации программы модели на языке Си, исполняемой на наземном отладочном комплексе, осуществляется простой заменой настроечных файлов

В заключении приводятся основные выводы

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

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

УА РВ = { Ф,}, Ф,= < i> tb *„ I >, 1= 1, N

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

4 Разработаны методы и средства синтеза УА РВ для БВС КА, включая

• алгоритм генерации семантики УА РВ, соответствующей спецификации,

• алгоритм построения логико-временной схемы (структуры) УА РВ,

• методы и средства параметрической генерации управляющей программы, реализующей требуемую семантику УА РВ, на целевом языке программирования (включая ассемблер БЦВМ и язык Си)

5 Сформулированы критерии, предложены методы выбора проектных решений при синтезе УА РВ (структурной оптимизации) и проведено исследование их эффективности, в том числе

• методов эквивалентных преобразований спецификаций УА РВ,

• методов оптимизации семантики УА РВ,

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

• методов оптимизации при генерации управляющей программы, реализующей управляющий алгоритм

6 Разработаны методы и средства верификации УА РВ, в том числе

• проверки спецификации УА РВ на непротиворечивость,

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

• верификации логико-временной схемы управляющего алгоритма (проверки соответствия реализуемой логико-временной схемой семантики спецификации УА РВ),

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

• автоматизированного построения таблицы информационных и управляющих связей УА РВ с другими программами БПО

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

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

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

ОСНОВНЫЕ РЕЗУЛЬТАТЫ ДИССЕРТАЦИИ ОПУБЛИКОВАНЫ В СЛЕДУЮЩИХ РАБОТАХ

Монография:

1 Калентьев А А , Тюгашев А А ИПИ/САЬБ технологии в жизненном цикле комплексных программ управления - Самара СНЦ РАН, 2006 - 285 с ил - 1000 экз - 18В1Ч 5-934-24257-1

Статьи в изданиях, рекомендованных ВАК для публикации результатов докторских диссертаций:

2 Тюгашев, А А Интегрированная среда для проектирования управляющих алгоритмов реального времени // Известия РАН Теория и системы управления -2001 -№5-, С 128-141

3 Калентьев А А , Тюгашев А А Использование технологии ГРАФКОНТ при автоматизированном проектировании управляющих программ реального времени для БВС КА // Всероссийский аэрокосмический журнал «Полет» - 2005 -№12 - С 41-47

4 Тюгашев А А Автоматизированная спецификации, верификация и синтез управляющих программ на основе логического и алгебраического подходов // Вестник СГАУ -2007-№1(12) - С 171-179

5 Тюгашев А А Автоматизированное оценивание временных характеристик программ управления комплексного функционирования в технологии ГРАФКОНТ // Вестник СГТУ Серия «Физико-математические науки» -2007 -№1 (14) -С 134-137

6 Тюгашев А А Автоматизация спецификации, синтеза и верификации управляющих программ реального времени с применением логического и алгебраического подходов // Мехатроника, автоматизация, управление - 2007 -№7 - С 46-50

7 Тюгашев А А Методология и программный комплекс для автоматизированного проектирования управляющих алгоритмов реального времени // Вестник СНЦ РАН Том 7-2005 -№1 -С 131-137

8 Калентьев А А, Тюгашев А А САЬЗ-технологии для бортовых алгоритмов управления космическими аппаратами // Вестник СНЦ РАН Том 7 -2005-№1 -С 124-130

9 Тюгашев А А Алгебраические модели управляющих алгоритмов и программ реального времени для космических аппаратов // Вестник СГТУ Серия «Физико-математические науки» - 2005 - выпуск 38 - С 19-25

10 Тюгашев А А Технология проектирования надежных управляющих алгоритмов реального времени для космических аппаратов // Вестник СГАУ -2004 - №1 -С 124-131

Статьи в сборниках научных трудов'

11 Калентьев А А, Тюгашев А А Оптимизация логико-временной схемы управляющего алгоритма при его автоматизированном синтезе И Международный симпозиум «Надежность и качество 2007» сб научн тр / ПГУ - Пенза, 2007 -С 117-118

12 Калентьев А А, Тюгашев А А Математическое моделирование управляющих алгоритмов и программ реального времени // Международный симпозиум «Надежность и качество 2005» сб научн тр / ПГУ - Пенза, 2005 ЧН -С 251-257

13 Калентьев А А , Тюгашев А А Технология проектирования надежных и качественных алгоритмов управления реального времени // Труды

Международный симпозиум «Надежность и качество 2004» сб научн тр /ЛГУ -Пенза, 2004 - С 249-253

14 Калентьев А А, Тюгашев А А Методология проектирования надежных алгоритмов управления для космических аппаратов //11-й Всероссийский научно-технический семинар по управлению движением и навигации летательных аппаратов сб научн тр / СГАУ - Самара, 2003 -С 115-119

15 Тюгашев А А Технология проектирования качественных и надежных управляющих программ реального времени для БВС КА // Международный симпозиум «Надежность и качество 2003» сб научн тр / ПГУ - Пенза, 2003 -С 201-203

16 Тюгашев А А Автоматизация оценивания временных характеристик программ управления комплексного функционирования в технологии ГРАФКОНТ И Меясдународный симпозиум «Надежность и качество 2003» сб научн тр / ПГУ -Пенза,2003 -С 198-201

17 Калентьев А А, Тюгашев А А Развитие системы автоматизации проектирования бортовых управляющих алгоритмов реального времени ГРАФКОНТ И Международный симпозиум «Надежность и качество 2002» сб научн тр / ПГУ - Пенза, 2002 - С 123-129

18 Тюгашев А А Использование функции выполнимости для описания алгоритмов управления дискретными асинхронными системами // Международный симпозиум «Надежность и качество 2002» сб научн тр / ПГУ -Пенза, 2002 -С 129-132

19 Калентьев А А, Мостовой Я А , Тюгашев А А Технология ГРАФКОНТ для автоматизированного проектирования комплексных управляющих программ И Сб научно-технических статей по ракетно-космической тематике / ГНПРКЦ «ЦСКБ-Прогресс» - Самара,2001 - С 165-167

20 Калентьев А А, Мостовой Я А, Тюгашев А А Проблема неоднозначности при порождении синтаксических структур над семантикой управляющих алгоритмов реального времени // Сб научно-технических статей по ракетно-космической тематике / ГНПРКЦ «ЦСКБ-Прогресс» - Самара,2001 -С 162-165

21 Тюгашев А А Построение улучшенного транслятора проблемно-ориентированного языка описания управляющих алгоритмов реального времени в системе ГРАФКОНТ // Международный симпозиум «Надежность и качество 2001» сб научн тр / ПГУ -Пенза, 2001 -С 33-35

22 Калентьев А А, Тюгашев А А Проблема автоматизированного формирования отладочных заданий в рамках информационной технологии автоматизированного проектирования бортовых алгоритмов управления // Международный симпозиум «Надежность и качество2001» сб научн тр /ПГУ -Пенза, 2001 -С 35-37

23 Тюгашев А А Неоднозначность порождения логической схемы управляющего алгоритма реального времени // Перспективные информационные технологии в научных исследованиях, проектировании и обучении сб научн тр / СГАУ - Самара, 2001 -С 29-35

' 24 Калентьев АА, Тюгашев АА Магешшчетая мэдгпь аягоришов удивления актами с множеством даскрешых состояний // Перспекшвнье информационные технологии в ночных исследованиях, проектировании и обучении °б геучн тр. /СГАУ -Смра,2001 -С29-35

25 Калентьев АА, Тюгашев АА Задзда согласования логики и времени исполнения фушщисшйщк управляющих программ в системе ГРАФКОНТ // Упраагшие доокшием и гшигашя летательных аппаратов сб нфчнтр/Ож^эодайфилгатаадмиикосма^^ -С.90-95

26 Калальев АА, Мосжвой ЯА, Платонов СН, Тюгашев АА, Вщушина ЛИ, Ниюлаев ЮА Сисюув автоматизированного синтеза бортовых алгоритмов уцзавления // Управление движением и ювига1щлеягатеэтьныхаппарапв.сб.научк

-С 96-97

27 Каналье» АА, Мостовой ЯА, Тюгашев АА Параметризованная генерация кеда аотайпер юго тшла в САЖ-теждагии ГРАФКОНГ // Мегкпународньш симпозиум «Надежность и канесшз» кндаа/ПГУ-Шва,1999С 186-187

28 Каленгаев АА, Мостовой ЯА, Тюгаша АА Проблема переполнения щм кодировании векторов трехзначной логики в системе ГРАФКОНГ // Междупфодтьш симпозиум «Надежность и качества» кндоох/ПГУ-Пнва, 1999С185-186

29 Капешь№АА,Тняаш®ААГрафичвдсийредаафва

управляющих алпоришэв // Мездунарсдаая научно-техническая конференция «Агауапьные проблемы атшшаиобеспеяениянадгжжстикздеотшр^ сбдоовдрв -Пенза, 1998,-С

158-159

30 КапнпьевАА, Тюгаикв АА Автоматизированный синтез управляющих программ реального времени на языке ахем&1ди//Ме>клун^»дная научно-темяческая конференция «Акгуалшьв проблемы анализа и обеспечения надежнешт и кажява приборе», у^ сбджтвдов -Пеша, 1998,-С 156-157

31 Тюгашев АА Псхярсттетешаупрашиюш^апгоршшгаб^мн^

Удивление д вижением и навигация леяагеяьных аппаратов сб научн. трУ Самарский филиал академии космонавтики -Самара, 1998 -С71-74

32 Капешьев АА, Тюгаикв АА Проектирование управляющих апгорщмов средавами обьекгноориентированного программирования // Управление движением и навигация летательных аппаратов, сб нг^^тр/С^марский^мпшчакадемиишдинавшш-СЫ^ 199&-С.68-71

33 Калальев АА, Тюгашев АА Алгебраические медаи и программные средотва для гртирежаншагюоригмшущншкниябэркжей апп^за1урсй//и^фрс®ьвмсдашвпроширс»аниии производавеРЭС. межвузовский сб научн. тр /ПГТУ -Пенза, 1996 -С 30-35

34 Кшендев АА, Ткхашев АА Языковые срерява системы автоматизированного синтеза алгоритмов управления реального врежни // Мевдунарсдая научно-техническая конференция «Амуальные проблемы ашлиза и обеспедазшнда^^ об дош. /ПГТУ-Пенза, 1996 С55-57

35 Калешъсв АА, Тюгашев АА Многоварианшый синтез алгоритме» управжния реального времени//УМ Всероссийский семинграс меад участием го уп)Х1В1]шию движением и навигации лешюлЕныхшщигов сб джгвдв /СГАУ -Самара, 1995 -С 19-25

36 Тюгашев АА Процессор выходных документов в системе автоматизации троекгирования управгиошихалгори1мв//Ш-йВсерсш1Йжий семинарасмеащ участием шупрашвнию д вижением и навигациилеяшепьныхаппарвгов об. доклад» /СГАУ -Самара, 1995 -С 17-19

37 Калешьев АА Тюгашев АА Разработка подсистемы синтеза управляющих алгоргамов на базе исчисления УА // Всероссийская н%чная школа «Кэмпыотфная алгебра, логика и интеллектов управление Проблемыанализастратетчесиэйсгайильносги>>гсб труда/И^ЦШРАН-1ф^тск),199Ф

Тезисы докладов:

38 Калешьев АА, Тюгашев АА Алгебраические и логические подасда к спецификации, верификации и синтезу управляющих программ для КА // 11-я Межаународная н^чно-техническая конференция «Системный анали^управление и давигация»тез дал/МАИ-М,2006 -С 171

39 Калетьев АА, Тюгашев АА Авгошпдарованное сдаивание характеристик управгет^^ программ БВС. // Международная научно-техническая конференция «Системный анализ, управление и навигаиия»тез джл./МАИ-М.,2005 -С. 101

40 Калешьев А А, Тюгашев А А Методы повышения качества при проектировании управляющих программ для космических аппаратов // Мевдународш конференция «Склемный анализ и управление» тез дркл./МАИ-М,2005 -С56

41 Калентьев АА, Тюгашев А А Технология проектирования надежных бортовых алгоритмов реального времени // 8-ая Международная конференция «Системный анализ и управление» тез докл / МАИ -M , 2003 - С 55

42 Калентьев А А, Тюгашев А А Автоматизация проектирования и отладки бортовых управляющих алгоритмов CASE-средствами // 7-ая Международная конференция «Системный анализ и управление» тез докл / МАИ-М, 2002 - С 51-52

43 Калентьев А А , Тюгашев А А Система автоматизации проектирования алгоритмов управления летательными аппаратами // б-я Международная конференция "Системный анализ и управление аэрокосмическими комплексами» тез докл / МАИ-М,2001 - С. 99

44 Калентьев А А , Тюгашев А А Моделирование алгоритмов управления асинхронными системами с дискретными состояниями // Тезисы докладов Международная космическая конференции, посвященной 40-летию первого полета человека в космос «Космос без оружия - арена мирного сотрудничества в XXI веке» тез докл / МАИ -Москва, 2001 С 50

45 Тюгашев А А Технология ГРАФКОНТ автоматизированного создания алгоритмов управления космическими аппаратами // XXVII н т к , посвященная 40-летию первого полета человека в космос «Гагаринские чтения» тез докл / МАТИ - Москва, 2001 С 19-20

46 Тюгашев А А Параметрическая генерация текста управляющей программы реального времени // XXVII н т к, посвященная 40-летию первого полета человека в космос «Гагаринские чтения» тез докл / МАТИ - Москва, 2001 -С 21

47 Калентьев А А , Тюгашев А А Использование многовходовой модели для представления управляющего алгоритма // Научно-техническая конференция «Перспективные информационные технологии в научных исследованиях, проектировании и обучении» тез докл / СГАУ - Самара, 1995 - С 65

48 Калентьев А А, Тюгашев А А Применение CASE-технологии для проектирования управляющих алгоритмов реального времени // Научно-техническая конференция «Перспективные информационные технологии в научных исследованиях, проектировании и обучении» тез докл / СГАУ - Самара, 1995 - С 64

49 Калентьев А А , Тюгашев А А Алгебраическая система синтеза УА // 1-ая Поволжская научно-техническая конференция «Научно-исследовательские разработки и высокие технологии двойного применения» тез докл / СГАУ -Самара, 1995 С 51-52

50 Тюгашев А А Автоматизация проектирования алгоритмов управления реального времени на основе алгебраических моделей // V-я научная межвузовская конференции «Математическое моделирование и краевые задачи» тез докл / СамГТУ - Самара, 1995 С 18

Подписано в печать 03 09 07 г Бумага офсетная Печать оперативная Объем 2 печ л Тираж 100 экз Закат № 896 Отпечатано в типографии AHO «Издательство СНЦ РАН» 443001, Самара,Студенческий пер, За тел (846)242-37-07

Введение.

1. Постановка проблемы.

1.1. Управление космическим аппаратом при решении целевых задач.

1.1.1. Структура системы управления космическим аппаратом.

1.1.2. Организация вычислительного процесса в БВС.

1.1.3. Управление КА при решении им целевых задач.

1.1.4. Структура комплекса БПО. Место УА РВ в комплексе программ БПО

1.2. Жизненный цикл БПО и его взаимосвязь с ЖЦ БВС и КА в целом.

1.3. Обзор существующих методов моделирования и автоматизации этапов ЖЦ ПО.

1.3.1. Основные проблемы, встающие при моделировании программ.

1.3.2. Использование временных логик.

1.3.3. Алгебраический подход к моделированию управляющих систем.

1.3.4. САЖ-мегодологии автоматизации этапов ЖЦ программных средств.

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

1.5. Выводы первого раздела.

2. Математические модели управляющих алгоритмов реального времени

2.1. Модель семантики управляющего алгоритма реального времени для БВС КА.

2.1.1. Построение модели семантики УАРВ.

2.1.2. Использование логических векторов для обусяавливания управляющих алгоритмов.

2.2. Многоосновная алгебраическая система УА РВ.

2.2.1. Алгебраическая система УА РВ.

2.2.2. Альтернативная интерпретация операций алгебраической системы УА РВ.

2.3. Построение формальных теорий УА РВ и их применение при спецификации управляющих алгоритмов реального времени.

2.3.1. Формальная теория управляющих алгоритмов.

2.3.2. Теория управляющих алгоритмов реального времени как эквациональная теория.

2.3.3. Формальная теория УА РВ как прикладное исчисление предикатов первого порядка.

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

2.4.1. Решение уравнений исчисления УА РВ.

2.5. Сравнение предлагаемого подхода УА РВ с известными временными логиками и алгебрами процессов.

2.6. Классификация предлагаемого подхода по парадигме программирования.

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

2.8. Использование среды логического программирования Пролог для представления формальной теории У А РВ.

2.9. Использование объектно-ориентированного программирования при реализации алгебраической системы УА РВ.

2.10. Производные модели У А РВ.

2.10.1. МноговходоваямодельУАРВ.

2.10.2. Многовариантная модель У А РВ.

2.10.3. Применение функций вьшолнимости дня описания УА РВ.

2.11. Выводы второго раздела.

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

3.1.1. Эквивалентные преобразования спецификаций управляющего алгоритма.

3.1.2. Оптимизация при синтезе плана управления (семантики УА).

3.1.3. Оптимизация при синтезе логико-временной схемы управляющего алгоритма.

3.1.4. Оптимизация при генерации программы на целевом языке программирования.

3.2. Выводы третьего раздела.

4. Технология автоматизации синтеза и верификации управляющих алгоритмов для БВС КА.

4.1. Стадии автоматизированной технологии.

4.2. Структура инструментального программного комплекса.

4.3. Автоматизация спецификации и верификации У А РВ.

4.3.1. Проблемно-ориентированный язык спецификации УА РВ.

4.3.2. Графическое конструирование семантики управляющего алгоритма.

4.4. Автоматизация синтеза управляющей программы.

4.4.1. Решение задачи трансляции спецификации и синтеза семантики У А РВ.

4.4.2. Решение задачи построения мношвходовой модели УА.

4.4.3. Параметрическая генерация управляющей программы.

4.5. Автоматизация построения технической документации на управляющий алгоритм.

4.5.1. Автоматическая генерация технической документации.

4.5.2. Графическое конструирование временных диаграмм.

4.6. Автоматизация тестирования и отладки УА РВ.

4.6.1. Решение задачи генерации отладочных заданий.

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

4.7. Реализация семантики управляющего алгоритма аппаратными средствами.

4.8. Интегрированная среда разработки управляющих алгоритмов и как РОМ-система.

4.9. Оценка эффективности разработанной технологии.

4.10. Выводы четвертого раздела.

5. Практическое применение разработанной технологии.

5.1. Применение технологии при разработке управляющего алгоритма режима приведения КА в ориентированное положение.

5.2. Использование разработанной технологии при моделировании отказов бортовой телеметрической системы.

5.2.1. Функции, структура и моделируемые режимы работы БИТС.

5.2.2. Функциональные задачи алгоритма моделирования неисправностей БИТС и логика его функционирования.

5.2.3. Методы моделирования потока отказов.

5.2.4. Описание алгоритма имитационного моделирования.

5.2.5. Синтез программы моделирования БИТС в рамках автоматизированной технологии.

5.3. Выводы пятого раздела.

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

Актуальность темы.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

БА) функционирование систем бортовой аппаратуры и программ комплекса БПО КА при решении им целевых задач.

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

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

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

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

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

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

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

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

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

Методы исследований основаны на использовании теории алгебраических систем, теории формальных систем, теории графов, декларативного, объектно-ориентированного и визуального подходов к программированию.

Научная новизна заключается в следующем:

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

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

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

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

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

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

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

Научная значимость состоит в том, что:

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

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

3. Построенная модель логико-временной схемы управляющего алгоритма применима для представления и анализа различных аспектов реализации программ реального времени в рамках приоритетной динамической дисциплины организации вычислительного процесса в БВС.

Практическая значимость определяется тем, что:

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

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

• визуальных средств (графического конструктора) для поддержки процесса спецификации требований к УА РВ;

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

• автоматического синтеза логико-временной схемы УА РВ, гарантированно реализующей требуемую семантику;

• автоматизированной генерации технической документации (блок-схемы и временной диаграммы) на управляющую программу;

• автоматической генерации управляющей программы на параметрически задаваемом целевом языке программирования;

• автоматического построения таблицы вариантов исполнения УА РВ, необходимой при отладке;

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

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

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

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

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

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

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

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

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

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

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

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

5.3. Выводы пятого раздела

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

2. Поставлена задача имитационного моделирования бортовой телеметрической системы, описываются применяемые при моделировании методы. Рассмотрены функции, структура и основные режимы работы БИТС.

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

Заключение

В диссертации получены следующие основные научные и практические результаты:

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

2. Построен формальный математический аппарат для описания УА РВ, в том числе впервые построена модель семантики УА РВ с адекватным отражением их временных и логических аспектов в виде набора кортежей, описывающих выполнение функциональных задач в заданные моменты времени: УА РВ = { Ф1 }, Ф1 = < % ть />, 1=1^.

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

4. Разработаны методы и средства синтеза УА РВ для БВС КА, включая:

• алгоритм генерации семантики УА РВ, соответствующей спецификации;

• алгоритм построения логико-временной схемы (структуры) УА РВ;

• методы и средства параметрической генерации управляющей программы, реализующей требуемую семантику УА РВ, на целевом языке программирования (включая ассемблер БЦВМ и язык Си).

5. Сформулированы критерии, предложены методы выбора проектных решений при синтезе УА РВ (структурной оптимизации) и проведено исследование их эффективности, в том числе:

• методов эквивалентных преобразований спецификаций УА РВ;

• методов оптимизации модели семантики УА РВ;

• методов оптимизации логико-временной схемы управляющего алгоритма;

• методов оптимизации при генерации управляющей программы, реализующей управляющий алгоритм.

6. Разработаны методы и средства верификации УА РВ, в том числе:

• проверки спецификации УА РВ на непротиворечивость путем применения логического вывода;

• проверки выполнимости спецификации УА РВ на заданном базисе ФЗ и поиска разрешающего базиса, в том числе с применением машины логического вывода среды логического программирования Пролог;

• верификации логико-временной схемы управляющего алгоритма (проверки соответствия реализуемой схемой семантики заданной спецификации УА РВ);

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

• автоматизированного построения таблицы информационных и управляющих связей УА РВ с другими программами БПО.

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

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

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

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

1. Авиастроение. Том 6 (Итоги науки и техники, ВИНИТИ АН СССР). М., 1978.

2. Теоретические основы проектирования информационно-управляющих систем космических аппаратов / В.В. Кульба, Е.А. Микрин, Б.В. Павлов, В.Н. Платонов; под ред. Е.А. Микрина; Ин-т проблем упр. Им. В.А. Трапезникова РАН.-М.:Наука, 2006.-579 с.

3. Лавров С.С. Программирование. Математические основы, средства, теория.-СПб.:БХВ-Петербург,2001.

4. Логика и компьютер. Моделирование рассуждений и проверка правильности программ / A.M. Анисов, П.И. Быстров и др.-М.-.Наука, 1990.

5. Калянов Т.Н. CASE. Структурный системный анализ (автоматизация и применение).-М.: Лори, 1996.

6. Норенков И.П. Основы автоматизированного проектирования. 2-е изд.-М.:Изд-во МГТУ им. Баумана, 2002.

7. Дружинин В.В., Конторов Д.С. Проблемы системологии (проблемы теории сложных систем). С предисловием акад. В.М. Глушкова. -М.:Сов.радио,1976.

8. Моисеев H.H. Расставание с простотой.-М.:"Аграф",1998.

9. Буч Г. Объектно-ориентированный анализ и проектирование с примерами приложений на С++:Пер. с англ.-М.:Бином;СПб.:Невский диалект, 1999.

10. Стандартизация разработки программных средств / Благодатских В.А. и др.;Под ред. О.С. Разумова.-М.:Финансы и статистика,2003.

11. П.Моисеев H.H. Математические задачи системного анализа.-М.:Наука, 1981.

12. Котов С.JI. Нормирование жизненного цикла программной продукции.-М.:ЮНИТИ-ДАНА, 2002.

13. Журавлев Ю.П. Системное проектирование управляющих ЦВМ.

14. М. -.Советское радио, 1974.

15. Ахо А., Сети Р., Ульман Д. Компиляторы: принципы, технологии иинструменты. :Пер. с англ.-М.:Изд. Дом «Вильяме», 2001.

16. Ахо А., Ульман Д. Теория синтаксического анализа, перевода икомпиляции в 2-х томах: Пер. с англ.-М.:Мир, 1978.

17. Буч Г., Рамбо Д., Джекобсон А. Язык UML. Руководство пользователя: Пер. с англ.-М.:ДМК, 2000.

18. Проблемы продвижения продукции и технологий на внешний рынок // Специальный выпуск. М,1997.

19. Вендров A.M. CASE-технологии. Современные методы и средства проектирования информационных систем.-М.:Финансы и статистика, 1998.

20. Липаев В.В. Выбор и оценивание характеристик качествапрограммных средств. Методы и стандарты.-М.:СИНТЕГ, 2001.

21. Управление космическими аппаратами зондирования

22. Земли компьютерные технологии / Д.И.Козлов, Т.П. Аншаков, Я.А. Мостовой, A.B. Соллогуб.-М.Машиностроение, 1998.

23. Соллогуб A.B., Аншаков Т.П., Данилов В.В. Космические аппаратысистем зондирования поверхности Земли. Под ред. Д.И. Козлова.-М. Машиностроение, 1993.

24. Боэм Б.У. Инженерное проектирование программного обеспечения.-М.:Радио и связь, 1985.

25. Динамика систем управления ракет с БЦВМ / В.Д. Арене, С.М.

26. Федоров, М.С. Хитрик, C.B. Лучко.-М.Машиностроение, 1972.

27. Баллистика и навигация космических аппаратов / Н.М. Иванов, Л.Н. Лысенко.- 2-е изд., перераб. и доп.-М.:Дрофа, 2004.

28. Денисов A.A., Колесников Д.Н. Теория больших систем управления.1. М.:Энергоиздат, 1982.

29. Калентьев A.A. Автоматизированный синтез алгоритмовасинхронного управления техническими системами с множеством дискретных состояний.-Самара,Самар.гос.аэрокосм.ун-т., 1998.

30. Богданов A.A. Тектология: Всеобщая организационная наука. В 2-х книгах.-М. ¡Экономика, 1989.

31. Брукс Ф. Мистический человеко-месяц или как создаются программные системы:Пер. с англ.-СПб.:Символ-Плюс, 1999.

32. Одинцов И.О. Профессиональное программирование. Системный подход.-СПб. :БХВ-Петербург, 2002.

33. Арчибальд Р. Управление высокотехнологичными программами ипроектами: Пер. с англ.-М.:ДМК Пресс, 2002.

34. Воеводин В.В., Воеводин В л.В. Параллельные вычисления.-СПб:БХВ1. Петербург, 2002.

35. Гордеев A.B., Молчанов А.Ю. Системное программное обеспечение.-СПб. Литер, 2002.

36. Орлов С.А. Технологии разработки программного обеспечения.1. СПб. .Питер, 2002.

37. Прангишвили И.В. Системный подход и общесистемные закономерности.-М.:СИНТЕГ, 2000.

38. Вермишев Ю.Х. Методы автоматического поиска решений при проектировании сложных технических систем.-М.:Радио и связь, 1982.

39. Вермишев Ю.Х. Основы автоматизации проектирования. -М.:Радио и связь, 1988.

40. Глушков В.М., Цейтлин Г.Е., Ющенко E.JI. Алгебра. Языки. Программирование.-Киев:Наукова думка, 1989.

41. Глушков В.М. Введение в кибернетику.-Киев:Изд-во АН УССР, 1964.

42. Глушков В.М. Синтез цифровых автоматов.-М.:Физматгиз, 1962.

43. Гайсарян С.С., Ластовецкий А.Л. Алгебраическая модель неймановских языков программирования //Программирование. 1984.-N6.-C12-22.

44. Дмитриев А.К., Мальцев П.А. Основы теории построения и контролясложных систем.-Л.:Энергоатомиздат,Ленингр.отд.,1988.

45. Тьюринг А. Может ли машина мыслить? -М.: Физматгиз,1950.

46. Нейман фон Дж. Теория самовоспроизводящихся автоматов. :Пер. сангл.-М. :Мир, 1971.

47. Винер Н. Кибернетика.:Пер. с англ.-М.:Сов. радио, 1968.

48. Берталанфи фон Л. Общая теория систем.-В кн. Исследования по общей теории систем.:Пер. с англ.-М.-.Прогресс,1969.

49. Директор Р., Ропер Р. Введение в теорию систем.:Пер. с англ.-М.Мир,1974.

50. Биркгоф. Теория структур.:Пер. с англ.-М.:ИЛ, 1952.

51. Котов В.Е. Сети Петри.-М.:Наука,1984.

52. Котов В.Е. Введение в теорию схем программ.-Новосибирск:Наука, Сиб.отд.-ние,1978.

53. Ершов А.П. Об операторных схемах Янова // Проблемы кибернетики,1967, вып. 20, С. 181-201.

54. Ершов А.П. Современное состояние теории схем программ.-Проблемы кибернетики, 1974, вып. 27,С.87-111.

55. Хетагуров Я.А. Основы проектирования управляющих вычислительных систем.-М.:Радио и связь, 1991.

56. Хакен Г. Синергетика.-М.:Мир, 1980.

57. Штрик A.A., Оссовский Л.Г. Структурное проектирование надежных программ встроенных ЭВМ.-Л.Машиностроение, Ленингр.отд.-ние, 1989.

58. Липаев В.В., Колин К.К., Серебровский Л.А. Математическоеобеспечение управляющих ЦВМ.-М.:Советское радио, 1972.

59. Мороз А.И. Курс теории систем.-М.:ВШ, 1987.

60. Майерс Г. Надежность программного обеспечения.-М.Мир, 1980.

61. Майерс Г. Искусство тестирования программ: Пер. с англ.-М.:Финансы и статистика, 1982.

62. Компьютерная алгебра: символические и алгебраические вычисления.

63. Под ред. Б. Бухбергера; Пер. с англ.-М.Мир, 1986.

64. Горбатов В.А. и др. САПР систем логического управления.-М. :Энергоатомиздат, 1988.62.3акревский А.Д. Алгоритмы синтеза дискретных автоматов.-М.:Наука, 1971.

65. Кейслер Г., Чэн И.И. Теория моделей:Пер.с англ.-М.Мир, 1977.

66. Мальцев А.И. Алгебраические системы. М.:Наука,1970.

67. Семантика языков программирования:Сб. статей.-М.Мир, 1980.

68. Сушков Б.Г. Проблемы проектирования вычислительных систем реального времени // Теория и реализация систем реального времени: Сб. тр. ВЦ АН СССР,-М, 1984.С.4-12.

69. Срагович Г.В., Сушков Б.Г. Реализация управляющей программы системы реального времени// Теория и реализация систем реального времени, сб. тр. ВЦ АН СССР, М., 1984, С.99-104.

70. Янов Ю.И. О логических схемах алгоритмов // Проблемы кибернетики.-М.:Физматгиз,1958.Вып.1. С.75-127.

71. Янов Ю.И. О равносильности и преобразованиях схемпрограмм//Доклады АН СССР,1957, т.113, №1, с.39-42.

72. Ляпунов A.A. О логических схемах программ// Проблемыкибернетики, вып. 1, 1958, М., Физ. мат. литер., С.46-75

73. Математическая логика в программировании. Сборник статей 19801988гг.: Пер. с англ.-М.Мир, 1990.

74. Математическая энциклопедия / Под ред.Виноградова И.Н.

75. М:Советская энциклопедия, 1982. 73.Основы синтеза структуры сложных систем.-М.:Наука, 1982.

76. Пиотровский Р.Г. Инженерная лингвистика и теория языка.-Л.:Наука,1. Ленинградское отд., 1979.

77. Рвачев A.A. Математика и семантика. Номинализм как интерпретация математики. Киев, Наукова думка, 1966.

78. Рубашкин В.И. Представление и анализ смысла в интеллектуальных информационных системах. М.:Наука,1989.

79. Современная прикладная алгебра / Г.Биркгххоф, Т.Барти и др.:Пер.сангл.-М.:Мир,1976.

80. Свами М., Тхуласираман К. Графы, сети и алгоритмы:Пер. с англ.-М.:Мир,1984.

81. Синтез управляющих автоматов. / Лазарев В.Г., Пийль Е.И.

82. М. :Энергоатомиздат, 1989.

83. Маркус С. Теоретико-множественные модели языков // М., Наука, 1970, 332с.

84. Типы данных в языках программирования и базах данных.

85. Новосибирск:Наука,Сибирское отд., 1987.

86. Успенский В.А., Семенов А.Л. Теория алгоритмов: основные открытия и приложения.-М. :Наука, 1987.

87. Фрид Э. Элементарное введение в абстрактную алгебру: Пер. с англ.-М.,Мир,1979.

88. Хубка В. Теория технических систем: Пер с нем.-М.:Мир,1987.

89. Крылов С.М. Формальная технология в философии, технике, биоэволюции и социологии.-Самара:СамГТУ,1997.

90. Клини С.К. Введение в метаматематику.-Пер. с англ.-М.:ИЛ,1957.

91. Клини С.К. Математическая логика.-Пер. с англ.-М.:Мир, 1973.

92. Марков A.A., Нагорный Н.М. Теория алгорифмов.-М.:Наука, Физматлит, 1984.

93. Крылов С.М. Формальная технология и универсальные системы // Кибернетика (современное название Кибернетика и системный анализ), 1986,№4,С.85-С89.

94. Крылов С.М. Формально-технологические модели в общей теориисистем. // Известия Самарского научного центра РАН, т.5, №1,2003,С.83-С.90.

95. Карпов Е.М. Об алгебре физических взаимодействий. //

96. Математическое обеспечение САПР:Межвуз.сб.наун.тр.-Куйбышев,КуАИ,1989.-С20.-С.29.

97. Калентьев A.A., Лихачев Ю.Д. Формирование модели управляющего алгоритма над структурированным базисом. // Математическое обеспечение САПР:Межвуз.сб.наун.тр.-Куйбышев,КуАИ, 1989.-С 8-С20.

98. Ван дер Варден, Бертел Ландерт. Алгебра: Пер.с англ.-М.:Наука,1987.

99. Шрейдер Ю.А. О понятии "математическая модель языка" М. Знание, 1971.

100. Шрейдер Ю.А. Равенство. Сходство. Порядок.-М.-.Наука, 1971.

101. Шрейдер Ю.А. К определению системы. // Научно-техническая информация. Сер. 2., 1971, №7.

102. Шрейдер Ю.А., Шаров A.A. Системы и модели.-М.:Радио и связь, 1982.

103. Юдицкий С.А., Магерут В.З. Логическое управление дискретными процессами: Модели, анализ, синтез.-М.-.Машиностроение, 1987.

104. Янг Стивен Дж. Алгоритмические языки реального времени: Пер. с англ.-М. Мир,1985.

105. Языки логического управления.-Минск:Наука и техника,1975.10111 Всесоюзное совещание по автоматизации программирования ПО систем управления движущимися объектами : Тез.докл.-Харьков,ХАИ, 1989.

106. Соколов А.П. Системы программирования: теория, методы, алгоритмы.-М.:Финансы и статистика, 2004.

107. Никифоров А.Д. Управление качеством: Учеб. пособие для вузов.-М.:Дрофа, 2004.

108. Касьянов В.Н., Евстигнеев В.А. Графы в программировании: обработка, визуализация и применение.-СПб.:БХВ-Петербург, 2003 -1104 е.: ил.

109. Боровский А.Н. С++ и Pascal в Kylix 3. Разработка Интернет-приложений и СУБД.-СПб. :БХВ-Петербург, 2003.

110. Critical analisys of tools for CASE / Crosier M, Glass D, Hughes J, Johnston W, McChessney I // Inf. and Software technologies, 1989,N9-pp486-496.

111. Debugging and monitoring highly parallel systems with GRIP / Venables P.J., Zeda H // Microprocesing and microprogramming -1990-28-N1-5 pp 79-84.

112. Evolution towards speciifications environment: expierences wyth syntax editors / Zelcomitch M.V. // Inf. and Software Technologies-1990-32-N3 pp 191-198.

113. Heylighen F. Basic concepts of the System Approach. "Principia Cybernetica Project", March 6, 2000.

114. Broenihk K.J.F., Hilderuk G.H., Bakkers A.W.P. Building Blocks for Embedded Control Systems. Proceedings PROGRESS 2000 workshop on Embedded Systems, 12-10-2000, Utrecht, STW, 2000, pp. 27-33.

115. Bunge M. Things // Int J of General Systems, 1974, VI, pp 229-236.

116. Priorities in process algebras / Cleaveland Ranee, Henneysey Matthew // Inf. and Computers-1990-87-N1-2 pp 58-77.

117. The object-oriented structured design notation for software design representation / Wasserman Anthony, Pircher Peter A,Muller Robert // Computer -1990-23-N3,pp 50-63.

118. STATEMATE: A working environment for the development of complex reactive systems / Hatel David, Lachover Hagi, Naamad Amnon, Paveli Ahir, etc. // IEEE Trans. Software Engineering-1990-16-N4 pp 403-444.

119. Annevelink I., Dewilde P. Object oriented date management based on abstract date types /Software Pract. And Exper, 1987, 17, N 1 l,pp 757782.

120. De Wolf J.B. Requirements specification and preliminary design for real time systems / COMPSAC 77. Proc. IEEE Comput. Soc.l. Int. Comput. Software and Appl. Conf., Chicago, New York, 1977, pp 17-23.

121. Huthagel S.P., Brown J.C. Performance properties of vertically partitioned object oriented systems / IEEE Trans. Software Eng., 1989, 15, N8, pp 935- 946.

122. Kaplan G. Application of CASE tools and object oriented programming to the software development process / IEEE Int. Conf. Comman.: World Prosp. Through Commun., Boston, Mass., June 11- 14, 1989, BOSTONIOC 89, v.3, N.Y.,pp 1319- 1323.

123. Royce, Walker W. Managing the development of large software systems: concepts and techniques. Proc. IEEE WESTCON, Los Angeles, August 1970, pp. 1-9.

124. Rothenberg I. Object oriented simulation: where do we go from here? / Winter Simil. Conf.Proc., Washington, Dec. 8-10, 1986, N.Y., pp 464469.

125. Ulden O.M., Thomasma T., Yonui M. Object oriented toolkits for simulation program generators / Winter Simil. Conf.Proc., Washington, Dec. 4-6, 1989, N.Y.,pp 593- 600.

126. Wilson R. Object oriented languages reorient programming techniques / Computer Design, 1987, 26, N20, 52-62.

127. Halpern J., Rabin M. A logic to reason about likelihood // Artificial Intelligence. 1987. Vol.32. P.379-405.

128. Pnueli A. The temporal logic of programs // Proc. 18th IEEE symp. on the foundations of computer science. San Francisco, 1977. P.46-57.

129. Pnueli A. A temporal semantic of concurrent programs // TCS. -1981.-№12.-P .45-60

130. Manna, Z., Pnueli A.: The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, 1992

131. Ben-Ari M., Manna, Z., Pnueli A.: The Temporal Logic of Branching Time. Proc. 8th Annual Symposium on Principles of Programming Languages, 1981, ACM Press, Williamsburg, p. 164-176. SpringerVerlag, 1992.

132. Baeten J.C.M., Bergstra J.A.: Real time Process Algebra. Formal Aspects of Computing, 3, p.142-188, 1991.

133. J.S. Ostroff. Temporal Logic of Real-time Systems. Research Studies Press, 1990.

134. R. Koymans. Specifying real-time properties with metric temporal logic. Real-time Systems, 2(4):255-299, 1990.

135. J.C.M. Baeten, С. Middleburg. Process Algebra with timing. EATCS Monographs. Springer Verlag, 2002.

136. J.W. de Bakker, J.J. Zucker. Denotational Semantics of concurrency. Proc. 14th Symp. Theory of Computation. ACM, 1992.

137. G.M. Reed, A.W. Roscoe. A timed model for communicating sequential processes. Theoretical Computer Science, 1988.

138. X.Nicollin, J. Sifakis. The algebra of timed processes ATP: Theory and application. Information and Computation, 1994.

139. S.A. Schneider. Concurrent and Real-Time Systems (the CSP Approach). Worldwide series in Computer Science. Wiley, 2000.

140. S. Yovine. Kronos: A verification tool for real-time systems. Journal of Software Tools for Technology Transfer, 1997.

141. J. A. Bergstra, C. A. Middelburg. Model Theory for Process Algebra. 2002

142. J. F. A. K. van Benthem, J. A. Bergstra Logic of transition systems. Journal of Logic, Language and Information, 3:247-283, 1995.

143. J. F. A. K. van Benthem, D. J. N van Eijck, V. Stebletsova. Modal logic, transition systems and processes. Journal of Logic and Computation, 4:811-855, 1994.

144. Xoop 4. A. 3. Непротиворечивые взаимодополняющие теории семантики языков программирования // В сб.:Семантика языков программирования.-М. Мир, 1980

145. Бусленко Н.П., Калашников В.В., Коваленко И.Н. Лекции по теории сложных систем. М.: «Сов.радио», 1973.

146. Парийская Е.Ю. Сравнительный анализ математических моделей и подходов к моделированию и анализу непрерывно-дискретных систем. // Дифференциальные уравнения и процессы управления. №1, 1997.

147. Henzinger T., Nicollin X., Sifalis J., Yovine S.: Symbolic ModelChecking for Real-Time Systems. In Proc. 7th LICS. IEEE Comp. Soc. Press, 1992.

148. Kroger, F. Temporal Logic of Programs EATCS Monographs on Theoretical Computer Science,Springer Verlag, 1987.

149. Halpern, J., Manna, Z., and Moszkowski, B., A Hardware Semantics Based on Temporal Intervals, in Lecture Notes on Computer Science, 154, 1983,278-291.

150. Allen, J.F Towards a General Theory of Action and Time Artificial Intelligence, 23(2), July 1984, pp. 123-154.

151. Koymans R., and De Roever, W.P. Examples of a Real-time Temporal Logic Specification, in Lecture Notes in Computer Science, 207, 1985, 231-251.

152. Koymans, R., Kuiper, and R., Zijlstra, E., Specifying message passing and real-time systems with real-time temporal logic, in ESPRIT '87 Achievement and Impact, North Holland, 1987, 311-324.

153. Koymans, R. Specifying Message Passing and Time-Critical Systems with Temporal Logic. Ph.D. Dissertation, Eindhoven University of Technology, 1989.

154. Ghezzi, C., Mandrioli, D., and Morzenti, A. TRIO, a Logic Language for Executable Specifications of Real-Time Systems. Journal of Systems and Software, 12, 2 (May 1990), 107-123.

155. Ghezzi, С., Mandrioli, D., and Morzenti, A. TRIO, a Logic Language for Executable Specifications of Real-Time Systems, in Proceedings of 10th French-Tunisian Seminar on Computer Science, (1989), 322-349.

156. Narayana, K.T., and Aaby, A. A. Specification of Real-Time Systems in Real-Time Temporal Interval Logic. Proceedings of IEEE Symposium on Real-Time Systems, (1988), 86-95.

157. Attiya, H., Lynch, N.A. Time Bounds for Real-Time Process Control in the Presence of Timing Uncertainty. IEEE Symposium on Real-Time Systems (1989).

158. Lynch, N., and Attiya, H. Using Mappings to Prove Timings Properties, in Proceedings of ACM Conference on Principles of Distributed Computing, 1990.

159. Калман P., Фалб П., Арбиб M. Очерки по математической теории систем. М.:Мир, 1971.

160. J.C.M. Baeten. The total order assumption. In S. Purushothaman and A. Zwarico, editors, Proceedings First North American Process Algebra Workshop, Workshops in Computing, pages 231-240. Springer Verlag, 1993.

161. H. Bekijc. Towards a mathematical theory of processes. Technical Report TR 25.125, IBM Laboratory Vienna, 1971.

162. H. Bekijc. Programming Languages and Their Definition (Selected Papers edited by C.B. Jones). Number 177 in LNCS. Springer Verlag, 1984.

163. J.A. Bergstra and J.W. Klop. Fixed point semantics in process algebra. Technical Report IW 208, Mathematical Centre, Amsterdam, 1982.

164. R. Milner. A Calculus of Communicating Systems. Number 92 in Lecture Notes in Computer Science. Springer Verlag, 1980.

165. R. Milner. An approach to the semantics of parallel programs. In Proceedings Convegno di informatica Teoretica, pages 285-301, Pisa, 1973. Instituto di Elaborazione della Informazione

166. R. Milner. Processes: A mathematical model of computing agents. In H.E. Rose and J.C. Shepherdson, editors, Proceedings Logic Colloquium, number 80 in Studies in Logic and the Foundations of Mathematics, pages 157-174. North-Holland, 1975.

167. R. Milner. Flowgraphs and flow algebras. Journal of the ACM, 26(4):794-818, 1979.

168. G.J. Milne and R. Milner. Concurrent processes and their syntax. Journal of the ACM, 26(2):302-321, 1979.

169. R. Milner. Algebras for communicating systems. In Proc. AFCET/SMF joint colloquium in Applied Mathematics, Paris, 1978.

170. R. Milner. Synthesis of communicating behaviour. In J. Winkowski, editor, Proc. 7th MFCS, number 64 in LNCS, pages 71-83, Zakopane, 1978. Springer Verlag.

171. C.A.R. Hoare. Communicating sequential processes. Communications of the ACM, 21(8):666-677, 1978.

172. M. Hennessy and R. Milner. On observing nondeterminism and concurrency. In J.W. de Bakker and J. van Leeuwen, editors, Proceedings 7th ICALP, number 85 in Lecture Notes in Computer Science, pages 299309. Springer Verlag, 1980.

173. D.M.R. Park. Concurrency and automata on infinite sequences. In P. Deussen, editor, Proceedings 5th GI Conference, number 104 in LNCS, pages 167-183. Springer Verlag, 1981.

174. G.D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Aarhus University, 1981.

175. G.D. Plotkin. The origins of structural operational semantics. Journal of Logic and Algebraic Programming, To appear, 2004. Special Issue on Structural Operational Semantics.

176. E.W. Dijkstra. Guarded commands, nondeterminacy, and formal derivation of programs. Communications of the ACM, 18(8):453—457, 1975.

177. C.A.R. Hoare. A model for communicating sequential processes. In R.M. McKeag and A.M. Macnaghten, editors, On the Construction of Programs, pages 229-254. Cambridge University Press, 1980.

178. R.W. Floyd. Assigning meanings to programs, in Schwartz J.T. (ed.): Mathematical aspects of computer science / Proc. Symposia in Applied Mathematics 19, Providence (R. I.), Amer. Math. Soc. 1967, pp. 19-32.

179. C.A.R. Hoare. An axiomatic basis for computer programming. Comm. ACM 12 (1967), pp 576-580.

180. C.A. Petri. Introduction to general net theory. In W. Brauer, editor, Proc. Advanced Course on General Net Theory, Processes and Systems, number 84 in LNCS, pages 1-20. Springer Verlag, 1980.

181. A. Mazurkiewicz. Concurrent program schemes and their interpretations. Technical Report DAIMI PB-78, Aarhus University, 1977.

182. M. Rem. Partially ordered computations, with applications to VLSI design. In J.W. de Bakker and J. van Leeuwen, editors, Foundations of Computer Science.

183. K.R. Apt, N. Francez, and W.P. de Roever. A proof system for communicating sequential processes. TOPLAS, 2:359-385, 1980.

184. J.W. de Bakker and J.I. Zucker. Processes and the denotational semantics of concurrency. Information and Control, 54:70-120, 1982.

185. J.A. Bergstra and J.W. Klop. A convergence theorem in process algebra. In J.W. de Bakker and J.J.M.M. Rutten, editors, Ten Years of Concurrency Semantics, pages 164-195. World Scientific, 1992.

186. R. Milner. Calculi for synchrony and asynchrony. Theoretical Computer Science, 25:267-310, 1983.

187. G.J. Milne. CIRCAL: A calculus for circuit description. Integration, 1:121-160,1983.

188. D. Austry and G. Boudol. Alg'ebre de processus et synchronisation. Theoretical Computer Science, 30:91-131, 1984.

189. M. Hennessy. Algebraic Theory of Processes. MIT Press, 1988.

190. J.C.M. Baeten, J.A. Bergstra, C.A.R. Hoare, R. Milner, J. Parrow, and R. de Simone. The variety of process algebra. Deliverable ESPRIT Basic Research Action3006, CONCUR, 1991.

191. J.-C. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier, and M. Sighireanu. CADP (CAESAR/ALDEBARAN development package): A protocol validation and verification toolbox. In R. Alur and T.A.

192. Henzinger, editors, Proceedings CAV '96, number 1102 in Lecture Notes in Computer Science, pages 437-440. Springer Verlag, 1996.

193. J.F. Groote and M.A. Reniers. Algebraic process verification. In 25., pp. 1151-1208,2001.

194. Wang Yi. Real-time behaviour of asynchronous agents. In J.C.M. Baeten and J.W. Klop, editors, Proceedings CONCUR'90, number 458 in LNCS, pages 502-520. Springer Verlag, 1990.

195. F. Moller and C. Tofts. A temporal calculus of communicating systems. In J.C.M. Baeten and J.W. Klop, editors, Proceedings CONCUR'90, number 458 in LNCS, pages 401-415. Springer Verlag, 1990.

196. K.G. Larsen, P. Pettersson, andWang Yi. Uppaal in a nutshell. Journal of Software Tools for Technology Transfer, 1, 1997.

197. Y.S. Usenko. Linearization in (xCRL. PhD thesis, Technische Universiteit Eindhoven, 2002.

198. Еленев В.Д. Моделирование процессов функционирования космических аппаратов с использованием сетевых подходов / В.Д. Еленев. Самара: Изд-во Самарского научного центра РАН, 2006.-108с.:ил.

199. Дискретная математика для программистов / Ф.А. Новиков.-СПб. Литер, 2002.-304 с.:ил.

200. Тюгашев А.А. Многоязыковый процессор автоматизированного описания управляющих алгоритмов. Дисс. на соискание ученой степени канд. техн. наук, Самара, 1997.

201. Тюгашев A.A. Интегрированная среда для проектирования управляющих алгоритмов реального времени // Известия РАН. Теория и системы управления, №2, 2006, с. 128-141.

202. Норенков И.П., Кузьмик П.К. Информационная поддержка наукоемких изделий. CALS-технологии.-М. :Изд-во МГТУ им. Баумана,2002.

203. Требования и спецификации в разработке программ: Пер. с англ.-М.:Мир, 1984.-344 е.,ил.

204. Непейвода H.H., Скопин И. Н. Основания программирования.— Ижевск-Москва: РХД, 2003.

205. Трусов B.C. Система визуального конструирования бортовых алгоритмов управления. Дисс. на соискание уч. степени кандидата техн. наук. Самара, 2005.