Методы разработки и верификации архитектурных спецификаций вычислительных комплексов на основе систем на кристалле тема диссертации и автореферата по ВАК РФ 05.13.15, кандидат наук Печенко, Иван Сергеевич

• Печенко, Иван Сергеевич
• кандидат наук
• 2018

Оглавление диссертации кандидат наук Печенко, Иван Сергеевич

Оглавление

Стр.

Список сокращений и условных обозначений

Введение

Глава 1. Процесс проектирования СБИС и его проблемы

1.1. Определение базовых понятий

1.2. Традиционный процесс разработки систем на

кристалле

1.3. Современный процесс разработки систем на

кристалле

1.4. Проблемы современного процесса разработки

систем на кристалле

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

Глава 2. Анализ и выбор форматов, использующихся при

создании спецификаций

2.1. Общие подходы

2.2. Выбор форматов для анализа

2.3. Анализ форматов на основе выбранных критериев

2.3.1. Применение форматов при проектировании архитектуры вычислительных систем

2.3.2. Сложность создания спецификаций

2.3.3. Возможности верификации данных

2.3.4. Трансляция на формальные языки

2.3.5. Представление архитектуры систем на кристалле

2

2.4. Результаты анализа форматов

2.5. Выводы по главе 2

Глава 3. Разработка методов

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

систем на кристалле

3.1. Общий подход

3.2. Методы создания и использования

поведенческих спецификаций

3.3. Методы создания и использования

структурных спецификаций

3.4. Выводы по главе 3

Глава 4. Применение методов создания и использования

архитектурных спецификаций систем на кристалле

4.1. Описание реализации предложенных методов

в виде программной системы ACES

4.1.1. Реализация методов создания

и использования поведенческих спецификаций

систем на кристалле

4.1.2. Реализация методов создания

и использования структурных спецификаций

систем на кристалле

4.1.3. Инфраструктура системы ACES

4.2. Описание реализации предложенных методов в виде программной системы в концерне «Вега»

4.3. Выводы по главе 4

3

Заключение

Литература

Приложение А. Акты о внедрении результатов

диссертационной работы

Используемые сокращения

СнК - система на кристалле

СБИС - сверхбольшая интегральная схема

ПО - программное обеспечение

ВС - вычислительная система

IP-блок - блок intellectual property

RTL - register transfer level

ACES - Analyzable, Consistent, Efficient Specification

TLM - transaction-level modeling

MSC - message sequence chart

UML - Unified Modeling Language

BPMN - Business Process Model and Notation

XML - eXtensible Markup Language

SQL - Structured Query Language

RDL - Register Definition Language

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

Введение

На протяжении нескольких десятков лет лидерами рынка вычислительных элементов были микропроцессоры, бывшие сердцем любой вычислительной системы. И только недавно у них появились конкуренты, способные сместить их с лидерской позиции - системы на кристалле (СнК). Их появление стало результатом многолетнего развития средств проектирования и производства сверхбольших интегральных схем (СБИС), сделавшего, наконец, качественный скачок. Благодаря последним технологиям стало возможным размещать на едином кристалле всю вычислительную систему или, по крайней мере, большую её часть: микропроцессор, графические и сигнальные процессоры, энергозависимую память, контроллеры устройств ввода/вывода и шины, соединяющие все перечисленные компоненты. Преимущества такого подхода неоспоримы: значительно увеличивается производительность системы за счёт меньшей длины соединений между компонентами, уменьшается энергопотребление - по той же причине. Эти преимущества имеют решающее значение при создании мобильных вычислительных систем, где системы на кристалле уже завоевали огромную популярность. Благодаря использованию СнК стало возможным разместить достаточно высокопроизводительную вычислительную систему в небольшом устройстве. На сегодняшний день подобные системы лежат в основе множества разнообразных вычислительных комплексов, решающих широкий круг задач.

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

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

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

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

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

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

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

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

Область исследования определена предметной областью паспорта специальности 05.13.15 п.6 «Разработка научных методов, алгоритмов и программ, обеспечивающих надежность, контроль и диагностику функционирования вычислительных машин, комплексов и компьютерных сетей» и включает в себя, в частности, разработку методов, обеспечивающих надёжность и корректность функционирования вычислительных комплексов.

Объектом исследования являются методы обеспечения корректности функционирования вычислительных комплексов на основе систем на кристалле.

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

Целью работы является разработка набора методов создания архитектурных спецификаций систем на кристалле и их верификации.

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

1. Провести анализ ранних стадий процесса разработки систем на кристалле для определения основных имеющихся недостатков в этом процессе.

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

3. Разработать подход к созданию и использованию архитектурных спецификаций систем на кристалле.

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

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

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

