В статье описан метод верификации семейств распределенных систем, порожденных контекстно-зависимой грамматикой специального вида. Этот метод основан на технике проверки моделей и абстракции. Репрезентативная модель зависит от грамматики, определяющей семейство систем. Эта модель симулирует поведение всех систем семейства таким образом, что свойства, выполнимые в репрезентативной модели, выполняются так же и в этих системах. Показано использование предложенного метода для верификации некоторых свойств мультиагентой системы разрешения контекстно-зависимых неоднозначностей в рамках пополнения онтологий.
При разработке требований к поведению распределенных программных систем инженер должен мысленно упорядочивать и определять последовательности событий. Из-за чередования процессов количество возможных последовательностей растет экспоненциально, поэтому разработка таких требований становится нетривиальным занятием. Как следствие, инженеры ограничиваются составлением очень простых требований, которых зачастую бывает недостаточно, чтобы выразить желаемые свойства системы.
В работе рассматривается расширение в линейной темпоральной логике известного и часто используемого на практике темпорального отношения leads-to (по событию--запросу когда-нибудь в будущем будет событие--отклик) на последовательность событий при помощи методики составления контекстных требований.
Основным результатом данной работы является построение формальных требований к системе управления энергоснабжением судна на основе данной методики. Формальная верификация этих требований методом проверки модели позволила выявить несколько ошибок в поведении системы, допущенных при ее проектировании, 3 из которых оказались критическими.
В статье представлена процедура построения параллельной композиции временных автоматов с использованием BALM-II и предложены различные подходы к получению линейных функций, задающих задержки выходов. Наше исследование включает три этапа: на первом этапе мы рассматриваем композицию временных автоматов, временные задержки выходов в которых это натуральное число или ноль; на втором этапе добавляются переходы по таймаутам; на третьем этапе рассматривается композиция временных автоматов в общем случае (когда задержки выходов задаются при помощи множества линейных функций). Данная работа посвящена только первому этапу нашего исследования.
Статья посвящена вопросам спецификации структуры и поведения программных библиотек. Описываются существующие проблемы спецификации библиотек. Дается краткий обзор состояния дел в области формализации спецификации библиотек и библиотечных функций. Формулируются требования к создаваемому формализму. На основе требований предлагается формализм, позволяющий специфицировать все необходимые свойства библиотек, требуемые для автоматизации нескольких классов задач: обнаружение дефектов в программном обеспечении, миграция приложений в новое окружение, генерация программной документации. В заключении определяются дальнейшие направления исследований.