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

• Быковский Сергей Вячеславович
• кандидат наук
• 2015

Оглавление диссертации кандидат наук Быковский Сергей Вячеславович

Введение

1 Обзор методов и средств функциональной верификации и встроенного функционального мониторинга СнК

1.1 Введение

1.2 Технологическая цепочка проектирования СнК

1.2.1 Особенности процесса проектирования СнК

1.2.2 Ошибки процесса проектирования реализации и эксплуатации

1.3 Эффективность современных методов и средств функциональной верификации СнК

1.3.1 Задача функциональной верификации СнК

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

1.4 Функциональный мониторинг СнК

1.4.1 Задача функционального мониторинга

1.4.2 Методы анализа результатов мониторинга

1.5 Встроенный функциональный мониторинг СнК

1.5.1 Классификация и критика существующих средств встроенного мониторинга

1.5.2 Средства автоматизации проектирования подсистемы функционального мониторинга

1.6 Выводы

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

2 Метод встроенного функционального мониторинга с динамической актуализацией модели поведения

2.1 Введение

2.2 Структура метода

2.3 Выбор математической модели для описания поведения вычислительного процесса

2.3.1 Правила спецификации алгоритма взаимодействия процессов

2.3.2 Правила спецификации алгоритма функционирования процессов

2.4 Разработка алгоритма динамической актуализации модели поведения

2.4.1 Задача наблюдения за функционированием процесса

2.4.2 Выделение состояний процесса на основе последовательности произошедших событий

2.4.3 Выделение состояний процесса на основе фактов произошедших событий

2.4.4 Выделение состояний процесса на основе структуры модели ожидаемого поведения

2.4.5 Профиль наблюдения за функционированием процесса

2.5 Анализ актуализированной модели поведения

2.5.1 Базовый метод анализа актуализированной модели

2.5.2 Определение вероятностных и временных характеристик процесса

2.6 Выводы

3 Разработка методов и средств автоматизации синтеза системы функционального мониторинга СнК

3.1 Введение

3.2 Технология автоматизированного синтеза системы функционального мониторинга

3.3 Микроархитектура встроенного монитора с динамической актуализацией модели поведения

3.3.1 Обобщенная структура монитора

3.3.2 Блоки захвата и арбитража событий

3.3.3 Блок обработки событий

3.3.4 Надежность монитора

3.4 ^тез блоков мониторов из высокоуровневого описания модели ожидаемого поведения

3.5 Выводы

4 Практика встроенного функционального мониторинга СнК

4.1 Введение

4.2 Сферы применения метода

4.3 Система функционального мониторинга для СнК цифровой обработки быстрых радиосвязных сигналов

4.4 Система функционального мониторинга для унифицированной информационно-измерительной платформы СнК

4.5 Выводы

Заключение

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

Список литературы

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

А.1 Акт о внедрении в ОАО «НЦ ПЭ»

А.2 Акт о внедрении в ФГУП «ЦНИРТИ им. академика А.И. Берга»

Приложение Б Спецификация процессов-бенчмарков

Б.1 Ведущее устройство протокола Modbus

Б.2 Ведущее устройство протокола PAR

Приложение В Листинг программных средств автоматизации проектирования системы функционального мониторинга

В.1 Реализация алгоритма поиска минимальной модели актуализации GAM

В.2 Реализация алгоритма определения настроек алгоритма наблюдения для OMF-

монитора

В.3 Реализация алгоритма восстановления модели ожидаемого поведения MOB на основе модели актуализации GAM

В.4 Реализация алгоритма восстановления модели наблюдаемого поведения MOB на

основе классов эквивалентности модели ожидаемого поведения MEB

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

Введение

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

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

Больше половины (52%) ошибок, выявленных на этапе натурных испытаний и эксплуатации, относятся к ошибкам в алгоритмах управления и взаимодействия СФ-блоков, в число которых входят процессоры, аппаратные ускорители, коммуникационные контроллеры и др.

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

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

Верификация системы с использованием мониторов утверждений (assertion- based verification), позволяет фиксировать только факт некорректного поведения. После обнаружения сбоя, для поиска его причин, необходимо проводить уточнение утверждений, вводить в систему новые мониторы. Изменение структуры прототипа и повтор испытаний увеличивает время реализации проекта при проектировании системы на ПЛИС и требует финансовые вложения при выпуске СнК в виде интегральной схемы.

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

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

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

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

- внезапные и перемежающиеся отказы;

- несколько сбоев/отказов за один цикл наблюдения;

- последовательность событий, которая привела к сбою/отказу.

Задачи исследования.

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

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

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

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

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

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

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

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

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

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

3. Предложена микроархитектура конфигурируемого встроенного монитора, реализующего разработанный метод мониторинга.

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

Основные защищаемые положения.

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

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

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

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

Практическая значимость. В процессе диссертационного исследования были получены следующие практические результаты:

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

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

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

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

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

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

2. Может быть использован в качестве основы при создании средств САПР для решения задачи натурной верификации.

Апробация результатов работы производилась в 10 докладах на 8 конференциях, из которых 2 всероссийские и 3 международные:

1. The 13th IEEE International Symposium on Parallel and Distributed Processing with Applications (IEEE ISPA-15), the 1st IEEE International Workshop on Distributed Intelligent Automation Systems. Helsinki. Finland. 2015.

2. The 4th Mediterranean Conference on Embedded Computing. Budva. Montenegro. 2015.

3. XLIV научной и учебно-методической конференции. Университет ИТМО. Санкт-Петербург. 2015 г.

4. 14th GeoConference on Informatics, Geoinformatics and Remote Sensing. SGEM 2014. Albena. Bulgaria. 2014.

5. VI Научно-практическая конференция молодых ученых «Вычислительные системы и сети (Майоровские чтения)». Университет ИТМО. Санкт- Петербург. 2014 г.

6. III Всероссийский конгресс молодых ученых. Университет ИТМО. Санкт- Петербург. 2014 г.

7. XLIII научная и учебно-методическая конференция. Университет ИТМО. Санкт-Петербург. 2014 г.

8. II Всероссийский конгресс молодых ученых. Университет ИТМО. Санкт- Петербург. 2013 г.

