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

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

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

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

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

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

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

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

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

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