Препринты Института систем информатики СО РАН 2012 г.

На первый взгляд верификация программ – это надежный метод, что гарантируется ее проработанной формальной базой. Однако она работает без проблем только в идеальном случае, когда программа и ее спецификация корректны, теория проблемной области полна и доказатель теоремы достаточно мощный. При нарушении любого из этих требований верификация значительно усложняется. Помимо возможных проблем в формальных основах (не рассматриваются в данной работе) причиной может быть то, что верификация, как процесс, по-прежнему использует неформальные или полуформальные методы. К ним относится локализация ошибок. Данная работа является обзором методов локализации/объяснения ошибок, разработанных в проекте C-light для решения этой проблемы. Их применение показано на примерах.

Описаны алгоритмы трансляции UCM-спецификаций (Use Case Maps) в раскрашенные сети Петри (CPN). UCM-спецификации позволяют описывать функциональные требования к системе в графической нотации, изображающей сценарии как совокупность причинно-следственных связей между событиями в системе, которые опционально привязаны к ее архитектуре. Рассматриваются все основные стандартные конструкции UCM за исключением сложных конструкций декомпозиции. Трансляция UCM-спецификаций в CPN модель проиллюстрирована примером.

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

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

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

Описаны три алгоритма пирамидальный сортировки: классический, алгоритм Флойда и улучшенный алгоритм, причем последний является самым быстрым из существующих алгоритмов сортировки. Алгоритмы представлены на языке предикатного программирования P вместе со спецификациями в виде предусловий и постусловий. Дедуктивная верификация алгоритмов в системе автоматического доказательства PVS вместе с повторными релизами спецификаций потребовала около двух месяцев.

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

Описывается реализация контроля динамической семантики предикатных программ в системе предикатного программирования методом доказательства условий семантической корректности в системе автоматического доказательства PVS. Условия семантической корректности программы транслируются в систему автоматического доказательства PVS.