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

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

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

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

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

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

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

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

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

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