Публикации. Основные результаты опубликованы в 8 научных публикациях общим объемом в 41 стр, в том числе в 3-х статьях в изданиях, включенных в перечень ВАК, и 4-х статьях в изданиях, индексируемых SCOPUS.

Внедрение результатов работы. Основные результаты работы были внедрены:

1. В ОКР:

1.1. «Разработка программного обеспечения ПЛИС модулей блока обработки информации» (ОАО «НЦ ПЭ», г. Санкт-Петербург, 2013-2014 гг.). Применение разработанных блоков аппаратных мониторов позволило на этапе

натурных испытаний установить причины 90% внезапных и перемежающихся отказов. По сравнению с используемыми методами протоколирования событий эффективность мониторинга увеличилась в 1.8 раз (приложение А.1).

1.2. «Разработка и изготовление образца цифровой системы управления и обработки информации» (ФГУП «ЦНИРТИ им. академика А.И. Берга», г. Москва, 2013-2014 гг.). В результате применения разработанных метода и средств проектирования была создана система функционального мониторинга нового типа, позволяющая проводить непрерывное наблюдение за поведением системы в процессе всего цикла автономных испытаний (8 часов) без участия оператора (приложение А.2).

2. В НИР:

2.1. НИР № 214434 «Исследование механизмов обеспечения надежности аппаратно-резервированных информационно-измерительных систем на базе ПЛИС» (Университет ИТМО, 2014 г.). Результаты были использованы в качестве основы для разработки архитектуры подсистемы сбора и обработки данных о параметрах узлов вычислительных систем на базе ПЛИС и для разработки средств измерения и оценки функциональных параметров узлов вычислительных систем на ПЛИС.

2.2. НИР № 713564 «Создание бесшовных технологий проектирования встраиваемых систем и систем на кристалле на основе реконфигурируемых архитектур» (Университет ИТМО, 2013 г.). Результаты диссертационной работы использовались при определении направлений и плана исследований и в качестве составляющих комплекса методов проектирования многоядерных реконфигурируемых систем на кристалле.

3. В учебных курсах магистратуры (кафедра вычислительной техники, Университет ИТ-МО, 2015 г.):

3.1. М.2.2.4 «Методы и технологии проектирования систем на кристалле» (магистерская программа: 230100.68.14 «Системотехника интегральных вычислителей. Системы на кристалле», направление подготовки 230100.68.00 «Информатика и вычислительная техника»);

3.2. М.2.2.5 «Организация вычислительного процесса: модели и методы» (магистерская программа: 230100.68.13 «Проектирование встроенных вычислительных систем», направление подготовки 230100.68.00 «Информатика и вычислительная техника»).

4. В исследованиях международной научной лаборатории Университета ИТМО «Архитектура и методы проектирования встраиваемых систем и систем на кристалле» (2014 г.).

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

Структура и объем работы. Диссертация состоит из введения, четырех глав, заключения и трех приложений. Полный объем диссертации 113 страниц текста с 35 рисунками и 15 таблицами. Список литературы содержит 106 наименований.

1. Обзор методов и средств функциональной верификации и встроенного функционального

мониторинга СнК

1.1 Введение

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

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

1.2 Технологическая цепочка проектирования СнК 1.2.1 Особенности процесса проектирования СнК

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

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

- методы и средства системного проектирования, ориентированные на создание гетерогенной (аппаратно-программной) вычислительной платформы;

- повторное использование в проекте готовых библиотечных аппаратных блоков (I?-ядер);

- следование определенному набору стандартов, регламентирующих правила упаковки и вывода на рынок, как всей системы, так и её подсистем.

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

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

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

Рисунок 1.1 - Этапы системного подхода к проектированию СнК

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

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

Современные системы автоматизированного проектирования (САПР) фирм Synopsys, Cadence, Mentor Graphics, Xilinx, Altera содержат инструменты для автоматизации процесса трансляции моделей системы между разными уровнями абстракции: уровнем регистровых пересылок (register transfer level, RTL), логическим и уровнем топологии (в рамках стандартного техпроцесса). Процесс трансляции моделей данных уровней хорошо формализован и требует от разработчика минимального участия.

Сегодня существуют также средства высокоуровневого синтеза (High-Level Synthesis, HLS) [2], осуществляющие преобразование высокоуровневых моделей до уровня RTL и дальше до уровня топологии. К таким средствам относятся программные продукты C-to-Silicon Compiler (Cadence), Catapult C (Calypto Design Systems), Synphony Model Compiler (Synopsys), Vivado HLS (Xilinx) [3]. Данные средства имеют ограниченную сферу применения и обычно используются для синтеза блоков цифровой обработки сигналов, а также подсистем потоковой обработки данных из описания логики их работы с помощью языков C/C++, Matlab. Ограниченная сфера применения средств HLS обуславливается отсутствием эффективных методов преобразования высокоуровневых моделей.

Переход с более высокого уровня абстракции на более низкий является многовариантным, в то время как критерий выбора лучшего варианта еще недостаточно формализован. С целью уменьшения размерности задачи на отдельных этапах проектирования разработчики делают выбор в пользу использования либо готовых СФ-блоков (component-based design) [1,4], либо проверенной вычислительной платформы (platform-based design) [5].

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

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

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

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

1.2.2 Ошибки процесса проектирования реализации и эксплуатации

Ошибки могут появляться в проекте на каждом этапе жизненного цикла СнК [6-9]. Как в процессе проектирования, так и на этапах реализации и эксплуатации.

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

Перечисленные ошибки приводят к вычислительным и невычислительным отказам системы. Под отказами понимаются нарушения исправного состояния объекта [10].

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

По данным исследования [11] при производстве СнК только 30% устройств готовы к эксплуатации после первого выпуска микросхемы. В среднем же на выявление и устранение ошибок требуется повторить выпуск микросхемы 3-5 раз. Стоимость каждого выпуска при современном технологическом процессе доходит до $4 млн., что значительно увеличивает себестоимость проекта.

По статистике [11,12] 50-60% ошибок (рисунок 1.2), приводящих к перевыпуску микросхем, относятся к ошибкам в алгоритмах работы сложно-функциональных блоков (СФ-блоков). Также СФ-блоки содержат большое количество ошибок, пропущенных на этапе проектирования/реализации, из-за несовершенства существующих средств функциональной верификации (подробнее в разделе 1.3.2).