Основные положения, выносимые на защиту:

1. Оригинальный подход к созданию и использованию архитектурных спецификаций вычислительных систем типа «система на кристалле».

2. Методы, алгоритмы и способы представления данных для работы с поведенческими (функциональными) спецификациями систем на кристалле.

3. Методы, алгоритмы и способы представления данных для работы со структурными (нефункциональными) спецификациями систем на кристалле.

4. Программные средства, реализующие предложенные методы.

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

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

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

3. Разработке алгоритма верификации протоколов функционирования систем на кристалле, представленных в виде диаграмм.

4. Разработке подхода к верификации структурных спецификаций систем на кристалле, представленных в табличном формате.

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

Достоверность результатов диссертационной работы подтверждается положительным опытом использования предложенного подхода при экспериментальной и промышленной эксплуатации построенного на её основе программного обеспечения.

Личный вклад. Все исследования, представленные в диссертационной работе, выполнены автором либо самостоятельно, либо при его непосредственном участии. Поход к созданию и использованию архитектурных спецификаций систем на кристалле представляет собой усовершенствованную версию существующих подходов и предложен лично автором. Программные реализации предложенных методов, описанные в главе 4, разработаны автором совместно с сотрудниками исследовательских лабораторий корпорации Intel и концерна «Вега». В опубликованных в соавторстве работах личный вклад автора сводится к следующему: в работах [2, 4] автором предложены алгоритмы трансляции из структурированного текста в диаграммы, а также импорта и экспорта табличных данных и поддержки соответствия таблиц и их шаблонов, в работе [3] автором предложены модели данных и схема подхода.

Апробация работы. Материалы диссертации докладывались на конференциях:

- Всероссийской научно-технической конференции «Проблемы разработки перспективных микро- и наноэлектронных систем» МЭС-2016, 3-7 октября 2016, г. Зеленоград;

- XVI научно-практической конференции «Современные информационные технологии в управлении и образовании», 20 апреля 2017, г. Москва.

- X международной научно-практической конференции «Научный форум: технические и физико-математические науки», 18 декабря 2017, г. Москва.

Публикация. Основные результаты исследований опубликованы в 5 научных статьях в изданиях, рекомендованных ВАК.

Структура и объём работы: диссертация состоит из введения, четырёх глав, заключения, библиографического списка и приложения. Работа содержит 140 страниц основного текста, включая 26 рисунков и 3 таблицы, а также библиографический список из 100 наименований.

Глава 1. Процесс разработки СБИС и его проблемы

1.1. Определение базовых понятий

Сложность современных систем на кристалле приводит к множеству проблем в процессе их проектирования. Несмотря на то, что традиционный процесс разработки СБИС в применении к СнК в последние десятилетия претерпел существенные изменения, компании-производители программно-аппаратных комплексов до сих пор сталкиваются с серьёзными трудностями при разработке таких систем. Особенного внимания заслуживают проблемы первых этапов проектирования СнК, связанные с разработкой спецификации, проектированием архитектурных моделей и ранней верификацией систем. Целью данной части работы является выявление таких проблем на ранних этапах проектирования СнК.

Определим для начала понятие «система на кристалле» (СнК). В литературе нет чёткого определения этого понятия, но обычно под системой на кристалле понимают вычислительную систему, на едином кристалле которой интегрированы все основные необходимые элементы, список которых обычно включает в себя [1]:

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

- Модули оперативной памяти.

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

- Контроллер прерываний.

- Контроллеры ввода и вывода информации.

Рис. 1.1. Типичная система на кристалле для мобильного сегмента.

Схема типичной системы на кристалле для мобильного сегмента, WonderMedia PRIZM WM8950 [2], представлена на рис. 1.1.

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

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

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

При определении понятия «система на кристалле» нужно отметить ещё одну важнейшую особенность СнК: принципиальную роль встроенного программного обеспечения в их конструкции. Это объясняется двумя причинами. Во-первых, функциональность современных систем слишком широка, и покрыть все функции системы аппаратной реализацией довольно сложно. Во-вторых, в связи с изменчивостью требований к системе при проектировании зачастую бывает проще использовать программируемые аппаратные блоки, которые в случае изменений в проекте перепрограммировать гораздо проще, нежели создать новую аппаратную часть. Разбиение функциональности системы на аппаратную и программную производится обычно из соображений производительности: чем выше требования к производительности определённых частей СнК, тем лучше реализовать их в виде аппаратных, а не программных блоков.

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

1.2. Традиционный процесс разработки систем на кристалле

Ранее в течение десятилетий проектирование СБИС велось по классической каскадной модели [1]. Классический процесс проектирования вычислительной системы может быть формально разделен на несколько стадий: планирование, разработка спецификации архитектуры, разработка микроархитектуры, описание системы на уровне регистровых передач (RTL), а также логический и физический синтез.

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

