В статье решается задача верификации разливов нефти на водных поверхностях рек, морей и океанов по оптическим аэрофотоснимкам с использованием методов глубокого обучения. Особенностью данной задачи является наличие визуально похожих на разливы нефти областей на водных поверхностях, вызванных цветением водорослей, веществ, не приносящих экологический ущерб (например, пальмовое масло), бликов при съемке или природных явлений (так называемые «двойники»). Многие исследования в данной области основаны на анализе изображений, полученных от радаров с синтезированной апертурой (Synthetic Aperture Radar (SAR) images), которые не обеспечивают точной классификации и сегментации. Последующая верификация способствует сокращению экологического и материального ущерба, а мониторинг размеров площади нефтяного пятна используется для принятия дальнейших решений по устранению последствий. Предлагается новый подход к верификации оптических снимков как задачи бинарной классификации на основе сиамской сети, когда фрагмент исходного изображения многократно сравнивается с репрезентативными примерами из класса нефтяных пятен на водных поверхностях. Основой сиамской сети служит облегченная сеть VGG16. При превышении порогового значения выходной функции принимается решение о наличии разлива нефти. Для обучения сети был собран и размечен собственный набор данных из открытых интернет-ресурсов. Существенной проблемой является несбалансированность выборки данных по классам, что потребовало применения методов аугментации, основанных не только на геометрических и цветовых манипуляциях, но и на основе генеративной состязательной сети (Generative Adversarial Network, GAN). Эксперименты показали, что точность классификации разливов нефти и «двойников» на тестовой выборке достигает значений 0,91 и 0,834 соответственно. Далее решается дополнительная задача семантической сегментации нефтяного пятна с применением сверточных нейронных сетей (СНС) типа кодировщик-декодировщик. Для сегментации исследовались три архитектуры глубоких сетей, а именно U-Net, SegNet и Poly-YOLOv3. Лучшие результаты показала сеть Poly-YOLOv3, достигнув точности 0,97 при среднем времени обработки снимка 385 с веб-сервисом Google Colab. Также была спроектирована база данных для хранения исходных и верифицированных изображений с проблемными областями.
Описывается подход к статической верификации исполняемых программ на основе сопоставления семантических аспектов вычислений, позволяющий построить паспорт программы. Паспорт, как результат статической верификации, может быть использован для создания среды контролируемого выполнения программ (динамической верификации реально выполняемых программ, прошедших статическую верификацию).
В статье описывается подход к верификации правил фильтрации межсетевого экрана, в том числе представляются модели, алгоритмы и разработанный программный прототип, предназначенные для обнаружения аномалий фильтрации в спецификации политики безопасности компьютерной сети. Предлагаемый подход основан на применении метода ―проверки на модели‖ (Model Checking) и позволяет использовать темпоральную логику для спецификации и анализа информационных процессов, протекающих в модели компьютерной сети c функционирующей системой безопасности, которые изменяются во времени и могут нарушить такие свойства безопасности, как конфиденциальность и доступность.
В настоящей статье анализируются существующие подходы к верификации протоколов безопасности и демонстрируется невозможность полноценной верификации протоколов безопасности в рамках только одного из подходов. Для решения данной задачи предлагается комбинированный подход к верификации, основанный на объединении сильных сторон существующих методов и средств.
Рассматриваются задачи выработки рекомендаций в сфере бюджетно-налоговой и торговой политики по противодействию экономическим санкциям на уровне как отдельных стран, подвергшихся таким санкциям, так и на уровне экономического союза, включающего такие страны. Исследования проведены на базе разработанной динамической многоотраслевой и многострановой вычислимой модели общего равновесия, которая описывает функционирование экономик девяти регионов планеты, включая пять стран Евразийского Экономического Союза. Исходные данные модели содержат построенные наборы согласованных матриц социальных счетов для исторического и прогнозного периодов на основе данных: базы Global Trade Analysis Project, национальных таблиц затраты-выпуск, международной торговли и данных Международного валютного фонда (включая прогнозные) по основным макроэкономическим показателям регионов. Получены результаты влияния на макроэкономические и отраслевые показатели стран Евразийского Экономического Союза и других регионов гипотетического сценария, предусматривающего введение с 2019 года дополнительных экономических санкций в отношении России со стороны некоторых регионов. Предлагается подход решения задач по противодействию политике санкций на базе теории параметрического регулирования путем постановки и решения ряда задач динамической оптимизации по определению оптимальных значений соответствующих инструментов бюджетно-налоговой и торговой политики на уровне отдельных стран Евразийского Экономического Союза и в целом. Результаты расчетов на базе модели протестированы на возможность их практического применения с помощью трех подходов, включая оценку устойчивости отображений значений экзогенных параметров откалиброванной модели в значения ее эндогенных переменных. Приведенные результаты демонстрируют для каждой страны Евразийского Экономического Союза большую эффективность применения согласованной экономической политики по противодействию санкциям, по сравнению с проведением такой политики отдельно на уровне этой страны.
Данная статья посвящена отбору и оценке речевых признаков, используемых в задаче автоматической текстонезависимой верификации диктора. Для решения поставленной задачи была использована система верификации диктора, основанная на модели Гауссовых смесей и универсальной фоновой модели (GMM-UBM система).
Рассмотрены область применения и проблемы современных систем автоматической идентификации диктора. Произведен обзор современных методов идентификации диктора, основных речевых признаков, используемых при решении задачи идентификации диктора, а также рассмотрен процесс извлечения признаков, использованных далее. К рассмотренным признакам относятся мел-кепстральные коэффициенты (MFCC), пары линейного спектра (LSP), кепстральные коэффициенты перцептивного линейного предсказания (PLP), кратковременная энергия, формантные частоты, частота основного тона, вероятность вокализации (voicing probability), частота пересечения нуля (ZCR), джиттер и шиммер.
Произведена экспериментальная оценка GMM-UBM системы с применением различных наборов речевых признаков на речевом корпусе, включающем в себя записи 50 дикторов. Признаки отобраны с помощью генетического алгоритма и алгоритма жадного добавления-удаления.
Используя 256-компонентные Гауссовы смеси и полученный вектор из 28 признаков, была получена равная ошибка 1-го и 2-го рода (EER), составляющая 0,579 %. По сравнению со стандартным вектором, состоящим из 14 мел-кепстральных коэффициентов, ошибка EER была уменьшена на 42,1 %.
В статье описывается общая архитектура системы верификации правил фильтрации межсетевого экрана, а также рассматриваются аспекты программной реали- зации этой системы. Реализация выполнена на основе применения метода «проверки на модели» (Model Checking). В качестве верификатора используется программная система SPIN. Также был разработан пользовательский интерфейс, который позволяет загружать данные о верифицируемой системе, правила политики фильтрации, управлять процессом верификации, а также в удобном виде представлять ее результаты. Кроме того, в предлагаемой системе реализована возможность применения различных стратегий разрешения аномалий.
В работе описываются разработанные авторами инструментальные средства и комплексный подход на их основе, при котором методы и средства анализа и верификации обеспечены для представителей всех четырех основных классов языков, на которых обычно описываются телекоммуникационные приложения: языки выполняемых спецификаций общего назначения (SDL), языки для описания и анализа укрупненных образцов поведения и выявления зависимостей между ними в сложных системах (UCM), специализированные языки, ориентированные на верификацию спецификаций телекоммуникационных систем (язык интерпретированных MSC диаграмм, язык взаимодействующих конечных автоматов, язык Dynamic-REAL) и индустриальные императивные языки (C/С++). Верификация спецификаций дополняется автоматизированным построением тестовых наборов, обеспечивающих заданную степень покрытия исходных поведенческих требований, причем эти тестовые наборы оптимизированы по заданным критериям производительности. Исполнение тестов происходит в среде автоматизированного тестирования на моделях систем, либо непосредственно на их реализациях, погруженных в соответствующие программные оболочки, обеспечивающие взаимодействие тестируемой системы с тестовым окружением. Тестовая оболочка позволяет одновременно с прогоном тестов проводить автоматизированный анализ результатов тестирования.
Предлагается метод машинного обучения, основанный на совместном применении генетического программирования и верификации моделей для построения автоматов управления системами со сложным поведением на основе обучающих примеров. Приводится описание структуры хромосом, генетического алгоритма, операций мутации и скрещивания. Изложены результаты экспериментального исследования на задаче построения конечного автомата управления дверьми лифта.
1 - 10 из 10 результатов