Если ошибки в подсистеме памяти и элементной базе (ошибки соединения проводников) выявляются на первом/втором экземпляре микросхемы, например, с помощью технологии граничного сканирования [13], то ошибки в алгоритмах работы СФ-блоков требуют 3 и более перевыпусков.

11 доля «пропущенных» ошибок

О □ доля микросхем перевыпущенных из-за ошибок данного типа

70 60 50 40 30 20 10

СФ-блоки Подсистема памяти Элементная база

Рисунок 1.2 - Доля ошибок разных типов в проектах СнК перед началом натурных испытаний

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

Ошибки спецификации в 60% случаев [11] являются причинами некорректного функционирования СФ-блоков. Авторы [7] отмечают, что многие системы на практике содержат ошибки не потому, что они не удовлетворяют своей спецификации, а потому что спецификация не содержит описания системы во многих нештатных ситуациях, которые не подразумеваются во время проектирования. Утверждается, что это не зависит от образованности разработчика и не является недостатками методологии проектирования. Это фундаментальная характеристика самого процесса проектирования.

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

1.3 Эффективность современных методов и средств функциональной верификации СнК

1.3.1 Задача функциональной верификации СнК

Согласно ГОСТ ISO 9000-2011 «Системы менеджмента качества. Основные положения и словарь» [14] под «верификацией» понимается подтверждение посредством объектных свидетельств того, что установленные требования были выполнены. Термин «требование» определяется как потребность или ожидание, которое установлено, обычно предполагается и является обязательным.

Следуя классификации терминов, приведенной в [14], понятие «верификация» относят к процессу оценки, а «требование» - к качеству. Таким образом, процесс верификации связывается с процессом оценки качества.

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

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

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

Функциональные требования к системе описываются в функциональной спецификации. Она определяет требования к составу функций и способам их реализации (ожидаемому поведению). Задачей процесса функциональной верификации является проверка соответствия характеристик системы требованиям её функциональной спецификации. Для краткости изложения, далее по тексту под термином «спецификация» будем понимать именно функциональную спецификацию.

Список литературы диссертационного исследования кандидат наук Быковский Сергей Вячеславович, 2015 год

Список литературы

1. Sinha R., Roop P., Basu S. Correct-by-Construction Approaches for SoC Design. Springer, 2013. P. 144.

2. Coussy P., Morawiec A. High-Level Synthesis. From Algorithm to Digital Circuit. Springer, 2008. P. 297.

3. Meeus W., Beeck K. An overview of today's high-level synthesis tools // Design Automation for Embedded Systems. 2012. Vol. 16, no. 3. P. 31-51.

4. Bricaud P. Reuse Methodology Manual for System-on-a-Chip Designs. 3rd edition. Springer, 2007. P. 312.

5. Sangiovanni-Vincentelli A., Densmore D., Passernone R. A Platform-Based Taxonomy for ESL Design // IEEE Design & Test. 2006. Vol. 23, no. 5. P. 359-374.

6. Wilcox P. Professional Verification. A Guide to Advanced Functional Verification. Springer, 2004. P. 191.

7. Kaeslin H. Digital Integrated Circuit Design: From VLSI Architectures to CMOS Fabrication. Cambridge University Press, 2008. P. 866.

8. Reis R., Lubaszewski M. Design of Systems on a Chip: Design and Test. Springer, 2007. С. 237.

9. Kanekawa N., Ibe E., Suga T. Dependability in Electronic Systems. Mitigation of Hardware Failures, Soft Errors, and Electro-Magnetic Disturbances. Springer Science and Business Media, 2011. P. 226.

10. ГОСТ 27.002-89. Надежность в технике. Основные понятия. Термины и определения. 1990.

11. The 2012 Wilson Research Group Functional Verification Study. 2012. URL: http://blogs.mentor.com/verificationhorizons/blog/2013/09/08/part-12-the-2012-wilson-research-group-functional-verification-study/.

12. Wagner I., Bertacco V. Post-Silicon and Runtime Verification for Modern Processors. Springer, 2011. P. 224.

13. Colin M., Rodham E. The Test Access Port and Boundary Scan Architecture. IEEE Computer Society Press, 1990.

14. ГОСТ ISO 9000-2011. Системы менеджмента качества. Основные положения и словарь. 2012.

15. Viskic I., Gajski D. Modeling Kahn Process Networks on MPSoC Platforms: Tech. Rep.: : 2008.

16. Lee E. A., Sangiovanni-Vincentelli A. Comparing models of computation. 1997. P. 234-241.

17. Грушвицкий Р., Михайлов М. Проектирование в условиях временных ограничений: верификация проектов//Компоненты и технологии, Санкт-Петербург. 2008. Т. 3. С. 96-102.

18. NPR 7123.1B. NASA Systems Engineering. Processes and Requirements. 2013.

19. Naval Systems Engineering Technical Review Handbook. 2009.

20. Laitenberger O. A Survey of Software Inspection Technologies // In Handbook in Software Engineering and Knowledge Engineering. 2002. Vol. 2. P. 517-555.

21. Wong Y.K. Modern Software Review: Techniques and Technologies. IRM Press, 2006.

22. Dobrica L., Niemela E. A survey on software architecture analysis methods // IEEE Transactions on Software Engineering. 2002. Vol. 28, no. 7. P. 638 - 653.

23. Babar M., Gorton I. Comparison of scenario-based software architecture evaluation methods //11th Asia-Pacific Software Engineering Conference. 2004. P. 600 - 607.

24. Кулямин В.В. Методы верификации программного обеспечения. М.: Институт Системного Программирования РАН, 2008. С. 111.

25. Fitting M. First-Order Logic and Automated Theorem Proving. 2nd edition. Springer, 1996. P. 326.

26. Newborn M. Automated Theorem Proving: Theory and Practice. Springer, 2001. P. 237.

27. Molitor P., Mohnke J. Equivalence Checking of Digital Circuits: Fundamentals, Principles, Methods. Springer, 2010. P. 263.

