Публикации

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

Препринт 89

В.Е. Козюра, В.А. Непомнящий, Р.М. Новиков

Верификация раскрашенных сетей петри методом проверки моделей

Для раскрашенных сетей Петри, ограниченных системами с конечным числом состояний, свойства которых представлены в мю-исчислении, разработана и реализована система верификации PNV (Petri net verifier), базирующаяся на методе проверки моделей. Наряду с описанием системы PNV в работе представлены эксперименты по верификации раскрашенных сетей Петри, моделирующих битовый и кольцевой коммуникационные протоколы, а также обедающих философов.

Препринт 88

М.Ф. Мурзина

О продолжении геодезических в графах кэли некоторых групп

Граф Кэли — одна из классических моделей для представления алгебраических групп. В данной работе изучается проблема продолжения кратчайших путей (геодезических) в графах Кэли некоторых гиперболических групп и групп целых чисел по сложению. Дается характеризация тупиковых вершин (вершин, из которых нет выхода по ребру с увеличением длины) в рассмотренных графах Кэли.

Препринт 87

В.А. Непомнящий, И.С. Ануреев, И.Н. Михайлов, А.В. Промский

На пути к верификации c-программ. Часть 2. Язык c-light-kernel и его аксиоматическая семантика

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

Препринт 86

Д.Ф. Семич

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

В работе описаны математическая модель и пример реализации низкобитрейтного видеокодека. Эта модель отличается от существующих тем, что при битрейте в 1 Мбит/с качество получаемого видео сравнимо с выдаваемым MPEG2 при битрейте 3.5 Мбит/с.

Препринт 85

А.А. Яковлев

Свободно распространяемые операционные системы. анализ текущего состояния в области свободно распространяемого ПО

Работа представляет собой обзор текущего положения в области развития свободно распространяемого ПО. Речь идет в основном об операционных системах и продуктах разработанных, а также поставляемых для этих систем Фондом Свободно распространяемого программного обеспечения, возглавляемого Ричардом Столлманом. Рассматриваемые операционные системы и программное обеспечение базируются на системе UNIX. Целью работы было сформировать объективную точку зрения на перспективы развития свободно распространяемого программного обеспечения и его способность к конкуренции с подобными коммерческими продуктами, защищенными авторскими правами. Были рассмотрены примеры тестов, результаты которых основаны на весьма поверхностном обозрении таких операционных систем, как Linux Red Hat 5.0/5.2, Free BSD 2.2.6/3.0, Solaris 7, UnixWare 7. Исследованы такие характеристики, как процесс инсталляции, интерфейс пользователя, языковая поддержка, вопросы безопасности, а также рассмотрено отдельно взятое ПО (Web-сервер Apache, компилятор GCC и т.п.) и оформление документации. В приложении представлен список утилит и программ представленных в рамках проекта GNU и др. и поставляемых вместе с дистрибутивами операционных систем.

Препринт 84

В.А. Непомнящий, И.С. Ануреев, И.Н. Михайлов, А.В. Промский

На пути к верификации с-программ. Часть 1. Язык c-light

Описано ориентированное на верификацию представительное подмножество языка C - язык C-light. Этот язык допускает детерминированные выражения, ограниченное использование операторов switch и goto, а вместо библиотечных функций для работы с динамической памятью включает операции new и delete языка C++. Для языка C-light представлена структурная операционная семантика в стиле Плоткина. Предполагается использование языка C-light в качестве входного языка системы верификации программ.

Препринт 81

С.И. Катков

Система параллельного программирования суперпаскаль: язык, транслятор, отладчик

Система параллельного программирования, разработанная для языка СуперПаскаль, предназначена для отладки параллельных алгоритмов на последовательных персональных машинах. Ее рекомендуется использовать для обучения параллельному программированию, создания и отладки параллельных алгоритмов.