Статья: Устранение неоднозначностей в расширенных регулярных выражениях с обратными ссылками посредством применения правил переписывания (2024)

Эта статья посвящена использованию метода верификации моделей для точного теста планируемости систем реального времени, выполняющихся на мультипроцессорных платформах. Чтобы использовать этот метод, мы формально описываем системы реального времени с абстрактным планировщиком, используя модели Крипке. Эта формализация содержит термины, достаточные для специализации абстрактного планировщика. Мы иллюстрируем наш подход, явно определяя планировщики, которые учитывают вытеснение/невытеснение задач и глобальный фиксированный приоритет или приоритет ближайшего дедлайна в различных сочетаниях. Свойство безопасности (планируемости) систем реального времени сформулировано с помощью линейной темпоральной логики LTL. Формализация систем реального времени как моделей Крипке и задание свойства безопасности (планируемости) как формулы LTL позволяет свести точный тест планируемости таких систем к задаче верификации моделей. Мы апробируем этот подход к точному тесту планируемости, реализуя на Promela — входном языке инструмента верификации моделей SPIN — нашу формализацию систем реального времени с невытесняющим планировщиком с глобальным фиксированным приоритетом (NP-GFP), вытесняющим планировщиком с глобальным фиксированным приоритетом (P-GFP), невытесняющим планировщиком с приоритетом ближайшего дедлайна (NP-EDF) и вытесняющим планировщиком с приоритетом ближайшего дедлайна (P-EDF). Мы проводим эксперименты в SPIN для доказательства/опровержения свойства безопасности (планируемости), чтобы оценить эффективность нашего подхода. Мы предлагаем эвристическую оценку планируемости системы реального времени на основе доказуемости небезопасности и недоказуемости безопасности системы реального времени при выполнении на мультипроцессорных платформах с числом процессоров, отличающимся на единицу.

Взаимодействие в открытых сетях несёт определённые риски. Для обеспечения информационной безопасности участников сетевого взаимодействия используют криптографические протоколы. Высокие гарантии безопасности могут быть достигнуты в результате их формальной верификации. Распространённым формальным методом верификации криптографических протоколов является метод проверки модели. В работе для проверки модели криптографических протоколов предлагается использовать инструментальное средство TLA+/TLC, широко применяемое на практике в различных прикладных областях. На языке спецификации TLA+ задаётся модель протокола, а также требуемые свойства безопасности в форме инвариантов. Модель протокола описывает его поведение в виде системы переходов, содержащей все возможные состояния модели протокола и переходы между ними. Для проведения автоматической проверки соответствия модели требуемым свойствам задействуется верификатор TLC. Задача верификации криптографических протоколов имеет свою специфику. Настоящее исследование предлагает три приёма моделирования, учитывающих особенности данной задачи и используемого инструментария TLA+/TLC. Первый приём моделирования состоит в замене системы, состоящей из произвольного количества агентов, на трёхагентную систему. Это позволяет упростить модель и уменьшить её пространство состояний. Второй приём связан с представлением передаваемых сообщений в виде иерархической структуры — это даёт возможность вкладывать одни зашифрованные сообщения в другие. Третий приём состоит в оптимизации модели с целью повышения производительности верификатора TLC. Это выполняется путем задания функции, порождающей множество только тех элементов, которые приводят к переходам между состояниями в модели. В итоге предложенные приёмы позволяют упростить модель и снизить время её верификации. Применение результатов демонстрируется на примере простого протокола — протокола Нидхема-Шредера для аутентификации с открытым ключом. После обнаружения верификатором TLC известной уязвимости этого протокола выполняется моделирование и верификация его доработанной версии. Результаты верификации показывают, что новая версия протокола не имеет данной уязвимости.

Процесс-ориентированное программирование — это подход к разработке управляющего программного обеспечения, в котором программа определяется как набор взаимодействующих процессов. PoST — это процесс-ориентированный язык, который является расширением языка ST из стандарта IEC 61131-3. В области разработки управляющего программного обеспечения формальная верификация играет важную роль вследствие необходимости обеспечения высокой надежности такого программного обеспечения. Дедуктивная верификация — это метод формальной верификации, в котором программа и требования к ней представляются в виде логических формул, а для доказательства того, что программа удовлетворяет требованиям, используется логический вывод. К управляющему программному обеспечению часто предъявляются темпоральные требования. Мы формализуем такие требования для процесс-ориентированных программ в виде инвариантов цикла управления. Но инварианты цикла управления, представляющие требования, недостаточны для доказательства корректности программы. Поэтому мы добавляем дополнительные инварианты, которые содержат вспомогательную информацию. В данной статье рассматривается проблема автоматизации дедуктивной верификации процесс-ориентированных программ. Предложен подход, в котором темпоральные требования задаются с использованием шаблонов требований, которые строятся из базовых шаблонов. Для каждого шаблона требований определяются соответствующий шаблон дополнительных инвариантов и леммы. В статье описан предлагаемый подход и схемы базовых и производных шаблонов требований. Рассмотрены схемы базовых шаблонов дополнительных инвариантов, схемы лемм, определяемых для базовых шаблонов, а также набор базовых шаблонов и леммы для них. Определены схема производных шаблонов дополнительных инвариантов и схемы лемм, определяемых для производных шаблонов. Представлены алгоритмы построения производных шаблонов дополнительных инвариантов и лемм для них, а также метод доказательства этих лемм. Рассмотрены схемы доказательства условий корректности. Предложенный подход демонстрируется на примере. Также проведен анализ связанных работ.

Статья посвящена задаче определения тональности по отношению к аспектам социально-экономического развития в предложениях на русском языке. Аспект, отношение к которому определяется, может как упоминаться явно, так и подразумеваться. Авторами были исследованы возможности применения нейросетевых классификаторов, а также предложен алгоритм определения тональности по отношению к аспекту, основанный на семантических правилах, реализованных с использованием деревьев синтаксических единиц. Тональность по отношению к аспекту определяется в два этапа. На первом этапе в предложении отыскиваются аспектные термины — явно упоминаемые события или явления, связанные с аспектом. На втором этапе тональность по отношению к аспекту определяется как тональность по отношению к аспектному термину, который теснее всего связан с аспектом. В работе предлагается несколько методов поиска аспектных терминов. Качество оценивалось на корпусе из 468 предложений, извлечённых из материалов предвыборной агитации. Лучший результат для нейросетевых классификаторов был получен с использованием нейронной сети BERT-SPC, предобученной на задаче определения тональности по отношению к явно упоминаемому аспекту, макро-F-мера составила 0.74. Лучший результат для алгоритма, основанного на семантических правилах, был получен при использовании метода поиска аспектных терминов на основе семантической схожести, макро-F-мера составила 0.63. При объединении BERT-SPC и алгоритма, основанного на правилах, в ансамбль была получена макро-F-мера, равная 0.79, что является лучшим результатом, полученным в рамках работы.