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

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

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

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

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

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

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

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