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

ииз171646

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

ЛУКИЧЕВ АЛЕКСАНДР НИКОЛАЕВИЧ

ДЕНОТАТИВНО-ОБЪЕКТНАЯ МОДЕЛЬ ВЫЧИСЛЕНИЙ ДЛЯ ВСТРОЕННЫХ СИСТЕМ

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

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

Санкт-Петербург 2008

о 5 ''ЮН да

003171646

Работа выполнена в Сапкт-Петербургском Государственном Университете Информационных Технологий, Механики и Оптики

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

Платунов Алексей Евгеньевич

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

Гатчин Юрий Армепакович

доцент, кандидат технических наук Григорьев Валерий Владимирович

Ведущее предприятие ИАнП РАН (Институт аналитического

приборостроения Российской академии наук) г Санкт-Петербург

Защита диссертации состоится 17 июня 2008 г в 15 часов 50 минут на заседании Совета по защите докторских и кандидатских диссертаций Д212 227 05 при Санкт-Петербургском Государственном Университете Информационных Технологий, Механики и Оптики по адресу 197101, Санкт-Петербург, Кронверкский пр , д 49

С диссертацией можно ознакомиться в библиотеке Санкт-Петербургского Государственного Университета Информационных Технологий, Механики и Оптики

Автореферат разослан 16 мая 2008 I

Ученый секретарь

Совета Д212 227 05, к т н , доцент /И-Ок/I Поляков Владимир Иванович

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ Актуальность темы Встроенные системы (ВсС) традиционно понимаются как специализированные цифровые вычислительные системы, непосредственно взаимодействующие с объектом контроля или управления и ооъединенные с ним однии ким^к/лцл« Еуртл-информационных технологий, информатизация общества и стремление к автоматизации многих задач человеческой деятельности правело в последнее десятилетие к массовому применению встроенных систем не точько в промышленности, медицине, на транспорте и других высокотехнологичных областях, но и в повседневной жизни Спрос на ВсС неуклонно растет, а вместе с ним растут и требования к этим продуктам

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Внедрение результатов работы Элементы предложенной модели вычислений применены в более, чем 10 НИР и НИОКР Наиболее показательными из них следует считать система контроля и управления моноимпульсного вторичного радиолокатора "Аврора" и программно-аппаратная платформа прикладных вычислителей встроенных систем "Терра" Результаты работы использованы в учебных курсах кафедры Вычислительной техники СПбГУ ИТМО в рамках инженерной и магистерской подготовки по специализациям "Информационно-управляющие системы" (230101 65 12) и "Системы реального времени" (230100 68 20), а также в рамках учебных модулей "Проектирование встроенных вычислительных систем" и "Схемотехника интегральных вычислителей" инновационной образовательной программы СПбГУ ИТМО

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

Структура и объем работы Диссертация состоит из введения, четырех глав и заключения Список использованной литературы составляет 89 наименований Текст диссертации содержит 160 страниц машинописного текста, 43 рисунка, 4 таблицы и 4 приложения

СОДЕРЖАНИЕ РАБОТЫ Во введении обоснована актуальность темы, сформулирована цель и задачи исследования,

перечислены теоретические и практические положения, выносимые на защиту

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

Современные методики проектирования, такие как HW/SW CoDesign, илатформно-ориен-тированное и акторное проектирование, аспектная технология выделяют уровень абстрактаой модели поведения системы, жестко привязанной к требованиям прикладной задачи и слабо зависящей от способа программно-аппаратной реализации на конкретной элементной базе Формальный язык, на котором производится высокоуровневое поведепческое описание системы, имеет в своей основе некоторую семантику, или "модель вычислений", задающую смысл и правила взаимодействия компонент вычислительного процесса Модель вычислений накладывает ограничения на вычислительный процесс, за счет которых возможен формальный анализ его свойств Проанализированы широко используемые при проектировании ВсС дискретно-событийная (ДС) модель, модель синхронно-реактивных (CP) систем, сети потоков данных (СПД) Отмечены проблемы, связанные l их использованием В частности, отмечено, что СПД в явном виде не учитывает управляющий, a CP информационный аспект ВсС ДС так ели иначе позволяет сочетание указанных аспектов, однако является довольно универсальной моделью, использование которой сопряжено с проблемами каузальных циклов, зеяоновых поведений, Heoi раниченного объема требуемой памяти и т д

Проанализирована модель сигналов с тэгами (Tagged Signal Model, TSM) E A Lee и A Sangiovanm-Vmcentelli, предоставляющая в высшей степени абстрактное описание вычислительного процесса как системы сигналов и их функциональных преобразований В противовес операционной семантике вычислений, модель названа авторами денотативной (deaotational) TSM предоставляет понятийную и теоретическую базу формального анализа и верификации модели вычислительного процесса и предназначена для сравнения друг с другом различных моделей вычислений, выделения общих и специфических формальных свойств моделей и исследования вопросов их иерархического сопряжения Ввиду своей абстрактности, TSM одипаково

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

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

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

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

