Повышение эффективности систем автоматизированного проектирования встраиваемых комплексов
Верификация программных систем – вид деятельности, направленный на выявление соответствия проверяемой программы заранее определенным требованиям качества, например, степень уверенности в корректности программы. При этом необходимым условием обеспечения качества программных систем (ПС) является наличие эффективного метода валидации/верификации ПС. Степень возможной уверенности в правильности программы определяется не только внешним описанием и режимом ее работы, но и внутренней структурой. Поэтому тестирование программ без учета структуры может доказать только наличие ошибок, а не их отсутствие. До настоящего момента автоматическая верификация программ была не распространена в ежедневной практике программистов, поскольку не существовало верификаторов, способных выполнить данную работу за приемлемое время.
На данный момент в области верификации сделаны следующие шаги:
- Разработан метод автоматизированной верификации программ Model Checking (проверка на модели). Суть его заключается в представлении программы в виде простой модели с конечным числом состояний, а требований - в виде предикатов темпоральной логики.
- Разработан теоретический базис (временные автоматы, темпоральная логика, логика Хоара.
- Разработаны инструменты верификации.
- Разработаны САПР:
- Perspec System Verifier фирмы Cadence. Реализованы средства верификации с помощью программного обеспечения. Основная идея этой технологии заключается в автоматической генерации тестов на уровне программного обеспечения, которые нацелены на максимальную загрузку системы коммуникаций между вычислительными ядрами проекта. Ожидается, что такой подход позволит существенно сократить время отладки сложных проектов.
- Industry's Highest Performance Simulation Solution фирмы Synopsis предоставляет средство верификации, а также поддержку моделирования, System Verilog и другие инструменты.
- Цена одной копии подобных САПР составляет около 40 тыс.$, стоимость разработки – порядка 700 млн.$.
Отметим, что для подобных САПР характерны следующие основные недостатки, обусловленные инструментарием в группе проверки на модели:
- эффект «комбинаторного взрыва» числа состояний, а в связи с этим – ограничения на длину проверяемой формулы;
- отсутствие методологических основ для автоматизированного формирования требований;
- узкая область применения для каждого из инструментов;
- многие из них требуют использования специализированного языка моделирования;
Одним из наиболее приоритетных направлений, связанных с разрешением этих недостатков, является снятие ограничение на число состояний, т.е. эффекта "комбинаторного взрыва".
Для исключения недостатков были проведены исследования, целью которых являлось повышение эффективности систем автоматизированного проектирования встраиваемых комплексов и решения задач валидации всех типов программного обеспечения. Поставленная цель достигается на основе решения научной задачи, связанной с созданием технологической среды, реализующей концепцию логико-темпорального пространства, и обеспечивающую создание верификационно-моделирующего модуля динамического анализа программного образа проектируемой системы.
В основе предлагаемой среды верификации лежат следующие основные концепции:
- Интеграция процесса контроля качества в процесс разработки ПО. Т.е. еще на этапе выработки требований (которые сразу формализуются и добавляются в базу знаний системы) вырабатываются случаи использования, определенные этими требованиями, создаются необходимые объекты.
- В основе построения среды верификации лежит использование формальных моделей, которые строятся по коду разработанной системы.
- На основе формальной модели и базы знаний требований строятся автоматизированные тесты, охватывающие значительную часть кода.
Для технологического процесса характерно то, что еще на этапе построения ТЗ будущей системы вырабатываются требования, проводится их формализация, а также разрабатываются варианты использования (Use Case). В процессе проектирования и разработки на основе исходных кодов программы вырабатываются формальные модели с помощью метода Model Checking, основная идея которого заключается в описании разрабатываемой системы в терминах темпоральной логики и поиске в полученной таким образом базе знаний контрпримеров опровергающих требования. Кроме того, предполагается использование символьных алгоритмов для избавления от комбинаторного взрыва числа состояний полученной модели. При этом обобщение разработанного алгоритма приведено в предложенной методике верификации, отвечающей на вопрос как надо организовать технологический процесс проверки. Структура методики представляет собой последовательность этапов, совокупность обоснованных методов и последовательность выполнения этапов проверки. Сущность методики можно охарактеризовать следующими положениями:
- Переход от программы на языке Verilog к логическому представлению в терминах троек Хоара;
- Разбиение программы на подпроцессы так, чтобы каждый из подпроцессов обеспечивал свойства сильной причинно-следственной связанности и детерминированности для каждого из выходных процессов (с учетом заранее наложенных правил спецификации, выраженных в виде логических утверждений);
- Представлении каждого из подпроцессов в виде управляющего и операционного автоматов (теоретическим обоснованием является теорема Глушкова о структурной полноте). Получение функций управляющих воздействий.
- Верификация программы методом проверки выполнимости правил спецификации на множестве полученных функций управления.