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

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

Ключевые слова: система на кристалле; архитектурная спецификация; верификация; автоматизация; шаблон; естественные языки; трансляция.

1. Введение

Сложность современных систем на кристалле ведёт к тому, что на первый план в процессе их проектирования выходит проблема верификации функциональных компонентов и процессов их взаимо­действия. Возникает необходимость начинать верификацию как можно раньше в процессе проектирования, так как чем позже бывают обнаружены ошибки в системе, тем сложнее и дороже обходится их исправление [1, 2].

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

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

2. Требования к предлагаемой методологии

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

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

2) Автоматизировать процесс генерации формальных моделей или их частей из данных спецификации для её дальнейшего анализа и верификации.

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

3. Схема предлагаемой методологии

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

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

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

Рисунок 1. Общая схема предлагаемой методологии

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

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

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

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

4. Заключение

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