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

Препринт 169

А.В. Промский

Формальный подход к локализации ошибок

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

Препринт в формате PDF (Русский)

Препринт 168

Н.В. Визовитин, В.А. Непомнящий

Алгоритмы трансляции UCM-спецификаций в раскрашенные сети Петри

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

Препринт в формате PDF (Русский)

Препринт 167

И.В. Каблуков, В.И. Шелехов

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

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

Препринт в формате PDF (Русский)

Препринт 166

М.С. Чушкин, В.И. Шелехов

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

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

Препринт в формате PDF (Русский)

Препринт 165

И.С. Ануреев

Системы переходов, ориентированные на разработку средств спецификации и верификации программных систем

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

Препринт в формате PDF (Русский)

Препринт 164

В.И. Шелехов

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

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

Препринт в формате PDF (Русский)

Препринт 163

В.А. Батраков, В.И. Шелехов

Автоматическое доказательство формул корректности предикатной программы в системе Russell

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

Препринт в формате PDF (Русский)

Препринт 162

И.В. Каблуков, В.И. Шелехов

Контроль динамической семантики предикатной программы

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

Препринт в формате PDF (Русский)