28. Huang S., Cheng K. Formal Equivalence Checking and Design Debugging. Springer, 1998. P. 229.

29. Карпов Ю.Г. MODEL CHECKING. Верификация параллельных и распределенных программных систем. СПб: БХВ-Петербург, 2010. С. 560.

30. Baier C., Katoen J. Principles of Model Checking. The MIT Press, 2008. P. 984.

31. Grumberg O., Veith H. 25 Years of Model Checking: History, Achievements, Perspectives. Springer, 2008. P. 234.

32. Boulanger J. Static Analysis of Software: The Abstract Interpretation. Wiley-ISTE, 2011. P. 331.

33. Hertz S., Sheridan D., Vasudevan S. Mining Hardware Assertions With Guidance From Static Analysis // IEEE Transactions on Computer-Aided Design of Integrated circuits and systems. 2013. Vol. 32, no. 6. P. 952-965.

34. Kamkin A., Smolov S., Melnichenko I. Static analysis of HDL descriptions: Extracting models for verification//Design & Test Symposium. 2013. P. 1-4.

35. Карпов Ю.Г. Теория автоматов. СПб.: Питер, 2003. С. 208.

36. Хопкрофт Дж. Э., Мотвани Р., Ульман Дж. Д. Введение в теорию конечных автоматов. М.: Вильямс, 2002.

37. Bresolin D., El-Fakih K., Villa T. Deterministic Timed Finite State Machines: Equivalence Checking and Expressive Power // Proceedings of the Fifth International Symposium on Games, Automata, Logics and Formal Verification. 2014. P. 203-216.

38. Bengtsson J., Yi W. Timed Automata: Semantics, Algorithms and Tools // Lecture Notes in Computer Science. 2004. Vol. 3098. P. 87-124.

39. Kempf T., Ascheid G., Leupers R. Multiprocessor Systems on Chip: Design Space Exploration. Springer, 2011. P. 189.

40. Sokolova A., Vink E. Probabilistic Automata: System Types, Parallel Composition and Comparison // Validation of Stochastic Systems: A Guide to Current Research. 2004. P. 1-43.

41. GimbertH., Oualhadj Y. Probabilistic Automata on Finite Words: Decidable and Undecidable Problems//ICALP. Springer-Verlag Berlin Heidelberg, 2010. P. 527-538.

42. Henzinger T. The Theory of Hybrid Automata // 11-th Annual IEEE Symposium on Logic in Computer Science. 1996. P. 278-292.

43. Abraham E. Modeling and Analysis of Hybrid Systems. Faculty of Mathematics, Computer Science, and Natural Sciences RWTH Aachen University, 2012. P. 113.

44. Tretmans J. Model Based Testing with Labelled Transition Systems // Formal Methods and Testing. Lecture Notes in Computer Science. 2008. Vol. 4949. P. 1-38.

45. Haase J. Models, Methods, and Tools for Complex Chip Design. Springer, 2013. P. 250.

46. Steven P. M. Formal Verification of Synchronous Models: An Industrial Application of Formal Methods: Tech. Rep.: : 2007.

47. Питерсон Дж. Теория сетей Петри и моделирование систем. 1984. С. 264.

48. Шалыто А.А. SWITCH - технология. Алгоритмизация и программирование задач логического управления. СПб.: Наука, 1998. С. 628.

49. Burch J., Clarke E., McMillan K. Symbolic model checking: 1020 States and beyond // Information and Computation. 1992. Vol. 98, no. 2. P. 142-170.

50. Takayama K., Satoh T., Nakata T. An approach to verify a large scale system-on-a-chip using symbolic model checking // Computer Design: VLSI in Computers and Processors. 1998. P. 308313.

51. Foster H., Krolnik A., Lacey D. Assertion-based design. second edition. Springer, 2004. P. 390.

52. Yuan J., Pixley C., Aziz A. Constraint-Based Verification. Springer, 2006. P. 254.

53. Prabhat M., Nikil D. Functional Verification of Programmable Embedded Architectures. Springer, 2005. P. 180.

54. Kornaros G., Pnevmatikatos D. A Survey and Taxonomy of On-Chip Monitoring of Multicore Systems-on-Chip // ACM Transactions on Design Automation of Electronic Systems. 2013. Vol. 18, no. 2. P. 38.

55. Delgado N., Gates A., Roach S. A taxonomy and catalog of runtime software-fault monitoring tools // IEEE Transactions on Software Engineering. 2004. Vol. 30, no. 12. P. 859-872.

56. Peters D., Parnas D. Requirements-based monitors for real-time systems // IEEE Transactions on Software Engineering. 2002. Vol. 28, no. 2. P. 146-158.

57. Santanu SarmaN., DuttN., Nicolau P. G. On-chip self-awareness using cyberphysical-systems-on-chip (CPSoC) // Proceedings of the 2014 International Conference on Hardware/Software Codesign and System Synthesis. 2014. P. 1-3.

58. Zilic Z., Boule M. Generating Hardware Assertion Checkers: For Hardware Verification, Emulation, Post-Fabrication Debugging and On-Line Monitoring. Springer, 2010. P. 280.

59. Barringer H., Havelund K. TraceContract: A Scala DSL for Trace Analysis // FM 2011: Formal Methods. Springer, 2011. P. 57-72.

60. Cook E., Wolf A. Discovering models of software processes from event-based data // ACM Transactions on Software Engineering and Methodology (TOSEM). 1998. Vol. 7, no. 3. P. 215-249.

61. Трахтенброт Б.А., Барздинь Я.М. Конечные автоматы. Поведение и синтез. М.: Наука, 1970. С. 400.

62. Кудрявцев В.Б., Грунский В.А., Козловский В.А. Восстановление автоматов по фрагментам поведения// Дискретная математика. 2009. Т. 21, № 2. С. 3-42.

63. Кудрявцев В.Б., Грунский В.А., Козловский В.А. Анализ поведения автоматов // Дискретная математика. 2009. Т. 21, № 1. С. 3-35.

64. Duarte L., Kramer J., Uchitel S. Model Extraction Using Context Information // Model Driven Engineering Languages and Systems Lecture Notes in Computer Science. 2006. Vol. 4199. P. 380394.