На стадии разработки спецификации архитектуры определяются основные требования к системе, её будущие характеристики и основные функциональные блоки.

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

На следующем этапе создаётся RTL-код аппаратных блоков системы на языках описания аппаратуры, таких как Verilog или VHDL. RDL-код детально описывает потоки сигналов между аппаратными регистрами и логические операции над данными. После разработки RTL-кода в классическом процессе начинается функциональная верификация системы

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

Общая схема традиционного каскадного процесса разработки СнК приведена на рис. 1.2.

С усложнением разрабатываемых СБИС возникла проблема: традиционный каскадный процесс не может обеспечить достаточный уровень покрытия верификации системы. Это объясняется тем, что в рамках традиционного процесса проектирования большинство действий по валидации систем проводились уже после создания ЯТЬ-кода. Одной из главных причин этого являлось отсутствие полных и завершённых моделей даже отдельных аспектов структуры и поведения системы [3]. Однако описание на уровне регистровых передач является слишком низкоуровневым для того, чтобы в короткие сроки провести полную валидацию системы, содержащей сотни миллионов элементов. Поэтому с усложнением проектируемых вычислительных систем стали прикладываться серьёзные усилия для того, чтобы перейти на более высокий уровень абстракции для описания и верификации систем. Требовалось создать новые способы формального описания системы, причём как аппаратной её части, так и программного обеспечения, и разработать новую методологию создания и верификации такого описания на этапе создания спецификаций архитектуры и микроархитектуры системы. Нужно было обеспечить возможность верификации архитектуры системы на самых ранних этапах её разработки, ведь, как известно, ошибки,

допущенные на самых ранних этапах проектирования, «стоят» компании-разработчику дороже всего [4-7].

Разработчики СБИС столкнулись с проблемой выбора новых языков описания системного уровня и методологии проектирования и верификации с использованием этих языков. Любой подобный язык системного уровня должен был обладать двумя основными качествами: иметь возможность объединять множество разнородных моделей и работать на высоком уровне абстракции.

В последние двадцать лет многие возможности были предложены для решения данной задачи [3]:

1. Использование языков описания аппаратуры с некоторыми дополнениями, как, например, расширение языка Verilog до SystemVerilog.

2. Адаптация языков программирования высокого уровня (C/C++, Java) для описания архитектурных спецификаций систем на кристалле.

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

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

В современной практике создания высокоуровневых моделей наиболее

часто применяются языки, разработанные с использованием первых двух подходов, такие как SystemC и SystemVerilog.

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

процесса проектирования [8], что привело к необходимости использовать итерации на каждом таком этапе.

Планирование

т и

Разработка архитектурной спецификации

т и

Проектирование микроархитектуры

т и

Написание RTL-кода

- р-

Функциональная верификация

и

Логический синтез

■ и

Временная верификация

р-

Физический синтез

Рис. 1.2. Традиционный процесс разработки СБИС.

Третьей проблемой традиционного подхода является возрастающая роль встроенного программного обеспечения в СнК [9]. Необходимо было

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

1.3. Современный процесс разработки систем на кристалле

Ответом на эти три проблемы стало создание и внедрение новой модели разработки СнК, называемой спиралевидной [1, 10, 11]. Эта модель выглядит следующим образом.

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

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

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

высокоуровневого моделирования. На этом этапе разработчики системы, применяя итеративный подход, оценивают производительность системы в различных ситуациях и находят оптимальное разделение функций аппаратного и программного обеспечения. Модель СнК, получаемая на этом этапе, является по сути абстрактной платформой и состоит из абстрактных моделей аппаратного и программного обеспечения. Например, модель программного обеспечения может точно имитировать наиболее часто используемую функциональность, исполнение операций ввода/вывода и другие важнейшие операции. Абстрактная модель аппаратной части платформы может быть описана на поведенческом уровне или на уровне транзакций. Результатом этого этапа проектирования является золотая модель архитектуры, в дальнейшем использующаяся в роли абсолютного стандарта, на соответствие которому проверяется каждый уровень описания системы. Эта золотая модель может быть как наследована от существующей СнК, так и создана с нуля. После того, как в золотой модели архитектуры определено разбиение задач между аппаратной и программной частями системы, разработка аппаратных и программных блоков может идти параллельно. Помимо этого, параллельно с разработкой IP-блоков идёт процесс физического проектирования будущей СнК. Это связано с тем, что при использовании современных технических процессов уже на стадии кодирования RTL необходимо иметь некоторые сведения относительно используемой технологии, библиотек, а также о предварительной планировке кристалла.

