Системная Информатика, № 8

Скачать

Метод верификации семейства мультиагентных систем разрешения неоднозначности

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

Верификация промышленных алгоритмов управления методом Model checking в сочетании с концепцией виртуальных объектов управления

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

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

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

Использование BALM-II для построения параллельной композиции временных автоматов с задержками выходов и таймаутами: сообщение о ходе исследования

В статье представлена процедура построения параллельной композиции временных автоматов с использованием BALM-II и предложены различные подходы к получению линейных функций, задающих задержки выходов. Наше исследование включает три этапа: на первом этапе мы рассматриваем композицию временных автоматов, временные задержки выходов в которых это натуральное число или ноль; на втором этапе добавляются...
Скачать

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

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

Формализмы для концептуального проектирования информационных систем

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