65. Corbett J., Dwyer M. Bandera: extracting finite-state models from Java source code // Proceedings of the 2000 International Conference on Software Engineering. 2000. P. 439-448.

66. ChipScope Pro and the Serial I/O Toolkit. 2015. URL: http://www.xilinx.com/tools/cspro.htm.

67. Е. Гурин. Использование логического анализатора ChipScope Pro для отладки цифровых устройств на ПЛИС фирмы Xilinx//Компоненты и технологии. 2007. Т. 7. С. 108-112.

68. Design Debugging Using the SignalTap II Logic Analyzer // Quartus II Handbook Volume 3: Verification. 2014. P. 268-338.

69. CoreSight SoC Components. 2015. URL: http://www.arm.com/products/system-ip/debug-trace/coresight-soc-components/index.php.

70. Stollon N. On-Chip Instrumentation: Design and Debug for Systems on Chip. Springer Science and Business Media, 2011. P. 244.

71. Stollon N. OCP System In Silicon Instrumentation Solutions. More Than Just Trace // Chip Design Magazine. 2007.

72. Edge J. A look at ftrace. 2009. URL: https://lwn.net/Articles/322666/.

73. Kevin S., Clinton L. A Configurable Automatic Instrumentation Tool for ANSI C // Automated Software Engineering Conference. 1998. P. 249-259.

74. Shobaki Mohammed El. On-Chip Monitoring of Single- and Multiprocessor Hardware Real-Time Operating Systems // In 8th International Conference on Real-Time Computing Systems and Applications. IEEE. 2002.

75. Yu Y. Efficient detection of data race conditions via adaptive tracking // In SOSP. 2005. P. 221234.

76. Zhou P., Teodorescu R., Zhou Y. Hard: Hardware-assisted lockset-based race detection // IEEE 13th International Symposium on High Performance Computer Architecture. 2007. P. 121-132.

77. Wen C. NUDA: A non-uniform debugging architecture and nonintrusive race detection for many-core systems // IEEE Transactions on Computers. 2012. Vol. 61, no. 2. P. 199-212.

78. Cuoq P., Kirchner F., Kosmatov N. Frama-C: A Software Analysis Perspective // SEFM'12 Proceedings of the 10th international conference on Software Engineering and Formal Methods. Springer Berlin Heidelberg, 2012. P. 233-247.

79

80

81

82

83

84

85

86

87

88

89

90

91

92

93

Bartetzko D., Fischer C., Moller M. JASS - Java with Assertions // RV'2001, Runtime Verification. Elsevier, 2001. P. 103-117.

Chen F., Rosu G. MOP: An Efficient and Generic Runtime Verification Framework // Proceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems and applications. 2007. P. 569-588.

Lee I. Runtime Assurance Based On Formal Specifications // International Conference on Parallel and Distributed Processing Techniques and Applications. 1999.

Abarbanel Y. FoCs - Automatic Generation of Simulation Checkers from Formal Specifications // Computer Aided Verification. 2000. P. 538-542.

Gajda A., Spallek R. From Hardware Trace to System Knowledge - Data-intensive Hardware Trace Analysis // The Fourth International Conference on Resource Intensive Applications and Services. 2012. P. 1-4.

Lee E. A. The problem with threads // Computer. 2006. Vol. 39, no. 5. P. 33-42.

Metz E., Lencevicius R., Gonzalez T. Performance data collection using a hybrid approach // Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIG-SOFT international symposium on Foundations of software engineering. 2005. P. 126-135.

Bartocci, E., Grosu, R., Karmarkar A. Adaptive Runtime Verification // RV'2012, Runtime Verification / Ed. by Springer. 2012. P. 168-182.

Stoller S., Bartocci E., Grosu R. Runtime verification with state estimation // RV'2011, Runtime Verification. Springer, 2011. P. 193-207.

Meredith P., Jin D., Griffith D. An overview of the MOP runtime verification framework // International Journal on Software Tools for Technology Transfer. 2012. Vol. 14, no. 3. P. 249-289.

Lee E. A., Neuendorffer S., Wirthlin M. J. Actor-Oriented Design of Embedded Hardware and Software Systems // Journal of Circuits, Systems, and Computers (JCSC). 2003. Vol. 12. P. 231260.

Lee E., Zheng H. Operational semantics of hybrid systems // Hybrid Systems: Computation and Control. 2005. P. 25-53.

Zeigler P., Praehofer H., Kim T. Theory of Modeling and Simulation. 2nd edition. 2000. P. 510.

Harel D., Pnueli A. On the development of reactive systems // Logic and Models for Verification and Specification of Concurrent Systems. 1985. Vol. F13. P. 477-498.

Henzinger T. A., Horowitz B., Kirsch C. M. Giotto: A time-triggered language for embedded programming.//EMSOFT. 2001. P. 166-184.

94. Angelov C., Berthing J. Distributed Timed Multitasking - A Model of Computation for Hard RealTime Distributed Systems // From Model-Driven Design to Resource Management for Distributed Embedded Systems. IFIP International Federation for Information Processing. 2006. Vol. 225. P.145-154.

95. Lee E., Messerschmitt D. Static scheduling of synchronous data flow programs for digital signal processing // IEEE Transactions on Computers. 1987. Vol. 36. P. 24-35.

96. Zhou G. Dynamic Dataflow Modeling in Ptolemy II. 2004.

97. Girault A., Lee B., Lee E. Hierarchical finite state machines with multiple concurrency models // IEEE Transactions On Computer-aided Design Of Integrated Circuits And Systems. 1999. Vol. 18. P. 742-760.

98. Bhattacharya B., Bhattacharyya S. Parameterized dataflow modeling of DSP systems // International Conference on Acoustics, Speech, and Signal Processing. 2000. P. 1948-1951.

99. Hewitt C., Bishop P., Steiger R. A universal modular ACTOR formalism for artificial intelligence // IJCAI'73 Proceedings of the 3rd international joint conference on Artificial. SanFrancisco: Morgan Kaufmann Publishers Inc, 1973. P. 235-245.

100. Clinger W. Foundations of actor semantics: Tech. Rep.: : MIT, 1981.

