close

Вход

Забыли?

вход по аккаунту

?

Методы разработки и верификации архитектурных спецификаций вычислительных комплексов на основе систем на кристалле

код для вставкиСкачать
На правах рукописи
Печенко Иван Сергеевич
Методы разработки и верификации
архитектурных спецификаций
вычислительных комплексов на основе
систем на кристалле
Специальность 05.13.15 –
Вычислительные машины, комплексы и компьютерные сети
Автореферат
диссертации на соискание учёной степени
кандидата технических наук
Москва 2018
2
Работа выполнена в Московской лаборатории
проблем САПР АО «Интел А/О».
перспективных
Научный руководитель:
Петров Андрей Борисович, доктор технических
наук,
профессор,
заведующий
кафедрой
корпоративных
информационных
систем
Института
информационных
технологий
Московского технологического университета
(МИРЭА)
Официальные
Бычков Игнат Николаевич, доктор технических
наук, заместитель Генерального директора
ПАО «ИНЭУМ им. И.С. Брука»
оппоненты:
Петров Константин Александрович, кандидат
технических наук, старший научный сотрудник
ФГУ ФНЦ НИИСИ РАН
Ведущая организация:
Акционерное
общество
«Научноисследовательский институт «Аргон»»
Защита состоится «21» июня 2018 г. в 16 час. 30 мин. на заседании
диссертационного совета Д 212.131.05 при федеральном государственном
бюджетном
образовательном
учреждении
высшего
образования
«Московский технологический университет» (МИРЭА), расположенном по
адресу: 119454, г. Москва, проспект Вернадского, дом 78, ауд. Д-117.
С диссертацией можно ознакомиться в библиотеке МИРЭА и на сайте
http://www.mirea.ru. Автореферат разослан 19 мая 2018 г.
Отзывы на автореферат в двух экземплярах, заверенные печатью,
просьба направлять по адресу: 119454, г. Москва, проспект Вернадского,
д.78, МИРЭА, диссертационный совет Д212.131.05.
Ученый секретарь
к.т.н., доцент
Андрианова Елена Гельевна
3
ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ
Актуальность работы
Благодаря
современным
полупроводниковым
технологиям
стало
возможным размещать всю вычислительную систему или, по крайней мере,
большую её часть на едином кристалле. Преимущества такого подхода
неоспоримы: значительно увеличивается производительность системы за
счёт меньшей длины соединений между компонентами, а также уменьшается
энергопотребление. Эти преимущества имеют решающее значение при
создании мобильных вычислительных систем, где такой подход уже завоевал
огромную
популярность.
На
сегодняшний
день
подобные
системы,
называемые системами на кристалле (СнК), лежат в основе множества
разнообразных вычислительных комплексов, решающих широкий круг задач.
Однако чрезвычайная сложность подобных систем ведёт к тому, что
традиционные методы разработки аппаратно-программных комплексов не
подходят для их создания. Несмотря на то, что в последние два десятилетия
были предложены новые процессы разработки, решающие основные
проблемы создания систем на кристалле, в них до сих пор остаётся
множество узких мест. Примером таких узких мест является верификация
архитектуры систем, которая может позволить исключить ошибки в
спецификациях. Стоит отметить, что такие ошибки, обнаруженные на
поздних циклах разработки, могут означать серьёзные проблемы для всего
проекта. По этим причинам необходимо дальнейшее развитие процесса
разработки систем на кристалле, которое позволит устранить описанные
сложности.
Наиболее перспективными с точки зрения такого развития являются
ранние стадии разработки СнК: создание спецификации системы, разработка
исполняемых моделей её архитектуры и ранняя верификация этих моделей. В
рамках современных процессов разработки переход от спецификации СнК к
исполняемым моделям архитектуры системы в большинстве случаев
4
выполняется вручную: команды разработчиков исполняемых моделей
получают спецификацию системы и на её основе пишут код на языках
высокоуровневого моделирования. Однако такой подход, во-первых, требует
много времени, а во-вторых, чреват появлением ошибок, а также
несоответствий между спецификациями и архитектурными моделями.
Противоположный подход - создание спецификаций на формальных языках также имеет несколько серьёзных недостатков, главными из которых
является сложность создания и плохая читабельность готовой спецификации.
Поэтому необходим новый подход к созданию спецификаций системы,
решающий проблему перехода от спецификаций к высокоуровневым
моделям. Основной темой диссертационной работы является разработка
такого подхода.
Область исследования определена предметной областью паспорта
специальности 05.13.15 п.6 «Разработка научных методов, алгоритмов и
программ,
обеспечивающих
надежность,
контроль
и
диагностику
функционирования вычислительных машин, комплексов и компьютерных
сетей» и включает в себя, в частности, разработку методов, обеспечивающих
надёжность и корректность функционирования вычислительных комплексов.
Объектом исследования являются методы обеспечения корректности
функционирования вычислительных комплексов на основе систем на
кристалле.
Предметом исследования является методы обеспечения корректности
архитектурных спецификаций вычислительных комплексов на основе систем
на кристалле.
Целью работы является разработка набора методов создания и
верификации архитектурных спецификаций систем на кристалле в основе
вычислительных комплексов.
Для достижения поставленной цели требуется решить следующие
задачи:
5
1. Провести анализ ранних стадий процесса разработки систем на
кристалле для определения основных имеющихся недостатков в этом
процессе.
2. Провести
сравнение
различных
форматов
архитектурных
спецификаций вычислительных систем и выбрать из них наилучшие по
соотношению
эффективности
процесса
создания
и
возможностей
автоматизации.
3. Разработать подход к созданию и использованию архитектурных
спецификаций систем на кристалле.
4. Разработать
способы
представления
данных
для
создания
архитектурных спецификаций систем на кристалле, а также методы и
алгоритмы работы с ними.
5. В
качестве
примера
программные средства
реализации
для создания
этих
и
методов
разработать
управления архитектурными
спецификациями вычислительных комплексов.
Методы
исследования
включают
в
себя
приложения
теории
формальных языков, теории трансляции, а также различные методы
программной инженерии.
Основные положения, выносимые на защиту:
1. Оригинальный подход к созданию и использованию архитектурных
спецификаций вычислительных систем типа «система на кристалле».
2. Методы, алгоритмы и способы представления данных для работы с
поведенческими (функциональными) спецификациями систем на кристалле.
3. Методы, алгоритмы и способы представления данных для работы со
структурными (нефункциональными) спецификациями систем на кристалле.
4. Программные средства, реализующие предложенные методы.
Научная новизна работы состоит в:
1. Разработке подхода к созданию спецификаций систем на кристалле и
их верификации, отличного от существующих и имеющего перед ними ряд
преимуществ.
6
2. Разработке метода трансляции текстовых описаний протоколов
функционирования систем на кристалле в диаграммы деятельности.
3. Разработке алгоритма верификации протоколов функционирования
систем на кристалле, представленных в виде диаграмм.
4. Разработке подхода к верификации структурных спецификаций
систем на кристалле, представленных в табличном формате.
Практическая значимость работы состоит в том, что применение
программных средств, построенных на основе предложенного набора
методов,
ведёт
к
повышению
качества
созданных
архитектурных
спецификаций вычислительных систем, а также позволяет намного раньше
начинать процесс верификации системы.
Достоверность результатов диссертационной работы подтверждается
положительным
опытом
использования
предложенного
подхода
при
экспериментальной и промышленной эксплуатации построенного на её
основе программного обеспечения.
Апробация работы. Материалы диссертации докладывались на
конференциях:
-
Всероссийской
научно-технической
конференции
«Проблемы
разработки перспективных микро- и наноэлектронных систем» МЭС-2016, 37 октября 2016, г. Зеленоград;
-
XVI
научно-практической
конференции
«Современные
информационные технологии в управлении и образовании», 20 апреля 2017,
г. Москва.
- X международной научно-практической конференции «Научный
форум: технические и физико-математические науки», 18 декабря 2017, г.
Москва.
Публикация. Основные результаты исследований опубликованы в 5
научных статьях в изданиях, рекомендованных ВАК.
Личный вклад. Все исследования, представленные в диссертационной
работе,
выполнены
автором
либо
самостоятельно,
либо
при
его
7
непосредственном
участии.
Поход
к
созданию
и
использованию
архитектурных спецификаций систем на кристалле представляет собой
усовершенствованную версию существующих подходов и предложен лично
автором. Программные реализации предложенных методов, описанные в
главе 4, разработаны автором совместно с сотрудниками исследовательских
лабораторий корпорации Intel и концерна «Вега». В опубликованных в
соавторстве работах личный вклад автора сводится к следующему: в работах
[2, 4] автором предложены алгоритмы трансляции из структурированного
текста в диаграммы, а также импорта и экспорта табличных данных и
поддержки соответствия таблиц и их шаблонов, в работе [3] автором
предложены модели данных и схема подхода.
Структура и объём работы: диссертация состоит из введения,
четырёх глав, заключения, библиографического списка и приложения. Работа
содержит 140 страниц основного текста, включая 26 рисунков и 3 таблицы, а
также библиографический список из 100 наименований.
Содержание работы:
Во введении приведено обоснование актуальности темы работы,
сформулированы цели и задачи, а также описаны основные результаты
работы, выделена их теоретическая и практическая значимость.
В первой главе приведён обзор процессов разработки вычислительных
систем: традиционного и современного, обозначены узкие места в
современном процессе разработки и поставлена задача по улучшению этого
процесса. Традиционный процесс разработки основывался на каскадной
модели, когда проект проходил по очереди несколько основных стадий:
стадию планирования, стадию разработки спецификации архитектуры,
разработки микроархитектуры, описания системы на уровне регистровых
передач (RTL), верификации системы, а также стадию логического и
физического синтеза. Со временем, при усложнении разрабатываемых
вычислительных систем, обострение проблемы верификации системы в
традиционном процессе её разработки привело к массовому переходу на
8
новую модель такого процесса. В отличие от традиционного подхода, в
современной модели верификация системы должна начинаться сразу после
создания архитектурной спецификации и проводиться непрерывно в течение
разработки системы, как показано на рис. 1.
Создание архитектурной спецификации проекта
Создание
структурных
спецификаций
Создание
поведенческих
спецификаций
Создание исполняемых моделей системы
Верификация архитектуры системы
Проектирование
аппаратных
блоков
Проектирование
программных
блоков
Физическое
проектирование
Рис.1. Современный процесс разработки СнК.
Применение такого процесса позволяет решать задачу разработки СнК
гораздо эффективнее, чем она решается с помощью классического подхода.
Тем не менее, и современный подход не лишён недостатков:
- процесс создания и верификации исполняемых моделей архитектуры
СнК настолько сложен, что приходится начинать разработку компонентов
системы до завершения этого процесса, что зачастую становится причиной
9
ошибок в архитектуре системы, которые выявляются только на поздних
этапах разработки;
-
невозможно
проводить
совместный
анализ
аппаратных
и
программных компонентов системы на ранних этапах её разработки.
Источником этих недостатков является низкое качество архитектурных
спецификаций и сложность создания высокоуровневых моделей системы на
их основе.
Для исправления этих недостатков необходимо разработать новый
набор методов для перехода от архитектурных спецификаций систем к
высокоуровневым моделям.
Так как процесс создания спецификаций зависит от формата
представления данных в них, в качестве первого шага разработки методов
необходимо провести сравнительный анализ различных форматов данных,
используемых в процессе создания спецификаций вычислительных систем, и
существующих методов автоматизации их использования. В результате этого
анализа необходимо выбрать один или несколько форматов, наиболее
подходящие для создания спецификаций систем на кристалле. После этого
необходимо определить общий вид нового подхода, учитывая требования,
основанные на целях, поставленных перед ним. Он должна позволять:
- повысить качество создаваемых спецификаций без существенных
дополнительных усилий архитекторов и без необходимости использовать для
создания спецификаций формальные языки;
-
поддерживать
процесс
переиспользования
существующих
спецификаций СнК;
- поддерживать процесс генерации формальных моделей или их частей
из данных спецификации.
В качестве третьего шага необходимо разработать модели данных для
спецификаций СнК на основе выбранных форматов, а также подробно
рассмотреть методы создания и использования спецификаций в применении
к выбранным моделям данных.
10
По результатам проведенного анализа была поставлена цель и
сформулирован полный перечень задач диссертационной работы.
Вторая глава посвящена исследованию, сравнению и выбору
форматов данных, которые будут использоваться в рамках разрабатываемых
методов. На основе сформулированных целей, были выбраны следующие
критерии сравнения форматов:
1) Выбранные форматы должны широко использоваться в современном
процессе создания спецификаций вычислительных систем.
2) Создание спецификаций в выбранных форматах не должно
требовать существенных усилий архитекторов и серьёзных знаний в области
формальных языков.
3) Должна существовать возможность автоматической верификации
данных в выбранных форматах.
4) Должна существовать возможность автоматической трансляции
данных из выбранных форматов на различные формальные языки,
требующая, возможно, добавления некоторой дополнительной информации к
спецификациям либо их структурирования.
5) Выбранные форматы должны хорошо подходить для спецификации
архитектуры систем на кристалле.
Исследуемые форматы были объединены в следующие группы:
1. Текст на естественном языке.
2. Формальные языки высокоуровневого моделирования, такие как
SystemC, Promela (Protocl Meta Language), Murphi.
3. Структурные диаграммы.
4. Диаграммы деятельности (UML-диаграммы деятельности и нотации
BPMN) и диаграммы взаимодействия (UML-диаграммы последовательности,
коммуникации,
временные
диаграммы
и
обзорные
диаграммы
взаимодействия, а также диаграммы последовательности сообщений).
5. Таблицы.
11
Автором было проведено исследование перечисленных форматов
данных. Для сравнения форматов по первому критерию было проведено
исследование некоторого объёма открытых спецификаций вычислительных
систем. Критерием сравнения был объём данных, представленных в каждом
формате. Для сравнения форматов по второму критерию автором было
проведено исследование для оценки сложности создания спецификаций, в
котором основным критерием сравнения форматов было выбрано время
создания спецификации. Для сравнения форматов по третьему и четвёртому
критерию
было
проведено
исследование
существующих
методов
верификации данных и автоматической трансляции данных из выбранных
форматов на различные формальные языки. Для сравнения по последнему
критерию были рассмотрены основные наборы данных, из которых состоит
большинство спецификаций СнК, и возможность представления этих данных
в различных форматах.
В результате этого исследования автором было сделано заключение,
что всем критериям удовлетворяют три группы форматов: структурные
диаграммы, диаграммы деятельности и взаимодействия, а также таблицы.
Область применения структурных диаграмм в описании архитектуры СнК,
однако, довольно узка, что ставит под сомнение эффективность построения
набора методов на их базе.
Решающим при выборе форматов является следующий критерий:
необходимо выбрать наименьший набор форматов, который обеспечит
полное или почти полное покрытие описания всех аспектов архитектуры
СнК. Важнейшими аспектами спецификации СнК являются структурный и
поведенческий, поэтому было решено выбрать по одной группе форматов
для каждого из них. На основе проведённого исследования автором было
предложено использовать таблицы для представления структурных аспектов
спецификации и диаграммы деятельности для представления поведенческих
аспектов спецификации.
12
В третьей главе предлагается оригинальный подход к созданию
архитектурных спецификаций СнК и работы с ними. Процесс работы со
спецификациями в рамках этого подхода представлен на рис. 2.
Необходимо
сразу
отметить
ограничения
на
применение
предложенного подхода. Можно выделить два основных условия, при
которых его применение будет неэффективным:
1) В случае, когда создание спецификаций ведётся сразу в виде
формальных моделей и при этом организационными методами решены
проблемы, присущие такому подходу (сложность создания спецификаций и
их плохая читабельность), применение предложенного подхода будет «шагом
назад», понижающим эффективность процесса разработки архитектуры
системы.
2) В случае, когда спецификация новой системы на кристалле по
большей части состоит из спецификаций готовых функциональных блоков,
написанных на формальных языках, либо повторяет готовые спецификации
СнК, для которых также готовы формальные модели, применение
предложенного подхода также может снижать эффективность процесса
разработки архитектуры. Экспериментальные результаты показывают, что
предложенный подход становится неэффективной, когда как минимум
имеются как минимум 75% готовой спецификации, представленной в виде
формальных моделей.
Так как спецификации можно разделить на две группы, для которых
используются разные форматы данных, было решено разделить набор
методов работы с ними на две части: одна для работы со структурными
спецификациями, другая для работы с поведенческими спецификациями.
Следующий шаг разработки подхода состоит в выборе моделей данных, а
также
в
создании
спецификаций.
различных
методов
и
алгоритмов
разработки
13
Определение состава спецификации
Создание шаблонов данных для фрагментов спецификации
Описание
классов связей
между
элементами
спецификации
Создание
инструментария
для проверки
целостности и
непротиворечивос
ти данных
Выбор алгоритмов
трансляции
данных из
спецификации на
формальные
языки
Разработка или выбор алгоритмов трансляции данных из
существующих спецификаций
Трансляция данных из существующих спецификаций
Создание различных фрагментов спецификации
Базовая проверка синтаксиса спецификаций
Создание связей между фрагментами
спецификации
Проверка целостности и непротиворечивости данных
Трансляция данных из спецификации
в формальные модели
Верификация полученных формальных моделей
Рис. 2. Процесс создания и использования спецификаций.
14
Для
поведенческих
спецификаций
модель
данных
должна
основываться на диаграммах деятельности, наиболее распространёнными из
которых являются UML-диаграммы деятельности и нотации BPMN.
Автором в работе была предложена модель данных, содержащая набор
примитивов, использующихся в этих визуальных языках, оптимальный с
точки зрения простоты представления поведенческих спецификаций СнК.
Автором в работе был предложен ряд алгоритмов, реализующих шаги
описанного подхода в применении к поведенческим спецификациям в форме
диаграмм. Так как одним из основных форматов описания алгоритмов в
существующих спецификациях является текстовый, в работе был предложен
оригинальный алгоритм трансляции текстового описания поведения системы
в диаграммы. Этот алгоритм основывается на структурировании текста путём
добавления в него специальных тэгов и последующей работе с уже
структурированным описанием алгоритма.
Для проверки корректности спецификаций в форме диаграмм автором
был предложен способ верификации формальной модели, созданной на
основе диаграммы. Для перехода от диаграммы к формальным моделям в
качестве промежуточного формата были выбраны системы состояний и
переходов. Для перевода диаграммы деятельности в такую систему
необходимо воспользоваться набором правил по переводу множества
возможных значений переменных, заданных для диаграммы, и множества
активных переходов между элементами диаграммы в набор состояний
системы. После этого необходимо определить правила перехода системы для
каждого действия в диаграмме. В качестве примера рассмотрим простейшую
диаграмму запуска IP-блока, представленную на рис. 3. Набор условий
перехода для этой диаграммы представлен в таблице 1.
Базовым форматом для представления структурных спецификаций
были
выбраны
таблицы.
Однако
таблицы
произвольного
вида
не
удовлетворяют всем критериям, определяющим подходящий формат данных.
15
Block
Driver
IP-block load
Block_activated =
true
Driver_activated == true
Driver_activated == false
Block_activated
= false
Driver_received_cont
rol = true
Рис. 3. Диаграмма запуска IP-блока.
Таблица 1. Условия перехода для диаграммы запуска работы IP-блока.
Условие перехода
Sequence1 ϵ L
Sequence2 ϵ L && Driver_activated == false
Message1 ϵ Q && Message1.Status ==
in_fabric
Message1 ϵ Q && Message1.Status ==
at_target
Message1 ϵ Q && Message1.Status ==
enabled
Действие при переходе
Block_activated = true
L.Remove(Sequence1)
L.Add(Sequence2)
Q.Add(Message1)
Message1.Status = in_fabric
L.Remove(Sequence2)
Block_activated = false
Message1.Status = at_target
Message1.Status = enabled
Q.Remove(Message1)
Driver_received_control = true
Поэтому для представления структурных спецификаций в рамках
описанного подхода был выбран процесс создания таблиц на основе заранее
определённой модели. Процесс создания таких таблиц состоит из двух
этапов: сначала создаются их шаблоны, описывающие вид таблицы, а также
ограничения на представленные в ней данные, а затем отдельные
экземпляры, соответствующие этим шаблонам. С помощью построения
16
шаблонов
с
определёнными
свойствами
такие
таблицы
возможно
реализовать по построению свободными от многих типовых для табличных
данных ошибок, например, некорректных ссылок, типов и пробелов в
записях.
Автором в работе был предложен ряд алгоритмов, реализующих шаги
описанного подхода в применении к структурным спецификациям в форме
таблиц. Трансляция данных из существующих спецификаций в табличный
формат возможна либо из другого табличного формата, либо из формальных
языков. Если для каждого формального языка необходимо разработать свой
подход для трансляции, то перевод таблицы в таблицу несложен и может
основываться, например, на механизме запросов SQL. Что касается проверки
корректности табличных данных, автором представлены требования к языку
записи логических выражений для такой проверки. Наконец, последней
составной частью процесса работы с табличными спецификациями является
трансляция её на различные формальные языки. Алгоритмы трансляции
необходимо разрабатывать отдельно для каждого шаблона таблиц и для
каждого целевого языка. В качестве примера в работе предложен алгоритм
трансляции таблицы битовых полей регистров на язык описания регистров
SystemRDL.
В
четвёртой
главе
предложены
программные
реализации
разработанного набора методов и алгоритмов.
Первая из этих реализаций, программная система ACES (Analyzable,
Consistent, Efficient Specification) была создана автором и его коллегами в
корпорации Intel. Так как де-факто промышленным стандартом для создания
спецификаций вычислительных систем является среда Microsoft Office,
именно эта среда выбрана в качестве рабочего интерфейса компонентов
системы ACES; дополнительные же возможности системы скрыты за
интерфейсом Microsoft Office. Такая структура системы позволяет решать
задачи создания и использования архитектурных спецификаций, не требуя
17
дополнительных усилий архитекторов, так как с их стороны процесс
создания спецификаций остаётся практически неизменным.
Основными компонентами системы ACES является модуль работы с
поведенческими спецификациями в форме диаграмм IFlow и модуль работы
со структурными спецификациями в форме таблиц ACES Tables.
Основой модуля работы с поведенческими спецификациями является
визуальный язык IFlow, основанный на предложенных в главе 3 диаграммах
деятельности. Важнейшими функциями, реализованными в модуле работы с
поведенческими спецификациями, являются:
1. Полуавтоматическая трансляция текстовых описаний сценариев
поведения системы в диаграммы с использованием специальных тэгов.
2. Трансляция диаграмм в формальные модели системы с помощью
систем
состояний
и
переходов
и
последующая
верификация
этих
формальных моделей.
В модуле работы со структурными спецификациями в качестве модели
данных
используются
таблицы,
построенные
на
основе
заранее
определённых шаблонов. В программной реализации такие шаблоны
определяются с использованием языка XML. На рис. 4 представлен пример
таблицы регистров, созданной с использованием шаблонов.
Важнейшими возможностями, реализованными в модуле работы со
структурными спецификациями, являются:
1. Различные функции для импорта и экспорта данных, как в форматах,
поддерживаемых ACES, так и в других форматах. Последнее осуществляется
с помощью подключаемых к системе ACES модулей.
2. Механизм валидации табличных данных.
3. Специальные функции, разработанные для улучшения визуальной
привлекательности, удобства использования и предупреждения нарушения
целостности
таблиц,
такие
как:
добавление
регулирование доступа к полям таблицы и так далее.
и
удаление
записей,
18
4. Механизм автоматического обновления таблиц при изменениях их
шаблонов.
Table name
Register definitions
Comment
Summary of OpenSPARC T2 Privileged Registers
Register
Address
Description
00
Trap PC
01
Trap Next PC
02
Trap State
03
Trap Type
04
Tick
05
Trap Base Address
06
Process State
07
Trap Level
Register Type
TPC
TNPC
TSTATE
TT
TICK
TBA
PSTATE
TL
Access
Type
RW
RW
RW
RW
RW
RW
RW
RW
Рис. 4. Пример таблицы регистров.
Второй экспериментальной реализацией описанного набора методов
является
программный
спецификациями
комплекс
вычислительных
для
систем,
работы
со
структурными
разработанный
в
рамках
исследовательской программы концерна радиостроения «Вега». В этом
случае
целевым
продуктом
разработки
были
системы
воздушного
базирования. Для этого в рамках реализации необходимо было расширить
предложенные методы для работы со спецификациями широкого спектра
вычислительных систем. Кроме того, в рамках исследовательской программы
необходимо было применять только набор методов для структурных
спецификаций, спецификации алгоритмов её поведения составлялись
отдельно.
Для валидации табличных данных, а также для перевода данных из
готовых
спецификаций
в
формат,
поддерживаемый
описываемым
программным комплексом, а также из этого формата в различные модели
системы, был разработан ряд алгоритмов трансляции.
19
Разработанный программный комплекс был применён для создания
структурных
спецификаций
архитектуры
программно-аппаратных
комплексов наземного и воздушного базирования, решающих задачи
авиационной навигации. Результатом экспериментального использования
программного
комплекса
стало
значительное
повышение
качества
выпускаемых спецификаций, а также скорости работы с ними. К примеру,
при эксперименте по применению описанного подхода к спецификации
программно-аппаратного
комплекса
из
27
функциональных
блоков,
содержавшей в начальной версии 834 страницы текста, было выявлено 26
серьёзных ошибок и неточностей на стадии первичной валидации и ещё 12
ошибок на стадии верификации сгенерированных формальных моделей. При
этом срок от готовности спецификации до начала верификации полученных
из неё формальных моделей сократился в среднем на 30% по сравнению с
традиционным
подходом,
при
котором
используются
текстовые
спецификации.
Основные результаты диссертационной работы:
1. Выявлены основные сложности на ранних этапах современного
процесса разработки вычислительных систем типа «система на кристалле»,
заключающиеся в сложности ранней верификации архитектуры таких
систем, и предложена возможность улучшения этого процесса.
2. Выявлены форматы для создания архитектурных спецификаций
систем на кристалле, наилучшие по соотношению удобства создания и
возможностей автоматизации, в частности, диаграммы деятельности и
взаимодействия для поведенческих (функциональных) спецификаций и
таблицы для структурных (нефункциональных) спецификаций.
3. Разработан подход к созданию архитектурных спецификаций систем
на кристалле.
20
4. Разработаны наиболее подходящие для описанного подхода способы
представления данных для двух основных типов спецификаций систем на
кристалле:
поведенческих
(функциональных)
и
структурных
(нефункциональных).
5. Разработаны методы и алгоритмы проведения различных операций
над спецификациями: трансляции на формальные языки, валидации данных в
выбранных форматах, а также создания ссылок между спецификациями.
6.
Разработаны
вычислительный
программные
комплекс,
реализации
разработанный
в
предложенной:
корпорации
Intel,
и
вычислительный комплекс, разработанный в концерне «Вега».
Основные публикации по теме диссертационной работы:
1)
Печенко
И.С.
Способы
представления
спецификаций
вычислительных систем: проблемы и возможности машинной обработки //
Информационные технологии. – 2016. – Т. 22. - № 9. - С. 676-683.
2) Печенко И.С., Венгер О.В., Плоткин Д.А. ACES Tables: среда для
создания и использования табличных спецификаций систем на кристалле //
Информационные технологии. - 2017. – Т. 23. - №5. – С. 388-393.
3) Печенко И.С., Петров А.Б. Модели данных для архитектурных
спецификаций систем на кристалле // Информационные технологии. - 2017. –
Т. 23. - №7. – С. 536-542.
4) Печенко И.С., Венгер О.В. Способ автоматизированного создания
диаграмм последовательности операций для сценариев поведения системы,
описанных в виде текста // Информационные технологии. - 2015. – Т. 21. №1. – С. 50-56.
5) Печенко И.С. Спецификация и валидация протоколов систем на
кристалле: проблемы и пути их решения // Проблемы разработки
перспективных микро- и наноэлектронных систем (МЭС) – 2016. - №. 2. – С.
92-99.
1/--страниц
Пожаловаться на содержимое документа