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

• Тюгашев, Андрей Александрович
• доктор технических наук
• 2007

Оглавление диссертации доктор технических наук Тюгашев, Андрей Александрович

Введение.

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%) снижения общей трудоемкости этапов ЖЦ УА РВ для БВС КА.

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

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

Список литературы диссертационного исследования доктор технических наук Тюгашев, Андрей Александрович, 2007 год

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.