101. Agha G., Thati P. An algebraic theory of actors and its application to a simple object-based language // In From Object-Orientation to Formal Methods. 2004. Vol. 2635. P. 26-57.

102. Vincentelli A., Lavagno L., Sentovich E. Models of computation for embedded system design // In System-level Synthesis. Kluwer Academic Publishers, 1999. P. 45-102.

103. Lee A., Sangiovanni-Vincentelli A. A denotational framework for comparing models of computation // IEEE Transactions on Computer-Aided Design of Integrated circuits and systems. 1998. Vol. 17, no. 12. P. 1998.

104. Liu X. Semantic foundation of the tagged signal model // Technical Report UCB/EECS-2005-31,Electrical Engineering and Computer Sciences University of California at Berkeley. 2005. P. 121.

105. Patterson D.A. H. J. Computer Organization and Design. 4th edition. Morgan Kaufmann Publishers Inc, 2011. P. 914.

106. MODBUS over Serial Line. Specification and Implementation Guide V1.02. 2006.

ПРИЛОЖЕНИЕ А

Акты о внедрении результатов работы А.1 Акт о внедрении в ОАО «НЦ ПЭ»

АКТ О ВНЕДРЕНИИ

научных и Iфактических результатов кандидатской диссертации Ьыковского C.B. на тему «Метод встроенного функционального мониторинга с динамической актуализацией модели поведения для систем на кристалле»

Настоящий акт подтверждает внедрение в фирме ОАО «НЦ ПЭ» результатов, полученных Быковским C.B. а холе исследований по теме диссертационной работы. а именно использование алгоритмических и программных средств автоматизированною синтеза встроенных функциональных мониторов с динамической актуализацией модели поведения. Разработанные средства использовались при создании системы встроенного функционального мониторинга модульной вычислительной системы, состоящей из 6 параллельно работающих систем на кристалле, в СЧ ОКР «Разработка про[раммного обеспечения ПЛИС модулей блока обработки информации».

Использование разработанных средств позволило синтезировать аппаратные блоки встроенных функциональных мониторов, характеризующихся низкими требованиями к плошади кристалла (менее 1% ресурсов ПЛИС), средним временем обработки событий 36 мке и возможностью долговременного наблюдения (до 8 часов) за поведением сложно-функциональных блоков системы с использованием фиксированного объема инструментальной памяти (единицы Кбайт). Применение синтезированных блоков мониторов позволило на этапе натурных испытаний установить причины 90% ннезапных и перемежающихся отказов, 11о сравнению с используемыми методами протоколирования событий эффективность мониторинга увеличилась в 1 К раза.

НАУЧНЫЙ ЦЕНТР ПРИКЛАДНОЙ ЭЛЕКТРОДИНАМИКИ

ОТКРЫТОЕ АКЦИОНЕРНОЕ ОБЩЕСТВО

190103, Рнескя. Санкт-Петербург. Рижский проспект д.26, лит.А, пом.1йН,коМ-22

ОАО «Научный иситр при клал ной злтрпишмшлш

телефон: [phone], факс: [phone] ИНН: 7839498284 КПП: 78190100] ОГРН: 1147847318793 e-mail: «fficcu scafg roup .cum. hup: нHw.staegruup.cum

Генеральный директор ОАО «НЦПЭ», доктор технических наук, профессор

А.2 Акт о внедрении в ФГУП «ЦНИРТИ им.

академика А.И. Берга»

Федеральное космическое агентства ФЕДЕРАЛЬНОЕ ГОСУДАРСТВЕННОЕ УНИТАРНОЕ ПРЕДПРИЯТИЕ «ЦЕНТРАЛЬНЫЙ НАУЧНО-ИССЛЕДОВАТЕЛЬСКИЙ РАДИОТЕХНИЧЕСКИЙ ИНСТИТУТ имени академика А.И. БЕРГА»

Новая Басманная ул., д 20, Москва, 105066

Тел [phone] Факс [phone] Телеграф: ПАЛЬМА Е-лм* posl@cnlrtJU

окпо Ч14В7465. огрн нитпэозмча. иншкпп »аппбаасютпкпмп_

¿/.¿c/S 3 f/j/AL

АКТ О ВНЕДРЕНИИ

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

Настоящий акт подтверждает внедрение на предприятии ФГУП «ЦНИРТИ им. академика А.И. Берга» результатов, полученных Быковским C.B. н ходе исследований по теме диссертационной работы, а именно:

• маршрут и средства проектирования многодоменной системы встроенного функционального мониторинга с динамической актуализацией модели поведения:

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

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

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

Исполняющий обязанности генерального директора ФГУП «ЦНИРТИ им. академика А.И. Берга»

Шпак А В </%, 20] 5 г.

724.18

ПРИЛОЖЕНИЕ Б Спецификация процессов-бенчмарков

Б.1 Ведущее устройство протокола Modbus

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

использован для связи нескольких СнК в модульной вычислительной системе. В качестве процесса-бенчмарка используется реализация алгоритма работы ведущего устройства протокола Modbus. Модель ожидаемого поведения MEB ведущего устройства представлена на рисунке Б.1. Спецификация взята из [106].

е4

Рисунок Б.1 - Модель ожидаемого поведения ведущего устройства протокола Modbus

В таблице Б.1 представлен список наблюдаемых событий для модели МЕВ. Таблица Б.1 - Список наблюдаемых событий для ведущего устройства протокола Modbus

Событие Описание

ео сигнал сброса

ei посылка широковещательного запроса

е2 прерывание от таймера

ез посылка запроса к ведомому устройству

е4 получен ответ от устройства, которое не является адресатом

е5 получен ответ от ведомомго устройства-адресата

ее обнаружена ошибка в ответе от ведомого устройства

ет завершение обработки ошибки

es завершение обработки ответа от ведомого устройства

Таблица Б.2 - Описание состояний ведущего устройства протокола Modbus

Состояние Описание

qo ожидание начала работы

qi ожидание ответа от ведомого устройства

q2 обработка ответа от ведомого устройства

qa обработка ошибки

q4 ожидание таймаута широковещательного запроса

Б.2 Ведущее устройство протокола PAR