Следующие шаги процесса проектирования можно условно разбить на три параллельных процесса: разработка аппаратных блоков СнК, разработка встроенного программного обеспечения и физическое проектирование [11]. Несмотря на параллельное выполнение этих процессов, они взаимосвязаны, и

результаты определённых этапов одних являются входными данными для некоторых этапов других.

Разработка аппаратных блоков СнК начинается с иерархического временного планирования, после чего, имея окончательные данные по иерархии аппаратных блоков и требованиям к ним, команда разработки приступает к созданию RTL-кода этих блоков. Затем, после готовности RTL-кода, как и в традиционном процессе проектирования, производится его верификация. Для процесса, в котором до RTL была создана золотая модель системы, важнейшей частью верификации RTL-кода является его проверка на соответствие этой модели, в обратном случае золотой моделью становится сам RTL-код. После верификации RTL производится логический синтез, статический временной анализ, физический синтез и так далее.

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

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

последним этапом физического проектирования, выполняющимся после физического синтеза, является финальное размещение элементов на кристалле и детальная трассировка.

Список литературы диссертационного исследования кандидат наук Печенко, Иван Сергеевич, 2018 год

Литература

1) Евтушенко Н., Немудров В., Сырцов И. Методология проектирования систем на кристалле. Основные принципы, методы, программные средства // ЭЛЕКТРОНИКА: Наука, Технология, Бизнес. -2003. - №. 6. - С. 7-11.

2) Спецификация системы на кристалле WonderMedia PRIZM WM8950. [Электронный ресурс] URL: http://www.wondermedia.com.tw/en/products/platform/soc/wm8950 (дата обращения: 01.12.2016)

3) Riccobene E. et al. A SoC design methodology involving a UML 2.0 profile for SystemC // Proceedings of the conference on Design, Automation and Test in Europe-Volume 2. - IEEE Computer Society, 2005. - P. 704-709.

4) Lee Y. et al. Customer Requirements Elicitation based on Social Network Service // KSII Transactions on Internet & Information Systems. -2011. - Т. 5. - №. 10.

5) Keller T. Contextual requirements elicitation // Seminar in Requirements Engineering, Spring 2011, Department of Informatics.

6) Dhungana D., Seyff N., Graf F. Research preview: Supporting end-user requirements elicitation using product line variability models // International Working Conference on Requirements Engineering: Foundation for Software Quality. - Springer Berlin Heidelberg, 2011. - С. 66-71.

7) Kumari S. N., Pillai A. S. A survey on global requirements elicitation issues and proposed research framework // Software Engineering and Service Science (ICSESS), 2013 4th IEEE International Conference on. - IEEE, 2013. - P. 554-557.

8) Henkel J. Closing the SoC design gap // Computer. - 2003. - Vol. 36. -№. 9. - P. 119-121.

9) Cesario W. O. et al. Multiprocessor SoC platforms: a component-based design approach // IEEE Design & Test of Computers. - 2002. - Vol. 19. - №. 6. - P. 52-63.

10) Стешенко В. и др. Проектирование СБИС типа" Система на кристалле". Маршрут проектирования. Синтез схемы // Электронные компоненты. - 2009. - №. 1. - С. 14-21.

11) Бухтеев А. В. Методы и средства проектирования систем на кристалле // Chip news. - 2003. - №. 4. - С. 4-14.

12) Schliebusch O. et al. Architecture implementation using the machine description language LISA // Proceedings of the 2002 Asia and South Pacific Design Automation Conference. - IEEE Computer Society, 2002. - P. 239.

13) Hoffmann A. et al. A survey on modeling issues using the machine description language LISA // Acoustics, Speech, and Signal Processing, 2001. Proceedings.(ICASSP'01). 2001 IEEE International Conference on. - IEEE, 2001. - Vol. 2. - P. 1137-1140.

14) Wieferink A. et al. System level processor/communication co-exploration methodology for multiprocessor system-on-chip platforms // IEE Proceedings-Computers and Digital Techniques. - 2005. - Vol. 152. - №. 1. - P. 3-11.

15) Pees S. et al. LISA—machine description language for cycle-accurate models of programmable DSP architectures // Proceedings of the 36th annual ACM/IEEE Design Automation Conference. - ACM, 1999. - P. 933-938.

16) Barreteau A. System-Level Modeling and Simulation with Intel® CoFluent™ Studio // Complex Systems Design & Management. - Springer International Publishing, 2016. - P. 305-306.

17) Rumbaugh J., Jacobson I., Booch G. Unified modeling language reference manual, the. - Pearson Higher Education. - 2004.

18) Robert T., Perrier V. CoFluent Methodology for UML // A CoFluent Design, White Paper. - 2010.

