Публикации

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

Препринт 56

Т.Г. Чурина

Способ построения раскрашенных сетей Петри, моделирующих SDL-системы

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

Препринт 55

И.С. Ануреев

Применение систем переписывания формул в автоматической верификации программ

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

Препринт 54

И.С. Ануреев

Теория систем переписывания формул

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

Препринт 51

М.А. Бульонков, Д.В. Кочетов

Визуализация свойств программ

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

Препринт 50

A.E. Рязанов

Система БУЦЕФАЛ: комбинирование дедуктивных процедур и описание стратегий поиска доказательств

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

Препринт 49

Д.М. Ушаков

Некоторые формальные аспекты недоопределенных моделей

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

Препринт 48

C.K. Черноножкин

Средства профилирования программ в проекте СОКРАТ

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