Протокол PAR (Positive Acknowledgment with Re-transmission) - протокол передачи данных с подтверждением и повторной передачей. Используется для передачи данных через ненадежные каналы. Каждое передаваемое сообщение маркируется с помощью двух разных маркеров 0 и 1. На стороне приемника с помощью маркеров контролируется последовательность переданных

сообщений.

Модель ожидаемого поведения MEB для ведущего устройства протокола PAR представлена на

рисунке Б.2. Спецификация взята из [29].

Рисунок Б.2 - Модель ожидаемого поведения ведущего устройства протокола PAR

В таблице Б.3 представлен список наблюдаемых событий для модели MEB. Таблица Б.3 - Список наблюдаемых событий для ведущего устройства протокола PAR

Событие Описание

eo прием сообщения от источника

ei передача сообщения в канал: сообщению присваивается маркер 0

e2 получение подтверждения от приемника

ea таймаут передачи сообщения

e4 установка флага готовности к передачи следующего сообщения

e5 передача сообщения в канал: сообщению присваивается маркер 1

Таблица Б.4 - Описание состояний ведущего устройства протокола PAR

Состояние Описание

51 передача первого сообщения в канал

52 ожидание подтверждения первого сообщения от приемника

5з установка флага готовности к передачи второго сообщения

54 ожидание второго сообщения от источника

55 передача второго сообщения в канал

56 ожидание подтверждения второго сообщения от приемника

57 установка флага готовности к передачи первого сообщения

58 ожидание первого сообщения от источника

ПРИЛОЖЕНИЕ В

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

мониторинга

Реализации представленных алгоритмов написаны на языке python.

В.1 Реализация алгоритма поиска минимальной модели

актуализации GAM

def refineEdgeGraph (s) :

s. genEdgeGraph ()

for epoch in xrange(5):

s.edge_graph = nx. MultiDiGraph () for trans in s . edge_graph_trans :

s . edge_graph . add_edge (trans . src_state , trans. dst_state)

label_states_dict_prev = s . getLabelStates ()

eq_states_count_prev = s . eqStatesCount (label_states_dict_prev )

uniq_states_idxs = [] nuniq_states_idxs = []

for label in label_states_dict_prev:

states = label_states_dict_prev [ label ] if (len (states) == 1):

uniq_states_idxs += [s . findEgStates (label , list (states)[0]) ]

else:

for state in states :

nuniq_states_idxs += [s . findEgStates (label , state)]

for state_id x in nuniq_states_idxs :

s . markPath ( state_idx , uniq_states_idxs )

diet = {}

for trans in s . edge_graph_trans :

split_value = str (trans . dst_state ). sp lit (",")

if ( split_value [0] not in diet): diet [ split_value [0]] = []

if ( split_val ue [ 1 : ] not in diet [ split_value [0]]) : diet [ split_value [0]] += [ split_val ue [ 1 : ] ]

new_eg_states = [] new_eg_trans = []

for trans in s . edge_graph_trans :

src_state = str (trans . src_state ) if(src_state in diet):

for label in diet [src_state]:

src_state_name = src_state

mark = " .join (label) if (mark != "") :

src_state_name += "," + mark

new_eg_trans += [ Trans ([ src_state_name , trans . dst_state , trans . in_events , set ()])]

else :

new_eg_trans += [ Trans ([ src_state , trans . dst_state , trans. in_events , set () ]) ]

for trans in new_eg_trans:

split_value = str (trans . src_state ). s p l i t (",")

if ( split_value [0] != "start"):

state_idx = int ( split_value [0])

labels = s . edge_graph_states [ state_idx ][" labels " ] | set ( split_value [ 1 : ])