19) Печенко И.С. Способы представления спецификаций вычислительных систем: проблемы и возможности машинной обработки // Информационные технологии. - 2016. - Т. 22. - № 9. - С. 676-683.

20) Описание структурных диаграмм UML на примере спецификации системы электронной коммерции [Электронный ресурс] URL: http://www.agilemodeling.com/style/componentDiagram.htm (дата обращения: 01.12.2016)

21) Dumas M., Ter Hofstede A. H. M. UML activity diagrams as a workflow specification language // International Conference on the Unified Modeling Language. - Springer Berlin Heidelberg, 2001. - P. 76-90.

22) Описание графических нотаций BPMN [Электронный ресурс] URL: http://www.bpmn.org/ (дата обращения: 01.01.2017).

23) Alur R., Yannakakis M. Model checking of message sequence charts // International Conference on Concurrency Theory. - Springer Berlin Heidelberg, 1999. - P. 114-129.

24) Спецификация архитектуры Microsoft Open Cloud Server [Электронный ресурс] URL: http://www.opencompute.org/wiki/Server/SpecsAndDesigns (дата обращения: 01.12.2016)

25) Mich L., Franch M., Novi Inverardi P. Market research for requirements analysis using linguistic tools // Requirements Engineering. - 2004. - Vol. 9. -№. 2. - P. 151-151.

26) Noebauer G. Creating compact models using standard spreadsheet software // Semiconductor Thermal Measurement and Management, 2001. Seventeenth Annual IEEE Symposium. - IEEE, 2001. - P. 126-133.

27) Abbes F., Casseau E., Abid M. SoC design case study using SystemC specifications // Microelectronics, 2003. ICM 2003. Proceedings of the 15th International Conference on. - IEEE, 2003. - P. 189-193.

28) Mueller W. et al. The simulation semantics of SystemC // Design, Automation and Test in Europe, 2001. Conference and Exhibition 2001. Proceedings. - IEEE, 2001. - P. 64-70.

29) Robles K. et al. Towards an ontology-based retrieval of UML Class Diagrams // Information and Software Technology. - 2012. - Vol. 54. - №. 1. -P. 72-86.

30) Salami H. O., Ahmed M. A. UML artifacts reuse: state of the art // arXiv preprint arXiv:1402.0157. - 2014.

31) Eynard B. et al. UML based specifications of PDM product structure and workflow // Computers in industry. - 2004. - Vol. 55. - №. 3. - P. 301-316.

32) Gavrilescu M. et al. Towards UML software models for Cyber Physical System applications // Telecommunications Forum (TELFOR), 2012 20th. -IEEE, 2012. - P. 1701-1704.

33) Grobelna I., Grobelny M. UML activity diagrams in requirements specification of logic controllers // AIP Conference Proceedings. - AIP Publishing, 2015. - Vol. 1702. - №. 1. - P. 100005.

34) Grobelna I., Grobelny M., Adamski M. Model checking of UML activity diagrams in logic controllers design // Proceedings of the Ninth International Conference on Dependability and Complex Systems DepCoS-RELCOMEX. June 30-July 4, 2014, Brunow, Poland. - Springer International Publishing, 2014. - P. 233-242.

35) Daw Z., Cleaveland R., Vetter M. Integrating model checking and UML based model-driven development for embedded systems // Electronic Communications of the EASST. - 2014. - Vol. 66.

36) Dijkstra E. W. A note on two problems in connexion with graphs // Numerische mathematik. - 1959. - Vol. 1. - №. 1. - P. 269-271.

37) Abraham R., Erwig M. Goal-directed debugging of spreadsheets // Visual Languages and Human-Centric Computing, 2005 IEEE Symposium on. IEEE. - 2005. - P. 37-44.

38) Abraham R., Erwig M. GoalDebug: A spreadsheet debugger for end users // Proceedings of the 29th international conference on Software Engineering. IEEE Computer Society. - 2007. - P. 251-260.

39) Fisher M., Rothermel G., Creelan T., Burnett M. Scaling a Dataflow Testing Methodology to the MultiparadigmWorld of Commercial Spreadsheets // Software Reliability Engineering, 2006. ISSRE'06. 17th International Symposium on. IEEE. - 2006. - P. 13-22.

40) Abraham R., Erwig M. Mutation operators for spreadsheets // Software Engineering, IEEE Transactions. - 2009. - Vol. 35.1. - P. 94-108.

41) Engels G., Erwig M. ClassSheets: automatic generation of spreadsheet applications from object-oriented specifications // Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering. ACM. - 2005. - P. 124-133.

42) Mendes J. Coupled evolution of model-driven spreadsheets // Software Engineering (ICSE), 2012 34th International Conference on. IEEE. - 2012. - P. 1616-1618.