На основе сделанных выводов и выявленных недостатков ОСМВ сформулирована цель исследования и задачи, коюрые необходимо решить для ее достижения

Во второй главе на основе объектно-событийной модели вычислений (ОСМВ) и модели сигналов с ягами (TSM) предложена денотативно-объектная модель вычислений (ДОМВ), в которой совмещены достоинства обеих исходных моделей

В рамках предложенной модели, вычислительный процесс представляет собой сеть абстрактных вычислителей (функциональных блоков ОСМВ), взаимодействующих с помощью сигналов Сигнал (в терминах TSM) есть функция s Т —» V, частично определенная на множестве временных меток Т и приписывающая метке времени некоторый элемент новых (появившихся в момент t) дапных s(t) € V Отсутствие новых данных в сигнале моделируется специальным значением е е V В качестве модели времени Т используется множество К+ U {оо}, как про-

стая и в то же время достаточно универсальная форма его представления Таким образом, любой сигнал между ФВ можно представить множеством отдельных событий появления новых данных {Mi))}, строго упорядоченным по их временным меткам t

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

Выходы ФБ нестрого зависят от его синхронного входа j, если для генерации одного или нескольких сигналов на выходе достаточно инструкций только по входу j

Дано денотативное (в терминах TSM) описание ФБ и его формальных свойств ФБ представляет собой функционал F;ь {Pln —> S} —» {Р„ —> S], где Рт есть множество его входных портов, Р0 множество выходных, a S множество сигналов в системе При эгом, Ffb непрерывна (по Скотту) и, если Р0 непустое, строго каузальна Интуитивно, строгая каузальность подразумевает генерацию результатов вычислений строго после соответствующих запросов, но не одновременно с ними Формальное определение понятия дано авторами TSM Строгая каузальность позволяет избежать проблемы циклических зависимостей сигналов в модели, присущей ДС, CP и СПД системам Функциональная зависимость выходных сигналов от входных означает детерминизм ФБ, под которым понимается свойство всегда одинаковым образом реагировать на одну и ту же последовательность входпых воздействий С помощью математического аппарата TSM показано, что любая сеть ФБ будет также обладать свойствами детерминизма, непрерывности и строгой каузальности

Реактивные свойства ФБ задаются атрибутами его синхронных портов каждый синхронный вход имеет атрибут 7, задающий минимальный интервал между принимаемыми инструкциями, с которым ФБ способен их обрабатывать (время отклика), а выход имеет атрибут ш, задающий минимальный интервал времени между генерируемыми на нем событиями (результатами) Действительное значение атрибута синхронного порта (7 или ш) характеризует наблюдаемый на входе или выходе сигнал, и задает требуемое в контексте системы от ФБ время отклика или получаемую интенсивность выходного сигнала соответственно Для введенных атрибутов соблюдается условие 7 < 7 и и < й, то есть синхронный порт допускает только сигналы, интервалы между событиями в которых не меньше соответствующего атрибута Показано, что ДОМВ не допускает зеноновых поведений, проявляющихся при дискретно-событийном моделировании управления объектами с непрерывной динамикой как бесконечное сокращение интервалов между событиями в одном или нескольких ДС-сигналах и возникающим вследствие "мгновенной" реакции системы на входные события при обратной связи с объектом

Между двумя векторами, содержащими М атрибутов синхронных портов, Bj = ||/?;i||, В2 =

е Тм можно установить отношения ■< и такие, что

Bi г< в2 V? = 1 М < Р,1, Bi-!Ba Vj = l М &2<fti

(1) (2)

Множество векторов Тм с этими отношениями становится частично упорядоченным, причем вектор бесконечных интервалов В± = ||оо|| будет его наименьшим элементом Это делает Тм полным частично-упорядоченным множеством

Временная модель ФВ задается векторами атрибутов его синхронных портов Г = ||7;|[, Г = Цт,!!, П = ||ы,||, П = |р,||, а также функцией вычисления вектора Л по вектору Г Сформулированы требования к /"л В частности, функция должна быть непрерывна и удовлетворять требованию

Гх -< Г => П± -< ^п(Г), (3)

где Гх и Пх есть векторы бесконечных интервалов С учетом непрерывности Ра, требование означает, что если на все необходимые входы ФБ поступили инструкции, он обязан выдать результат за конечное время

На основе структуры мпожества векторов атрибутов, задаваемой отношением (1), и теоремы Кнастера-Тарского о неподвижной точке предложен способ вычисления атрибутов -у и О всех синхронных портов в сети ФБ Способ заключается в приведении временной модели сети к виду с обратной связью и вычислении неподвижной точки суперпозиции (?п функций Рр, отдельных ФБ (рис 1) Показано, что атрибуты могут быть вычислены за конечное время и что может быть найдена непрерывная функция ^Ь(с1) вычисления атриб}тов выходов сети ФБ по атрибутам внешних синхропных входов Для этого необходима только непрерывность всех

Д]