new_state = {"state": s . edge_graph_states [ state_idx ][" state

" ] , "labels": labels} idx = 1

for i in xrange (len (new_eg_states)) : item = new_eg_states [ i ]

if ((item [" state " ] == new_state [" state "]) & (item[" labels"] == new_state [" labels "])) : idx = i break

if (idx == -1):

new_eg_states += [new_state] idx = len (new_eg_states) - 1

trans . src_state = idx

split_value = str (trans . dst_state ). sp lit (",")

state_idx = int ( split_value [0])

labels = s . edge_graph_states [ state_idx ][" labels " ] | set ( sp l i t_va l u e [ 1 : ] )

new_state = {"state": s . edge_graph_states [ state_idx ][" state "] ,

"labels": labels} id x = -1

for i in xrange (len (new_eg_states)) : item = new_eg_states [ i ]

if ((item [" state " ] == new_state [" state " ]) &(item [" labels " ] == new_state [" labels "])) : idx = i

break

if (idx == -1):

new_eg_states += [new_state] idx = len ( new_eg_states ) - 1

trans . dst_state = idx

s . edge_graph_states = new_eg_states s . edge_graph_trans = new_eg_trans

iter_count = 0 while (1) :

find = 0

for trans in s . edge_graph_trans :

if (trans . src_state != "start"):

src_label = s . edge_graph_states [ trans . src_state ][" labels"]

dst_label = s . edge_graph_states [ trans . dst_state ][" labels"]

event = list (trans . in_events) [0]

intersection = (dst_label - src_label) - set ([event])

if (len (intersection) > 0): find = 1

s . edge_graph_states [trans . src_state ][" labels " ] | = intersection

if (find == 0): break

iter count += 1

if (iter_count == 100) :

print "ERROR in refineEdgeGraph : ITER COUNT OVERFLOW" ,

*50 break

*

label_states_dict_next = s . getLabelStates ()

eq_states_count_next = s . eqStatesCount (label_states_dict_next)

i f ( eq_states_count_next == eq_states_count_prev ) : break

return eq_states_count_next

def genEdgeGraph(s)

s.edge_graph = nx. MultiDiGraph ()

s . edge_graph_states = [] s . edge_graph_trans = []

buf_graph_trans = []

state_id x = 0

for trans in s . model :

eg_state = {"state": trans . dst_state , "labels": trans . in_events . copy()}

eg_state_idx = -1

for i in xrange (len (s . edge_graph_states)) : item = s . edge_graph_states [ i ]

i f (( item [ " state " ] == eg_state [ " state " ] ) & ( item [ " l abels " ] == eg_state [ " label s " ] ) ) : eg_state_idx = i

break

i f ( eg_state_idx == -1) :

s . edge_graph_states += [eg_state] eg_state_idx = len (s . edge_graph_states ) - 1

buf_graph_trans += [Trans ([ trans . src_state , eg_state_idx , trans. in_events , set ( ) ] ) ]

for trans in buf_graph_trans: state = trans . src_state

state_labels = set ( )

fi n d = 0

for i in xrange (len (s . edge_graph_states)) : eg_state = s . edge_graph_states [ i ] i f ( state == eg_state [ " state " ] ) :

s . edge_graph_trans += [Trans([i, trans . dst_state , trans.

in_events , set () ] ) ] fi n d = 1

i f ( fi n d == 0)

s . edge_graph_trans += [Trans ([ trans . src_state , trans . dst_state , trans . in_events , set () ]) ]

def markPath(s, state_idx , uniq_state_idxs ) : a 11_ p a t h = []

s_paths_from_start = list (nx. all_simple_paths (s. edge_graph , "start", state_idx))

for ustate_idx in uniq_state_idxs:

s_paths = list (nx. all_simple_paths (s . edge_graph , ustate_idx ,

state_idx)) for s_path in s_paths:

for s_path_from_start in s_paths_from_start :

if (s. pathIncludeTail( s_path_from_start , s_path)) :

a11_path += list (nx. all_simple_paths (s. edge_graph , ustate_idx , state_idx))

min_len = 0 if ( all_path ) :

min_len = min(map(len , all_path ))

short_simple_paths = [] for path in all_path :

i f ( len ( path ) == min_len ) :

if (path not in short_simple_paths) : short_simple_paths += [path]

for path in short_simple_paths: mark = " ! "

for trans in s . edge_graph_trans :

i f ( trans . dst_state == path [0 ] ) :

mark = list (trans . in_events) [0] break

for state_i in xrange (len (path)-1):

src_state = path[state_i] dst_state = path [ state_i + 1 ]

for trans in s . edge_graph_trans :

if ((trans . src_state == src_state) & (trans . dst_state == dst_state)) : trans . dst_state = str (dst_state) + "," + mark

В.2 Реализация алгоритма определения настроек алгоритма

наблюдения для OMF-монитора

def getMonitorConfig ( self , proc) :

if (proc . refineEdgeGraph () == 0): self. correct_model = 1

# monitor_config

# config line

# {"ev_id":

# { "del_list": set(ev_list)

# }

# }

monitor_config = {} all _event_set = set () i = 0

for item in proc . edge_graph_states :

all_event_set |= item [" labels " ]

print i , ": " , item i += 1

for trans in proc . edge_graph_trans : print trans

for event in list ( all_event_set) :

d e l _l i s t = set ()

for trans in proc . edge_graph_trans :

trans_event = list (trans . in_events) [0] if (event == trans_event) :

dst_labels = proc . edge_graph_states [ trans . dst_state ][" labels"]

if (trans . src_state == "start"):

src_labels = set () else:

src_labels = proc . edge_graph_states [ trans . src_state ][" labels"]

del_list |= src_labels - dst_labels monitor_config [event] = {"del_list": del_list} return monitor_config

В.3 Реализация алгоритма восстановления модели ожидаемого поведения MOB на основе модели актуализации GAM

def extractRefModel ( self) :

self. extract_graph = copy . deepcopy ( self. graph) self. extract_graph .name = " extract_graph "

# extract algorithm based on GAM model (edge_graph_states) for i in xrange (len ( self. extract_graph . states )) : state = self. extract_graph . states [ i ]

if (state != set (["start"])):

match_states = set ()

for item in self. proc_list [0]. edge_graph_states : i f ( state == item [ " labels " ] ) :

match_states |= set ([ item [ " state " ] ] )

i f ( match_states != set () ) :

self. extract_graph . states [ i ] = match_states

# delete trans

new_graph = copy . deepcopy( self. extract_graph )

# delete eq states new_graph . states = []

for state in self. extract_graph . states : if (state not in new_graph . states ) : new_graph . states += [state]

# delete eq trans new_graph . trans = []

for trans in self. extract_graph . trans :

new_tran = copy . deepcopy (trans ) src_state_idx = trans . src_state dst_state_idx = trans . dst_state

new_src_state_idx = new_graph . findState ( self. extract_graph . states [ src_state_idx ])

new_dst_state_idx = new_graph . findState ( self. extract_graph . states [ dst_state_idx ])

new_tran . src_state = "" new_tran . dst_state = ""

if ( new_src_state_idx != -1):

new_tran . src_state = new_src_state_idx

if (new_tran . dst_state != -1):

new_tran . dst_state = new_dst_state_idx

trans_idx = new_graph . findTran (new_tran)

i f ( len ( trans_idx ) == 0) :

new_graph . trans += [new_tran]

self. extract_graph . states = new_graph . states self. extract_graph . trans = new_graph . trans

В.4 Реализация алгоритма восстановления модели наблюдаемого поведения MOB на основе классов эквивалентности модели ожидаемого поведения MEB

def extractGraph ( self , path): states = []

for state in self. graph . states :

states += [ self. findGoldenState ( state ) ]

new_model = []

for trans in self. graph . trans :

src_state = " ," . j o i n (map( str , list ( states [ trans . src_state ]))) dst_state = " ," . j o i n (map( str , list ( states [ trans . dst_state ])))

if (len (src_state) == 0):

src_state = " ," . join (map( str , list ( self. graph . states [ trans . src_state])))

if (len ( dst_state ) == 0):

dst_state = " ," . join (map( str , list ( self. graph . states [ trans . dst_state ]) ))

new_trans = Trans ([ src_state , dst_state , trans . in_events , set () ]) find = 0

for item in new_model:

if (item == new_trans) : find = 1

if (find == 0):

new_model += [new_trans]

new_graph = MyGraph (" monitor_eq_class_extract_model" , new_model)

return new_graph

def findGoldenState ( self , state):

cur_trans = self. proc_list [0]. model state_label = set () new_trans = []

from_start = 0

for i in xrange(len (state)-1, -1, -1): ev = l i s t ( state ) [ i ] if(ev == "-"):

from_start = 1 else:

for trans in cur_trans: