Публикации

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

Препринт 159

Ю.Г. Платонов

Анализ требований к системе «Электронный документооборот» на предприятии с повышенной степенью ответственности за конечный продукт и возможности использования для этих нужд современных информационных систем

В работе рассмотрены проблемы разработки информационной системы «Электронный документооборот» как подсистемы информационного комплекса, предназначенного для предприятия с повышенной степенью ответственности за конечный продукт. Подсистема «Электронный документооборот» должна обеспечивать высокий уровень защиты данных при широком спектре функциональных возможностей, в связи с чем представляет особый интерес для исследователя. В качестве предприятия – потенциального заказчика системы рассматривается ОАО ИСС им. Решетнева (г. Железногорск), занимающееся разработкой бортового программного обеспечения для космических спутников.

Автор формулирует требования к подсистеме «Электронный документооборот» и проводит анализ ряда существующих программных продуктов на предмет их дальнейшего использования в качестве этой подсистемы. Исходя из особенностей существующих систем электронного документооборота в свете требований, обусловленных спецификой предприятия- заказчика, автор делает вывод о необходимости проведения ряда научных изысканий для разработки собственного программного продукта.

Препринт 158

И.С. Ануреев

Язык Atoment: стандартная библиотека

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

Препринт 157

И.С. Ануреев

Язык Atoment: синтаксис и семантика

Язык Atoment является предметно-ориентированным языком разработки методов верификации программ. Он используется в мультиязыковой программной системе ускоренной разработки и апробации методов и техник верификации Спектр. Удобный специализированный язык позволяет пользователю системы описывать в естественной нотации методы и техники верификации, верифицировать алгоритмы в различных предметных областях, добавляя при необходимости свои языки для их представления, разделять методы и техники верификации с другими пользователями системы и комбинировать их. В работе представлены синтаксис и семантика языка Atoment.

Препринт 156

В.А. Непомнящий, Е.В. Бодин, С.О. Веретнов

Моделирование и верификация распределённых систем, представленных на языке SDL, с помощью языка Dynamic-REAL

В настоящей работе описан программный комплекс SRDSV (SDL/REAL Distributed Systems Verifier) для моделирования, анализа и верификации SDL-спецификаций распределенных систем. Этот комплекс включает транслятор из языка SDL в язык Dynamic-REAL (dREAL), систему автоматического моделирования dREAL-спецификаций и две системы верификации этих спецификаций методом проверки моделей, одна из которых использует известную систему SPIN. Описано применение комплекса SRDSV для анализа и верификации динамической системы управления сетью касс-терминалов.

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

Препринт 155

И.В. Марьясов

Применение смешанной аксиоматической семантики языка С-kernel к верификации программы топологической сортировки

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

Препринт 154

В.И. Шелехов

Разработка эффективных программ стандартных функций FLOOR, ISQRT и ILOG2 по технологии предикатного программирования

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

Препринт 153

Н.С. Карнаухов, Д.Ю. Першин, В.И. Шелехов

Язык предикатного программирования P

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