Статья: Методы определения тональности по отношению к аспектам социально-экономического развития в предложениях на русском языке (2024)

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

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

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

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