Денотативно-объектная модель вычислений для встроенных систем

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

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

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

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

В наибольшей степени указанным требованиям отвечают модель сигналов с тэгами (Tagged Signal Model, TSM) E.A. Lee и A. Saiigiovanni-Vincentelli и объектно-событийная модель вычислений (ОСМВ) Постникова II.П. Тем не менее, они обладают рядом серьезных недостатков и ограничений.

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

Для достижения указанной цели в работе были решены следующие задачи:

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

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

3. Исследование формальных свойств вычислительного процесса в рамках предложенной модели.

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

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

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

7. Исследование возможностей сопряжения предложенной модели вычислений с другими моделями вычислений встроенных систем, а также условий их иерархического гетерогенного моделирования.

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

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

Научная новизна работы:

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

2. Показано, что вычислительный процесс в рамках предложеной модели вычислений обладает детерминизмом, не может иметь каузальных циклов и зеноно-вых поведений.

3. Предложен механизм на основе ряда ограничений, позволяющий иерархическое сопряжение ДОМВ с классом моделей вычислений, удовлетворяющих актива-ционной абстрактной семантике. На примере трех моделей вычислений из этого класса показано, что такое объединение не противоречит их семантикам.

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

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

6. На основе понятий связи функциональных блоков и временного масштаба модели сформулированы критерии качества модели.

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

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

Предложена методика высокоуровневого проектирования встроенных вычислителей на платформе «Терра» с использованием разработанного прототипа САПР. Разработаны инструменты автоматического анализа планируемости и частичной трансляции поведенческих моделей в исходный код на языке С. Разработан уровень поддержки ДОМВ в ОС реального времени «Терра», обеспечивающий взаимодействие задач и ресурсов платформы в рамках предложенной модели вычислений.

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

Элементы предложенной модели вычислений применены в более, чем 10 НИР и НИОКР. Наиболее показательными из них следует считать: система контроля и управления моноимпульсного вторичного радиолокатора «Аврора» и программно-аппаратная платформа прикладных вычислителей встроенных систем «Терра». Результаты работы использованы в учебных курсах кафедры Вычислительной техники СПбГУ ИТМО в рамках инженерной и магистерской подготовки по специализациям «Информационно-управляющие системы» (230 101.65.12) и «Системы реального времени» (230 100.68.20), а также в рамках учебных модулей «Проектирование встроенных вычислительных систем» и «Схемотехника интегральных вычислителей» инновационной образовательной программы СПбГУ ИТМО.

Апробация работы произведена в 8 докладах на 7 международных и всероссийских конференциях. Основные результаты опубликованы в 7 работах. Работа поддержана грантом правительства Санкт-Петербурга 03/3.11/15−03/14 в рамках конкурса грантов студентов и аспирантов 2007 года.

Список аббревиатур

ВсС Встроенные системы.

ДС Дискретно-событийный сигнал или модель вычислений с дискретными событиями.

ОСМВ Объектно-событийная модель вычислений Постникова Н.П.

ОСРВ Операционная система реального времени.

ПЛК Программируемый логический контроллер.

ПЛИС Программируемая логическая интегральная схема.

САПР Система автоматизированного проектирования.

СПД Сети с потоками данных. Множество вариантов модели вычислений Dataflow Process Networks.

ФБ Функциональный блок.

ASIC Application-Specific Integrated Circuit. Заказная (специализированная) интегральная схема.

CPLD Complex Programmable Logic Device. Вариант архитектуры современных ПЛИС.

FPGA Field-Programmable Gate Array. Вариант архитектуры современных ПЛИС.

GC Garbage Collector. Механизм учета и автоматического высвобождения неиспользуемой динамически выделенной памяти.

IP Intellectual Property. Завершенный аппаратный компонент для применения в системах на кристалле.

HW Hardware. Аппаратное обеспечение вычислительных систем.

RTL Register Transfer Level. Уровень регистровых пересылок описания аппаратуры.

SoC System-On-a-Chip. Система на кристалле.

SW Software. Программное обеспечение вычислительных систем.

TSM Tagged Signal Model. Модель сигналов с тэгами Е.А. Lee и A. Sangiovanni-Vincentelli.

WCET Worst-Case Execution Time. Время выполнения в наихудшем случае. Пессимистичная оценка времени выполнения алгоритма или задачи реального времени (без учета влияния других компонентов вычислительного процесса).

Результаты работы применены в учебных курсах кафедры Вычислительной техники СПбГУ ИТМО в рамках инженерной и магистерской подготовки по специализациям «Информационно-управляющие системы» (230 101.65.12) и «Системы реального времени» (230 100.68.20), а также в рамках учебных модулей «Проектирование встроенных вычислительных систем» и «Схемотехника интегральных вычислителей» инновационной образовательной программы СПбГУ ИТМО.

Заключение

.

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

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

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

3. Предложен механизм на основе ряда ограничений для сопряжения ДОМВ с классом моделей вычислений, удовлетворяющих активационной абстрактной семантике. На основе анализа семантики моделей СПД, ДС, СР и НВ из этого класса, а также проведенных экспериментов показана возможность и выявлены условия гетерогенного моделирования с использованием ДОМВ.

Основные практические результаты работы:

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

2. Предложена методика высокоуровневого проектирования встроенных вычислителей на платформе «Терра» с использованием разработанного прототипа САПР. Разработаны средства частичной трансляции поведенческих моделей в исходный код на языке С. Реализован уровень поддержки семантики ДОМВ в ОС реального времени платформы «Терра» .

3. На основе сформулированных требований даны рекомендации по иерархическому сопряжению ДОМВ в рамках гетерогенного моделирования.

4. Предложена методика анализа и формальной верификации моделей в рамках ДОМВ и разработан алгоритм вычисления временных характеристик модели, которые апробированы в разработанном прототипе САПР.

Эффективность полученных в работе результатов подтверждается их успешным применением в более, чем 10 НИР и НИОКР по созданию ВсС различного назначения, сложности и архитектуры. Наиболее показательными из них следует считать: система контроля и управления моноимпульсного вторичного радиолокатора «Аврора» и программно-аппаратная платформа прикладных вычислителей встроенных систем «Терра» .