43) Cunha J., Fernandes J. P., Mendes J., Saraiva J. MDSheet: A framework for model-driven spreadsheet engineering // Proceedings of the 34th International Conference on Software Engineering. IEEE Press. - 2012. - P. 1395-1398.

44) Cunha J., Fernandes J. P., Mendes J., Pacheco H., Saraiva J. Bidirectional Transformation of Model-Driven Spreadsheets // ICMT. - 2012. - Vol. 12. - P. 105-120.

45) Stevens P. Bidirectional model transformations in QVT: Semantic issues and open questions // Model Driven Engineering Languages and Systems. Springer Berlin Heidelberg. - 2007. - P. 1-15.

46) Holzmann G. J. The model checker SPIN // IEEE Transactions on software engineering. - 1997. - Vol. 23. - №. 5. - P. 279-295.

47) Bose P. Automated translation of UML models of architectures for verification and simulation using SPIN // Automated Software Engineering, 1999. 14th IEEE International Conference on. - IEEE, 1999. - P. 102-109.

48) Weise C. An incremental formal semantics for PROMELA // Proceedings of the 3rd International SPIN Workshop. - 1997.

49) Distefano S., Scarpa M., Puliafito A. From UML to Petri nets: The PCM-based methodology // Software Engineering, IEEE Transactions. - 2011. - Vol. 37.1. - P. 65-79.

50) Bernardi S., Merseguer J. Performance evaluation of UML design with Stochastic Well-formed Nets // Journal of Systems and Software. - 2007. -Vol. 80.11. - P. 1843-1865.

51) Falcioni D. et al. Direct verification of bpmn processes through an optimized unfolding technique // Quality Software (QSIC), 2012 12th International Conference on. - IEEE, 2012. - P. 179-188.

52) Takemura T. Formal semantics and verification of BPMN transaction and compensation // Asia-Pacific Services Computing Conference, 2008. APSCC'08. IEEE. - IEEE, 2008. - P. 284-290.

53) Grobelna I., Wisniewska M., Wisniewski R., Grobelny M., Mroz P. Decomposition, validation and documentation of control process specification in form of a Petri net // Human System Interactions (HSI), 2014 7th International Conference on. IEEE. - 2014. - P. 232-237.

54) Karatkevich A. Dynamic analysis of Petri net-based discrete systems // Lecture Notes in Control and Information Sciences. - 2007. - Vol. 356, Springer Berlin Heidelberg, 2007.

55) Wisniewski R., Karatkevich A., Adamski M., Kur D. Application of comparability graphs in decomposition of Petri nets // 7th International Conference on Human System Interactions (HSI), Portugal. - 2014. - P. 216220.

56) Alur R., Yannakakis M. Model checking of message sequence charts // International Conference on Concurrency Theory. - Springer Berlin Heidelberg, 1999. - P. 114-129.

57) Alur R., Etessami K., Yannakakis M. Realizability and verification of MSC graphs // Theoretical Computer Science. - 2005. - Vol. 331. - №. 1. - P. 97-114.

58) Finkbeiner B., Krüger I. Using message sequence charts for component-based formal verification // Specification and Verification of Component-Based Systems (SAVCBS Workshop affiliated with OOPSLA'01, Proceedings), volume ISU TR. - 2001. - P. 32-45.

59) Braun A., Gerlach J., Rosenstiel W. Checking temporal properties in SystemC specifications // High-Level Design Validation and Test Workshop, 2002. Seventh IEEE International. - IEEE, 2002. - P. 23-27.

60) Larsen K. G., Pettersson P., Yi W. UPPAAL in a nutshell // International Journal on Software Tools for Technology Transfer (STTT). - 1997. - Vol. 1. -№. 1. - P. 134-152.

61) Herber P., Fellmuth J., Glesner S. Model checking SystemC designs using timed automata // Proceedings of the 6th IEEE/ACM/IFIP international conference on Hardware/Software codesign and system synthesis. - ACM, 2008. - P. 131-136.

62) Gasparini L., Norman T.J., Kollingbaum M.J., Chen L., Meyer J.J.C. Verifying Normative System Specification containing Collective Imperatives and Deadlines // Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems. International Foundation for Autonomous Agents and Multiagent Systems. - 2015. - P. 1821-1822.

63) Plagge D., Leuschel M. Seven at one stroke: LTL model checking for high-level specifications in B, Z, CSP, and more // International journal on software tools for technology transfer. - 2010. - Vol. 12.1. - P. 9-21.

64) Legay A., Delahaye B., Bensalem S. Statistical model checking: An overview // Runtime Verification. Springer Berlin Heidelberg. - 2010. - P. 122135.

