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

Настоящая работа посвящена исследованию проблемы автоматического построения сетевых моделей SDL-спецификаций распределенных систем. Язык спецификаций и описаний SDL принят в качестве международного стандарта. Рассматриваются SDL-системы с таймерами, средством сохранения сигнала и приоритетами, позволяющие адекватно представлятьзн ачительный класс коммуникационных протоколов. В качестве моделей выбраны раскрашенные сети Петри, предложенные Йенсеном, которые расширяются посредством семантик времени в смысле Мерлина и приоритетов. В работе представлен метод трансляции SDL-систем в данную сетевую модель.

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

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

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

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

Универсальные методы решения задач изучаются в рамках научной дисциплины “искусственный интеллект”. Настоящая работа посвящена описанию недоопределенных моделей как аппарата для решения задач удовлетворения ограничений. Такие задачи возникают во многих областях науки и техники. Использование метода распространения ограничений в недоопределенных моделях позволяет оценивать множество всех решений такой задачи. В статье даются обоснования недоопределенных моделей. Предлагается понятие недоопределенного расширения многосортной модели, и обсуждаются различные типы таких расширений. Определяются денотационная и операционная семантики распространения ограничений в недоопределенных моделях и доказывается их эквивалентность.

Описываются возможности и назначение системы профилирования ассемблерных и Модула-2 программ, созданной в рамках проекта СОКРАТ. Приводятся необходимые определения и указываются основные подходы при реализации подобных систем. Выделены характерные черты данного подхода. Приводятся примеры работы системы.