Повышение эффективности систем автоматизированного проектирования встраиваемых комплексов

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

На данный момент в области верификации сделаны следующие шаги:

  • Разработан метод автоматизированной верификации программ Model Checking (проверка на модели). Суть его заключается в представлении программы в виде простой модели с конечным числом состояний, а требований - в виде предикатов темпоральной логики.
  • Разработан теоретический базис (временные автоматы, темпоральная логика, логика Хоара.
  • Разработаны инструменты верификации.
  • Разработаны САПР:
  • Perspec System Verifier фирмы Cadence. Реализованы средства верификации с помощью программного обеспечения. Основная идея этой технологии заключается в автоматической генерации тестов на уровне программного обеспечения, которые нацелены на максимальную загрузку системы коммуникаций между вычислительными ядрами проекта. Ожидается, что такой подход позволит существенно сократить время отладки сложных проектов.
  • Industry's Highest Performance Simulation Solution фирмы Synopsis предоставляет средство верификации, а также поддержку моделирования, System Verilog и другие инструменты.
  • Цена одной копии подобных САПР составляет около 40 тыс.$, стоимость разработки – порядка 700 млн.$.

Отметим, что для подобных САПР характерны следующие основные недостатки, обусловленные инструментарием в группе проверки на модели:

  • эффект «комбинаторного взрыва» числа состояний, а в связи с этим – ограничения на длину проверяемой формулы;
  • отсутствие методологических основ для автоматизированного формирования требований;
  • узкая область применения для каждого из инструментов;
  • многие из них требуют использования специализированного языка моделирования;

Одним из наиболее приоритетных направлений, связанных с разрешением этих недостатков, является снятие ограничение на число состояний, т.е. эффекта "комбинаторного взрыва".

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

В основе предлагаемой среды верификации лежат следующие основные концепции:

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

Для технологического процесса характерно то, что еще на этапе построения ТЗ будущей системы вырабатываются требования, проводится их формализация, а также разрабатываются варианты использования (Use Case). В процессе проектирования и разработки на основе исходных кодов программы вырабатываются формальные модели с помощью метода Model Checking, основная идея которого заключается в описании разрабатываемой системы в терминах темпоральной логики и поиске в полученной таким образом базе знаний контрпримеров опровергающих требования. Кроме того, предполагается использование символьных алгоритмов для избавления от комбинаторного взрыва числа состояний полученной модели. При этом обобщение разработанного алгоритма приведено в предложенной методике верификации, отвечающей на вопрос как надо организовать технологический процесс проверки. Структура методики представляет собой последовательность этапов, совокупность обоснованных методов и последовательность выполнения этапов проверки. Сущность методики можно охарактеризовать следующими положениями:

  1. Переход от программы на языке Verilog к логическому представлению в терминах троек Хоара;
  2. Разбиение программы на подпроцессы так, чтобы каждый из подпроцессов обеспечивал свойства сильной причинно-следственной связанности и детерминированности для каждого из выходных процессов (с учетом заранее наложенных правил спецификации, выраженных в виде логических утверждений);
  3. Представлении каждого из подпроцессов в виде управляющего и операционного автоматов (теоретическим обоснованием является теорема Глушкова о структурной полноте). Получение функций управляющих воздействий.
  4. Верификация программы методом проверки выполнимости правил спецификации на множестве полученных функций управления.

Другие проекты