65) Harel D. Can programming be liberated, period? // Computer. - Jan. 2008. - Vol. 41, № 1. - P. 28-37.

66) Harel D. From play-in scenarios to code: An achievable dream // Computer. - 2001. - Vol. 34, № 1. - P. 53-60.

67) Navigli R., Velardi P., Gangemi A. Ontology learning and its application to automated terminology translation // IEEE Intelligent systems. - 2003. - Vol. 18. - №. 1. - P. 22-31.

68) Mahesh K., Helmreich S., Wilson L. Ontology development for machine translation: Ideology and methodology. - Computing Research Laboratory, New Mexico State University, 1996.

69) Groff J. R. et al. SQL: the complete reference. - McGraw-Hill/Osborne, 2002. - Vol. 1.

70) Qu Y. Z. et al. Mapping between relational database schemas and ontologies: The state of the art // Journal of Computer Research and Development. - 2008. - Vol. 45. - №. 2. - P. 300-309.

71) Yang S., Wu J. Mapping relational databases into ontologies through a graph-based formal model // Semantics Knowledge and Grid (SKG), 2010 Sixth International Conference on. - IEEE, 2010. - P. 219-226.

72) Vogel-Heuser B., Witsch D., Katzke U. Automatic code generation from a UML model to IEC 61131-3 and system configuration tools // Control and Automation, 2005. ICCA'05. International Conference on. - IEEE, 2005. - Vol. 2. - P. 1034-1039.

73) Chauvel F., Jézéquel J. M. Code generation from UML models with semantic variation points // International Conference on Model Driven Engineering Languages and Systems. - Springer Berlin Heidelberg, 2005. - P. 54-68.

74) Albert M., Cabot J., Gómez C., Pelechano V. Generating operation specifications from UML class diagrams: A model transformation approach // Data & Knowledge Engineering. - 2011. - Vol. 70.4. - P. 365-389.

75) Linzhang W., Jiesong Y., Xiaofeng Y., Jun H., Xuandong L., Guo Z. Generating test cases from UML activity diagram based on gray-box method // Software Engineering Conference, 2004. 11th Asia-Pacific. IEEE. - 2004. -P. 284-291.

76) Amálio N., Glodt C., Kelsen P. Building VCL models and automatically generating Z specifications from them // FM 2011: Formal Methods. Springer Berlin Heidelberg. - 2011. - P. 149-153.

77) Amálio N., Kelsen P. Modular design by contract visually and formally using VCL. // Visual Languages and Human-Centric Computing (VL/HCC), 2010 IEEE Symposium. - 2010. - P. 227-234.

78) Amálio N., Kelsen P., Ma Q., Glodt C. Using VCL as an aspect-oriented approach to requirements modelling. // Transactions on aspect-oriented software development VII, Springer Berlin Heidelberg. - 2010. - P. 151-199.

79) Letichevsky A. et al. Basic protocols, message sequence charts, and the verification of requirements specifications // Computer Networks. - 2005. -Vol. 49. - №. 5. - P. 661-675.

80) Hoare C. A. R. An axiomatic basis for computer programming //Communications of the ACM. - 1969. - Vol. 12. - №. 10. - P. 576-580.

81) Березин В. В. и др. Твердотельная революция в телевидении: Телевизионные системы на основе приборов с зарядовой связью, систем на кристалле и видеосистем на кристалле // М.: Радио и связь. - 2006.

82) Спецификация архитектуры OpenSPARC T2 [Электронный ресурс] URL: http://www.oracle.com/technetwork/systems/opensparc/opensparc-t2-page-1446157.html (дата обращения: 01.07.2016)

83) Thompson J., Heimdahl M., Erickson D. Structuring formal control systems specifications for reuse: Surviving hardware changes //Lfm2000: Fifth NASA Langley Formal Methods Workshop. - National Aeronautics and Space Administration, Langley Research Center, 2000. - Vol. 210100. - P. 117.

84) Печенко И., Петров А. Методология создания спецификаций систем на кристалле // Сборник материалов XVI научно-практической конференции «Современные информационные технологии в управлении и образовании». - 2017. - С. 274-282.

85) Gelhausen T., Tichy W. Thematic Role Based Generation of UML Models from Real Word Requirements // In Proceedings of the 1st IEEE International Conference on Semantic Computing. - 2007. - P. 282-289.

86) Sharma V., Sarkar S., Verma K., Panayappan A., Kass A. Extracting High-level Functional Design from Software Requirements // In Proceedings of the 16th IEEE Asia-Pacific Software Engineering Conference. - 2009. - P. 3542.

87) Deeptimahanti D.K., Sanyal R. An Innovative Approach for Generating Static UML Models from Natural Language Requirements // Advances in Software Engineering, Communication in computer and Information Science. -2009. - Vol. 30. - P. 147-163.