Д—тЬ

Gn I с? --J

e = 0o(d,.)

G„(e) = Oa(d,«) Fo(d) = 0D(dj!»<Gda

Рис 1 Приведение временной модели сети ФВ к виду с обратной связью

Fnt

На основе требований к функции Fn и формального определения ФБ, задано необходимое и достаточное условие, при котором сеть ФБ будет сама являться функциональным блоком (условие иерархичности сети ФБ) Для этого необходимо, в частности, чтобы в каждую цепь обратной связи был включен ФБ с нестрогой зависимостью выходов от синхронных входов в составе цепи В этом случае функция Fa сети ФВ будет удовлетворять требованию (3), что означает невозмолшость самопроизвольного останова вычислений Это свойство подразумевает невозможность ситуаций бтокировок (deadlock) и зависаний (hvelock) в процессе работы системы, то есть ее живучесть Выполнение требования (3) может рассматриваться при анализе сети

ФБ как формальное условие ее живучести

Понятие нестрогой зависимости выходов ФБ от синхронных входов, а также обоснование иерархичности сетей с обратной связью обеспечивает существование в рамках ДО MB функциональных блоков, которые в ответ на одну инструкцию генерируют несколько (или бесконечное число) событий на выходе, то есть ФБ-источников сигналов Произвольный вид функции Fn (с учетом сформулированных требований) допускает отсутствие у ФБ выходов, то есть обеспечивает существование ФБ-приемников сигналов

Сформулированы понятия временного масштаба модели и связи ФБ по управляющим потокам

О — тах(1/ mm jp, 1/ттйр), (4)

¡fe = £ 1/£р, (5)

где Р,„ я Р„ есть множества синхронных входных и выходных портов всех ФБ, P0i и Р„2 есть множества выходов двух ФБ, через которые они взаимодействуют друг с другом Интегральный показатель v характеризует скорость выполнения вычислений и может быть использовал при оценке требуемой производительности платформы для реализации модели Оценка связи двух ФБ йЕ подразумевает интенсивность управляющих потоков и может быть использована при решении задачи системной декомпозиции, особенно при проектировании распределенных ВсС На основе показателей и г/£ сформулированы частные критерии качества модели критерий минимизации временного масштаба nunт<кы йт и критерий минимизации связей ФБ

Nm N„

i=l J=H 1

где Ai есть множество моделей, реализующих одни и те же требования к системе, a Nm есть число ФБ в модели т

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

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

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

Понятие абстрактной семантики модели в рамках комплекса позволило выделить схожие модели вычислений и, изолировав общие элементы, найти основу для их сопряжения при гетерогенном моделировании (механизм передачи сигналов, активизации вычислений, понятие состояния и тд) Абстрактная семантика представляет собой некоторый уровень, на котором возможно выделение общих для нескольких моделей вычислений правил взаимодействия компонент вычислительного процесса В главе описаны 3 типа абстрактной семантики моделей вычислений, поддерхшваемых Ptolemy II Показано, что ДОМВ имеет активационную семантику Это позволило сформулировать особенности использования моделей ДОМВ в качестве отдельных элементов на более высоком уровне абстракции и особенности использования гетерогенных моделей в рамках ДОМВ На основе понятия абстрактной семантики были сформулированы требования к функционально полиморфным компонентам моделей в Ptolemy II для их использования в рамках ДОМВ

Приведены примеры иерархического объединения ДОМВ с моделями в рамках СПД, ДС, CP и модели с непрерывным временем (НВ) Показало, что использование модели ДОМВ в качестве компонента в моделях СПД, ДС и НВ не нарушает их семантик (однако для СПД и НВ требует дополнительных механизмов сопряжения) Напротив, такое использование невозможно в CP, так как CP предполагает мгновенные вычисления Также показано, что использование моделей СПД, ДС, НВ или CP в качестве функциональных блоков ДОМВ не нарушает их семантик

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

Предложенные во второй главе методы анализа модели в рамках ДОМВ реализованы в разработанном прототипе САПР Методика анализа включает этапы вычисления атрибутов всех синхронных портов сети ФБ (см алгоритм 1), проверки соблюдения времени отклика, проверки условий иерархичности и живучести и оценки интегральных показателей качества модели (временного масштаба й и матрицы связей ФБ {vs,}}) Основные этапы методики показаны на рис 2

Разработан алгоритм вычисления атрибутов портов сети ФБ на основе предложешкл о во второй главе метода Для вычисления атрибутов все синхронные входы в модели делятся на два множества внешних и внутренних, связанных соединениями При этом, действительные значения атрибутов внешних входов (вектор Г) считаются исходными данными

____Алгоритм 1 Вычисление атрибутов синхронных кортов сети ФБ_

