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

Препринт 148
З.В. Апанович
От рисования графов к визуализации информации

Методы визуализации информации широко применяются последние годы в таких областях как биологические науки, искусственный интеллект, анализ финансовой информации и т.д. Визуализация информации – это процесс преобразования больших и сложных видов абстрактной информации в визуальную форму. Универсальным средством представления такой информации являются графы. Данная работа имеет целью показать эволюцию методов визуализации графов в связи с потребностями визуализации информации и имеет обзорный характер.

Препринт 147
В.А. Непомнящий, Е.В. Бодин, С.О. Веретнов
Язык спецификаций распределенных систем Dynamic-REAL

В настоящей работе описан язык спецификаций распределенных систем Dynamic-REAL (dREAL), который расширяет разработанный ранее язык Basic-REAL посредством динамических конструкций порождения и уничтожения экземпляров процессов. Язык dREAL включает подъязыки выполнимых и логических спецификаций. В работе представлены синтаксис и формальная семантика языка dREAL. В качестве примера рассматривается протокол управления сетью касс-терминалов.

Препринт 146
Э.Г. Тумуров
Технология спецификации коммуникационных протоколов

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

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

Препринт 145
В.И. Шелехов
Модель корректности программ на языке исчисления вычислимых предикатов

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

Препринт 144
М.Ю. Машуков, Т.Г. Чурина
Моделирование спецификаций языка SDL с помощью раскрашенных сетей Петри

В работе рассматриваются SDL-спецификации распределенных систем с динамическим порождением и уничтожением экземпляров процессов. Для них предложен метод трансляции в сети Йенсена, сетевая модель ис следуется в системе CPN Tools. Описана реализация метода трансляции и приведены оценки размера сети.

Эта работа частично поддержана грантом РФФИ № 07-07-00173а.

Препринт 143
В.И. Шелехов
Исчисление вычислимых предикатов

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

Препринт 142
В.А. Непомнящий, Е.В. Бодин, С.О. Веретнов, М.В. Тюрюшкин
Симуляция и верификация статических SDL-спецификаций распределенных систем с помощью промежуточного языка REAL

В настоящей работе описана система SRPV (SDL/REAL Protocol Verifier) для моделирования, анализа и верификации статических SDL-спецификаций коммуникационных протоколов, которая базируется на трансляции языка SDL в язык Basic-REAL (bREAL). Эта система включает: транслятор из языка SDL в язык bREAL, конвертор из языка описания свойств SDL-спецификаций в подъязык логических bREAL-спецификаций, систему моделирования bREAL-спецификаций и систему верификации этих спецификаций. В качестве примера описано применение системы SRPV к анализу и верификации протокола "Касса-Пассажир".




Вы обнаружили ошибку в следующем тексте:
Просто нажмите кнопку "Отправить сообщение об ошибке" для завершения. Вы можете также ввести комментарий (желательно).