88) Aho A. V., Ullman J. D. The theory of parsing, translation, and compiling. - Prentice-Hall, Inc., 1972.

89) Печенко И., Петров А. Модели данных для архитектурных спецификаций систем на кристалле // Информационные технологии. -2017. - Т. 23. - №7. - С. 536-542.

90) Печенко И.С., Венгер О.В. Способ автоматизированного создания диаграмм последовательности операций для сценариев поведения системы, описанных в виде текста // Информационные технологии. - 2015.

- Т. 21. - №1. - С. 50-56.

91) Кларк Э., Грамберг О., Пелед Д. Верификация моделей программ: Model checking // М.: МЦНМО. - 2002. - Т. 416.

92) Rushby J. Using model checking to help discover mode confusions and other automation surprises // Reliability Engineering & System Safety. - 2002.

- Vol. 75. - №. 2. - P. 167-177.

93) Печенко И.С. Спецификация и валидация протоколов систем на кристалле: проблемы и пути их решения // Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС) - 2016. - №. 2. -С. 92-99.

94) Krstic S. et al. Security of SoC firmware load protocols // Hardware-Oriented Security and Trust (HOST), 2014 IEEE International Symposium on.

- IEEE, 2014. - P. 70-75.

95) Описание языка SystemRDL [Электронный ресурс] URL: http://accellera. org/activities/working-groups/systemrdl (дата обращения: 01.01.2017)

96) Abraham R., Erwig M., Kollmansberger S., Seifert E. Visual specifications of correct spreadsheets // Visual Languages and Human-Centric Computing, 2005 IEEE Symposium. - 2005. - P. 189-196.

97) Burnett, M., Cook, C., Pendse, O., Rothermel, G., Summet, J. and Wallace, C. End-user software engineering with assertions in the spreadsheet paradigm. // In Proceedings of the 25th international conference on Software engineering. - May 2003. - P. 93-103.

98) Fraer R., Keren D., Khasidashvili Z., Novakovsky A., Puder A., Singerman E., Talmor E., Vardi M.Y., Yang J. From visual to logical formalisms for SoC validation // Formal Methods and Models for Codesign (MEMOCODE). 2014. Twelfth ACM/IEEE International Conference. P. 165174.

99) Печенко И., Венгер О., Плоткин Д. ACES Tables: среда для создания и использования табличных спецификаций систем на кристалле // Информационные технологии. - 2017. - Т. 23. - №5. - С. 388-393.

100) Kruijtzer W. et al. Industrial IP integration flows based on IP-XACT standards // Design, Automation and Test in Europe, 2008. DATE'08. - IEEE, 2008. - P. 32-37.

Приложение А. Акты о внедрении результатов диссертационной

работы

«Утверждаю»

Директор по архитектуре «АО Интел А/О» Российского отделения корпорации Intel, член-корреспондент РАН Бабаян Б.А.

_

" аекаеЬА_2016г.

2016г.

Акт внедрения

результатов диссертационной работы Печенко Ивана Сергеевича «Методы разработки и верификации архитектурных спецификаций вычислительных комплексов на основе систем на кристалле», представленной на соискание учёной степени кандидата технических наук по специальности 05.13.15.

Комиссия в составе к.т.н. A.B. Жмурина - председателя, членов комиссии: к.т.н. Д.А.

Плоткина, с.н.с. О.В. Венгера настоящим актом подтверждает, что результаты

диссертационной работы И.С. Печенко:

• предложенные модели данных для создания спецификаций системных протоколов в виде таблиц и диаграмм

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

реализованы в виде программных модулей в рамках экспериментальной программной платформы для работы с архитектурными спецификациями в АО «Интел А/О» в 2016 году. Применение программной платформы при разработке различных элементов архитектуры промышленных СнК показало, что она позволяет существенно повысить качество спецификаций, своевременно выполнить эффективную верификацию спецификаций и ускорить процесс получения формальных моделей системной архитектуры.

УТВЕРЖДАЮ аместитель генерального «Концерн «Вега»

В.А.Михеев

х-о 2017г.

Акт

о внедрении результатов диссертационной работы Печенко И.С.

Комиссия в составе: Крыжановский Ю.М., канд. техн. наук, заместитель начальника отдела - научный руководитель отдела - председатель; члены комиссии Коновалова И.В., начальник отдела, Уэльсон A.B., заместитель начальника отдела, - настоящим актом подтверждает, что результаты диссертационных исследований Печенко Ивана Сергеевича были применены в ходе разработки экспериментальных программно - аппаратных комплексов.

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

Председатель комиссии

Члены комиссии

И.В.Коновалова

A.B.Уэльсон