1 Присвоить действительный значениям атрибутов внутренних входов бесконечность

2 Для каждого ФБ с индексом г выполнить связанную с ним функцию Кп,

3 Присвоить действительным значениям атрибутов внутренних входов значения атрибутов связанных с ними выходов и выполнить шаг 2, после чего перейта на шаг 4

4 Если значения атрибутов выходов изменились, то выполнить шаг 3

Если все функции Fnx непрерывны, алгоритм 1 завершается за конечное число шагов (на практике, не более двух проходов шага 2) Непрерывность всех функций Fn> не может быть гарантирована, поскольку для атомарных (неделимых) ФБ Fn> может быть задана пользователем вручную (на языке математически выражений Ptolemy II) Поэтому на число итераций алгоритма установлено ограничение Требование непрерывности функции Fq, атомарного ФВ (как и другие требования семантики ДОМВ) контролируется пользователем

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

Оценка эффективности алгоритма 1 производилась по объему требуемых вычислительных ресурсов (объем памяти/время вычисления), по сравнению с алгоритмом вычисления атрибутов выходов в рамках ОСМВ На наборе моделей с различными типами топологии показано, что алгоритм 1 требует объем памяти в 2" - 1 раз меньший, чем алгоритм ОСМВ, где I есть число уровней иерархии тестовой модели При этом, в ходе экспериментов время вычислепия отличалось незначительно

