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

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

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

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

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

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