Л, (П

Рис 2 Схема анализа характеристик модели в рамках ДОМВ

Для проверки соблюдения времени отклика сформулировано условие

Пк ;< ГиЬ (7)

где Пк есть расширенный вектор действительных значений атрибутов выходов, вычисленный на к-й итерации алгоритма 1, а Гт4 есть расширенный вектор атрибутов т внутренних входов Условие означает, что на все синхронные входы в модели поступают инструкции с минимальными интервалами, не нарушающими время отклика соответствующих ФБ

В ранках ДОМВ, для вектора Г атрибутов внешних синхронных входов модели должпо выполняться Гх -< Г, где Г^ есть вектор бесконечных интервалов С помощью алгоритма 1

проверяется условие живучести вычислительного процесса, с учетом (3)

П± -С Дг(Г) (8)

Вели условие (8) не выполняется, то элементы полученного после выполнения алгоритма 1 вектора атрибутов будут указывать на паличие блокировки (deadlock) или зависания (hvelock) в модели В случае блокировки, атрибуты блокированной цепи обратной связи будут равны бесконечности, а в случае зависания, по неблокированным цепям обратной связи можно найти ФБ, блокирующие остальную часть модели Выполнение условия (8) также означает, что модель может быть прсдставлепа одним функциональным блоком, то есть ее иерархичность

На основе действительных значений атрибутов синхронных портов вычисляются интегральные показатели временной масштаб модели й и матрица связей ФВ {Рец}

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

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

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

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

Рис 3 Методика высокоуровневого проектирования в рамках ДОМВ

ках другой модели вычислений Атрибуты синхронных входов ФБ представляют собой время выполнения в наихудшем случае (WCET) соответствующих входам алгоритмов обработки событий Это время задается разработчиком на основе экспертной оценки, а затем уточняется с помощью разработанного инструмента анализа шшшруемости обработчиков, с учетом характеристик конкретной аппаратуры WCET сервисов ОС "Терра" документированы и учитываются в высокоуровневой модели Отлаженная модель с уточненными временными характеристиками может быть транслирована в исходный код на языке С, при этом ее управляющий аспект (передача данных и активизация вычислений) транслируются автоматически с помощью разработанного инструмента Информационный аспект модели (алгоритмы преобразования данных) кодируется разработчиком вручную

Разработаны средства поддержки семантики ДОМВ в ОС "Терра" на основе механизма сигналов и планировщика (рис 4) Механизм сигналов реализует передачу данных между сипхрон-ными портами задач и операционной системы, координируя моменты взаимодействия компонентов вычислительного процесса (ФБ в поведенческой модели) Планировщик задач обеспечи-

j I Прикладные дадачи(ФС> ^ |

t | Механизм енпшюв |——ппатароицик 1

-pid......}—.—.............-

[ Сметшим» 8и6ди1тг»и>1 (С Rurttm« Library rtlogj {

( Подсистема ввода-яьяада (драйверы} (

-— Г ~1-

I BSP I

г _,

Подамстема ввода-аьдода ¿драйверы) |

Рис 4 Структура ОС 'Терра", включающая уровень поддержки ДОМВ

вает передачу управления обработчикам событий на синхронных входах ФБ по принципу EDF (Earliest Deadline First) Атрибуты выходов используются механизмом сигналов для коптроля

Ii»

моментов передачи данных и выполнения требований реального времени

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

В главе приводятся количественные оценки эффективности предложенной методики для ряда проектов на основе платформы "Терра" по стоимости, срокам и трудоемкости разработки, результатам тестирования, проценту повторного использования кода Приведены оценки для МВРЛ "Аврора", станции зависимого наблюдения АЗН-В "ОНИКС-М" и БСПС "Акробат-Ш"

ОСНОВНЫЕ РЕЗУЛЬТАТЫ

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

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

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

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

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

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

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

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

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

СПИСОК ПУБЛИКАЦИЙ ПО ТЕМЕ ДИССЕРТАЦИИ

1 Лукичев А Н , Ключев А О Организация тестового программного обеспечения встроенных систем // Научно-техничесхии вестник СПбГИТМО (ТУ) Выпуск 6 Информационные, вычислительные и управляющие системы - СПб СПбГИТМО(ТУ), 2002 с 95-99

2 Лукичев А Н Расширение возможностей лабораторного комплекса SDK-11 // Научно-гехнический вестник СПбГИТМО (ТУ) Выпуск 10 Информация и управление в технических системах - СПб СПбГИТМО(ТУ), 2003 с 86-90

3 Ковязин Р Р, Лукичев А Н , Платунов А Е , Постпиков Н П Архитектурное проектирование информациовно-унрачляющих систем // Высокие технологии, фундаментальные и прикладные исследования, образование Сборник трудов Третьей международной научно-практической конферешцм «Исследование, разработка и применение высоких технологий в промышленности» - СПб изд-во Политех уп-та, 2007 Том 9, с 52-53

4 Лукичев А Н Паттерны в проектировании встроенных систем // Высокие технологии, фундаментальные и прикладные исследования, образование Сборник трудов Третьей мех<дупародной научно-практической конференции «Исследование, разработка и применение высоких технологий в промышленности» - СПб изд-во Почитех ун-та, 2007 Том 9, с 77-78

5 Лукичев А Н Вычислительные механизмы как инструмент проектирования встроенных систем // Научно-технический вестник СПбГУ ИТМО Выпуск 45 - СПб СПбГУ ИТМО, 2007, с 58-64

6 Лукичев А Н Паттерны проектирования встроенных систем // Научно-технический вестник СПбГУ ИТМО Выпуск 39 Труды молодых ученых СПб СПбГУ ИТМО, 2007, с 114121

7 Лукичев А Н Временные характеристики функциональных блоков при дискретно-событийном моделировании встроенных систем // Сборник докладов ИММОД-2007, том 1 -СПб ФГУП ЦНИИ технологии судостроения, 2007, ISBN 978-5-98361-04S-4 с 172-176

Тиражирование и брошюровка выполнены в учреждешш «Университетские телекоммуникации» 197101, Санкт-Петербург, Саблинская ул , 14 Тел (812) 233 4669 объем 1 п л Тчраж 100 зкз

ВВЕДЕНИЕ

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

1 Модели вычислений встроенных систем

1.1 Введение.

1.2 Современные тенденции в проектировании ВсС.

1.2.1 Ключевые особенности встроенных систем.

1.2.2 Методика Hardware-Software Co-Design.

1.2.3 Акторное проектирование

1.2.4 Аспектный взгляд на процесс проектирования.

1.3 Модели вычислений встроенных систем

1.3.1 Сети потоков данных.

1.3.2 Модель с дискретными событиями.

1.3.3 Синхронно-реактивные системы.

1.4 Модель сигналов с тэгами

1.5 Объектно-событийная модель вычислений.

1.6 Постановка задачи.

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

2.1 Введение.

2.2 Денотативное описание.

2.2.1 Сигналы

2.2.2 Функциональные блоки.

2.2.3 Композиции функциональных блоков.

2.3 Временные характеристики моделей

2.3.1 Вычисление атрибутов ФБ с матрицей Т.

2.3.2 Вычисление атрибутов синхронных портов сети ФБ.

2.3.3 Условие иерархичности.

2.3.4 Временной масштаб.

2.3.5 Связь функциональных блоков

2.4 Источники и приемники сигналов.

2.4.1 Приемники сигналов

2.4.2 Источники сигналов.

2.5 Свойства вычислительного процесса

2.5.1 Детерминизм и строгая каузальность.

2.5.2 Иерархичность и композициональность.

2.5.3 Статический анализ временных характеристик.

2.5.4 Живучесть.

2.5.5 Отсутствие зеноновых поведений.

2.6 Выводы.

3 Прототип САПР системного уровня

3.1 Введение

3.2 Построение гетерогенных моделей.

3.2.1 Абстрактный синтаксис.

3.2.2 Абстрактная семантика.

3.2.3 Функциональный полиморфизм.

3.2.4 ДОМВ в другой модели вычислений.

3.3 Имитационное моделирование.

3.3.1 Пакет ptolemy.domains.oe.kernel.

3.3.2 Инициализация

3.3.3 Имитационное моделирование.

3.4 Анализ и верификация модели.

3.4.1 Методика анализа.

3.4.2 Вычисление атрибутов синхроииых портов.

3.4.3 Иерархичность и живучесть модели.

3.4.4 Корректность и качество модели

3.5 Выводы.

4 Применение ДОМВ при проектировании встроенных систем

4.1 Введение.

4.2 СКУ МВРЛ "Аврора".

4.2.1 Подсистема контроля и управления.

4.2.2 Контроллер команд и сигналов.

4.2.3 Реализация ККС.

4.3 Прикладное программирование на платформе "Терра".

4.3.1 Программно-аппаратная платформа "Терра".

4.3.2 Поддержка прикладного программирования.

4.3.3 Характеристика механизма сигналов.

4.3.4 Высокоуровневое программирование.

4.4 Выводы.

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

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

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

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

В наибольшей степени указанным требованиям отвечают модель сигналов с тэгами (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 НИР и НИОКР. Наиболее показательными из них следует считать: система контроля и управления моноимпульсного вторичного радиолокатора "Аврора" и программно-аппаратная платформа прикладных вычислителей встроенных систем "Терра". Результаты работы использованы в учебных курсах кафедры Вычислительной техники СПбГУ ИТМО в рамках инженерной и магистерской подготовки по специализациям "Информационно-управляющие системы" (230101.65.12) и "Системы реального времени" (230100.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. Время выполнения в наихудшем случае. Пессимистичная оценка времени выполнения алгоритма или задачи реального времени (без учета влияния других компонентов вычислительного процесса).

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

Заключение

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

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

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

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

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

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

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

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

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

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

1. А.Е. Платунов. Архитектурные абстракции в технологии сквозного проектирования встроенных вычислительных систем. Научно-технический вестник СПб-ГУ ИТМО(ТУ), 6:76-82, 2003.

2. Edward A. Lee. Absolutely positively on time: What would it take? Computer, 38(7):85-87, July 2005.

3. Н.П. Постников. Поведенческий и инструментальный аспекты проектирования встроенных вычислительных систем, дисс. канд. техн. паук, СПбГИТМО (ТУ), Санкт-Петербург, апрель 2004.

4. Edward A. Lee, Stephen Neuendorffer, and Michael J. Wirthlin. Actor-oriented design of embedded hardware and software systems. Journal of Circuits, Systems, and Computers, 12(3):231-260, June 2003.

5. Gérard Berry. The foundations of esterel. In Gordon Plotkin, Colin Stirling, and Mads Tofte, editors, Proof, Language, and Interaction: Essays in Honour of Robin Milner, pages 425-454. MIT Press, 2000.

6. Edward A. Lee. Cyber-physical systems are computing foundations adequate? In NSF Workshop On Cyber-Physical Systems: Research Motivation, Techniques and Roadmap, October 2006.

7. Н.Н. Непейвода and И.Н. Скопин. Основания программирования. Институт компьютерных исследований, Ижевск-Москва, 2003.

8. Эдвард А. Ли. Проблемы с потоками. Перевод с англ. Петрова А.В. Technical Report UCB/EECS-2006-1, UC Berkeley, январь 2006.

9. Nickolai Zeldovich, Alexander Yip, Frank Dabek, Robert Morris, David Mazifcres, and Frans Kaashoek. Multiprocessor support for event-driven programs. In Proceedings of the 2003 USENIX Annual Technical Conference (USENIX '03), June 2003.

10. Herb Sutter and James Larus. Software and the concurrency revolution. Queue, 3(7), September 2005.

11. A.E. Платунов and Н.П. Постников. Единое проектное пространство плюс ас-пектная технология перспективная парадигма проектирования встраиваемых систем. Научно-технический вестник СПбГУ ИТМО, 11:121-128, 2003.

12. Edward A. Lee and Alberto Sangiovanni-Yincentelli. A denotational framework for comparing models of computation. IEEE Transactions on CAD, 17(12):1217-1229, December 1998.

13. Deepak Mathaikutty, Hiren Patel, Sandeep Shukla, and Axel Jantsch. Ewd: A metamodeling driven customizable multi-moc system modeling framework. In ACM Transactions on Design Automation of Electronic Systems, volume 12. ACM, August 2007.

14. International Electrotechnical Commission. Function Blocks for Industrial Process Measurement and Control Systems, 2000.

15. Brijesh Sirpatil, James M. Jr. Baker, and James R. Armstrong. Using systemc to implement embedded software. In International HDL Conference and Exhibition (HDLCon 2002), March 2002.

16. A.H. Лукичев. Паттерны проектирования встроенных систем. Научно-технический вестник СПбГУ ИТМО, 39:114-121, 2007.

17. Rolf Ernst and Jorg Henkel. A hardware/software partitioner using a dynamically determined granularity. In Proceedings of the 34th Conference on Design Automation, page 691, 1997.

18. Giovanni de Michelli and Rajesh К. Gupta. Hardware/software co-design. In Proceedings of the IEEE, volume 85, pages 349-365, March 1997.

19. Axel Jantsch, Peeter Ellervee, Johnny Oberg, Ahmed Hemani, and Hannu Tenhunen. A software oriented approach to hardware/software codesign. In International Conference on Compiler Construction, pages 93-102, 1994.

20. Peter Voigt Knudsen and Jan Madsen. Pace: A dynamic programming algorithm for hard ware/software partitioning. In Proceedings of the 4th International Workshop on Hardware/Software Co-Design, page 85, 1996.

21. Alberto Sangiovanni-Vincentelli. Defining platform-based design. EEDesign of EETimes, February 2002.

22. Дж. Дэбии and Т. Харман. Simulink Jh. Секреты мастерства. Бином. Лаборатория знаний, 2003.

23. Paul Caspi, Adrian Curie, Aude Maignan, Christos Sofronis, Stavros Tripakis, and Peter Niebert. From simulink to scade/lustre to tta: a layered approach for distributed embedded applications. In Proceedings of LCTES'03, June 2003.

24. Esterel Technologies. Esterel Studio 6.0 Technical Datasheet, December 2007.

25. Carl Hewitt, Peter Bishop, and Richard Steiger. A universal modular actor formalism for artificial intelligence. In IJCAI, pages 235-245, 1973.

26. William D. Clinger. Foundations of actor semantics. Technical Report AITR-633, MIT, May 1981.

27. Gul A. Agha, Ian A. Mason, Scott F. Smith, and Carolyn L. Talcott. A foundation for actor computation. Journal of Functional Programming, 7(1):1—72, 1998.

28. Gul A. Agha and Prasanna Thati. An algebraic theory of actors and its application to a simple object-based language. In From Object-Orientation to Formal Methods, volume 2635/2004, pages 26-57. Springer Berlin / Heidelberg, March 2004.

29. Alberto Sangiovanni-Vincentelli, Luciano Lavagno, and Ellen Sentovich. Models of computation for embedded system design. In System-level Synthesis, pages 45-102. Kluwer Academic Publishers, 1999.

30. Gérard Berry. The Constructive Semantics of Pure Esterel. INRIA, 2002.

31. Stephen A. Edwards. The Specification and Execution of Heterogeneous Synchronous Reactive Systems. PhD thesis, EECS Department, University of California, Berkeley, 1997.

32. Thomas A. Henzinger, Christoph М. Kirsch, Marco A.A. Sanvido, and Wolfgang Pree. From control models to real-time code using giotto. IEEE Control Systems Magazine, 23(l):50-64, February 2003.

33. Stephen Edwards and Edward A. Lee. The case for the precision timed (pret) machine. Technical Report UCB/EECS-2006-149, EECS Department University of California, Berkeley, November 2006.

34. А.Н. Лукичев. Вычислительные механизмы как инструмент проектирования встроенных систем. Научно-технический вестник СПбГУ ИТМО, 45:58-64, 2007.

35. А.Е. Платунов. Роль вычислительных моделей и механизмов в проектировании встроенных систем. Научно-технический вестник СПбГУ ИТМО, 14:164-169, 2004.

36. Gilles Kahn and David В. MacQueen. Coroutines and networks of parallel processes. In B. Gilchrist, editor, Proceedings of the IFIP Congress 77, pages 993-998. North-Holland Publishing Company, 1977.

37. Edward A. Lee and David G. Messerschmitt. Static scheduling of synchronous data flow programs for digital signal processing. IEEE Transactions on Computers, 36(l):24-35, 1987.

38. J. Kodosky, J. MacCrisken, and G. Rymar. Visual programming using structured data flow. In Proceedings of the IEEE Workshop on Visual Languages, pages 34-39,1991.

39. G.R. Gao, R. Govindarajan, and P. Panangaden. Well-behaved dataflow programs for DSP computation. In Proceedings of the ICASSP-92, volume 5, pages 561-564,1992.

40. Joseph T. Buck and Edward A. Lee. Scheduling dynamic dataflow graphs with bounded memory using the token flow model. In Proceedings of IEEE International Conference on Acoustics, Speech, and Signal Processing, volume 1, pages 429-432, 1993.

41. Edward A. Lee. Multidimensional streams rooted in dataflow. In Proceedings of the IFIP Working Conference on Architectures and Compilation Techniques for Fine and Medium Grain Parallelism. North-Holland, 1993.

42. Joseph T. Buck. Static scheduling and code generation from dynamic dataflow graphs with integer-valued control systems. In Proceedings of IEEE Asilomar Conference on Signals, Systems and Computers, 1994.

43. Alain Girault, Bilung Lee, and Edward A. Lee. Hierarchical finite state machines with multiple concurrency models. IEEE Transactions On Computer-aided Design Of Integrated Circuits And Systems, 18(6), June 1999.

44. Don Mills and Clifford Cummings. Rtl coding styles that yield simulation and synthesis mismatch. In SNUG'99, 1999.

45. Ye Zhou and Edward A. Lee. Causality interfaces for actor networks. Technical Report UCB/EECS-2006-148, EECS Department, UC Berkeley, Nov 2006.

46. Xiaojun Liu. Semantic foundation of the tagged signal model. Technical Report UCB/EECS-2005-31, Electrical Engineering and Computer Sciences University of California at Berkeley, December 2005.

47. Xiaojun Liu and Edward A. Lee. Cpo semantics of timed interactive actor networks. Technical Report UCB/EECS-2007-131, EECS Department, University of California, Berkeley, November 2007.

48. R. Milne and C. Strachey. A Theory of Programming Language Semantics. Chapman and Hall, London, 1976.

49. Susan Owicki and Leslie Lamport. Proving liveness properties of concurrent programs. In ACM Transactions on Programming Languages and Systems, volume 4, pages 455-495, July 1982.

50. A. Gamatie and T. Gautier. Synchronous modeling of avionics applications using the signal language. In 9th IEEE Real-Time and Embedded Technology and Applications Symposium, pages 144-151, 2003.

51. Ч. Xoap. Взаимодействующие последовательные процессы. Пер. с англ. Мир, Москва, 1989.

52. Robin Milner. Communication and Concurrency. Prentice Hall, December 1989.

53. A.H. Лукичев and A.O. Ключев. Организация тестового программного обеспечения встроенных систем. Научно-технический вестник СПб ГИТМО(ТУ), 6:95-99, 2002.

54. Accellera. Verilog-AMS Language Reference Manual, November 2004.

55. Г. Биркгоф. Теория решеток. Наука, М., 1984.

56. A.H. Лукичев. Исследование моделей вычислений встроенных систем, магистерская дисс., СПбГУ ИТМО, Санкт-Петербург, June 2005.

57. NXP Semiconductors. UM10204■ I2C-bus specification and user manual, June 2007.

58. A.H. Лукичев. Временные характеристики функциональных блоков при дискретно-событийном моделировании встроенных систем. In Сборник докладов ИММОД-2007, volume 1, pages 172-176. ФГУП ЦНИИ технологии судостроения, октябрь 2007.

59. В.A. Davey and Н.А. Priestly. Introduction to Lattices and Order. Cambridge University Press, second edition edition, 2002.

60. Edward A. Lee. The problem with threads. Computer, 39(5):33-42, May 2006.

61. Угрюмов Е.П. Цифровая схемотехника. БХВ-Петербург, СПб., 2 edition, 2007.

62. Altera Corporation. Metastability in Altera Devices, May 1999.

63. Ye Zhou. Interface Theories for Causality Analysis in Actor Networks. PhD thesis, Electrical Engineering and Computer Sciences, University of California, Berkeley, May 2007.

64. Edward A. Lee and Thomas M. Parks. Dataflow process networks. In Proceedings of the IEEE, volume 83, pages 773-801. IEEE, May 1995.

65. Edward A. Lee and Haiyang Zheng. Leveraging synchronous language principles for heterogeneous modeling and design of embedded systems. In Proceedings of EMSOFT'07. ACM, October 2007.

66. A.H. Лукичев. Расширение возможностей лабораторного комплекса SDK-1.1. Научно-технический вестник СПб ГИТМО(ТУ), 6:86-90, 2003.

67. Atmel Corporation. 8-bit AVR Microcontroller with 128K Bytes In-System Programmable Flash, August 2007.

68. Altera Corporation. MAX II Device Handbook, December 2007.

69. Freescale Semiconductor. MPC8349E PowerQUICCrM II Pro Integrated Host Processor Family Reference Manual, July 2005.

70. Altera Corporation. Nios II Processor Reference Handbook, October 2007.

71. Altera Corporation. Cyclone II Device Handbook, February 2008.

72. Altera Corporation. Stratix Device Handbook, July 2005.

73. Altera Corporation. Stratix II GX Device Handbook, October 2007.

74. IEEE. Draft Standard Physical and Environmental Layers for PCI Mezzanine Cards: PMC, April 1995.

75. PCI Special Interest Group. PCI Local Bus Specification. Production Version. Revision 2.1, June 1995.

76. The IEEE and The Open Group. IEEE Std 1003.1. The Open Group Base Specifications, 2004.

77. Thomas A. Henzinger and Christoph M. Kirsch. The embedded machine: Predictable, portable real-time code. In Proceedings of PLDI'02, June 2002.

78. Edward A. Lee and Steve Neuendorffer. MoML a modeling markup language in XML - version 4.0. Technical Report ERL/UCB MOO/12, EECS Department, UC Berkeley, 2000.

79. Telelogic AB. Telelogic Lifecycle Solutions: Change Management. Managing Change Throughout the Development Lifecycle, 2005.