Толерантный синтаксический анализ позволяет найти области программы, представляющие интерес в контексте конкретной задачи, и извлечь информацию об их структуре. В то время как эти области должны быть подробно описаны в грамматике языка, другие части программы могут быть не описаны совсем или описаны менее детально, при этом генерируемый парсер должен признавать корректными все возможные вариации программы в нерелевантных областях, то есть, должен быть толерантным по отношению к ним. Островные грамматики - один из основных способов реализации толерантного парсинга. Термином «остров» обозначаются релевантные области кода, термином «вода» - нерелевантный код. В настоящей работе описывается модифицированный LL(1) алгоритм со встроенной обработкой специального символа «Any», позволяющего сопоставлять последовательности токенов, не описанные разработчиком грамматики в явном виде. Применение данного алгоритма к островным грамматикам ведёт к сокращению описания воды и упрощению описания островов. Наша реализация «Any» является более безопасной для использования и менее ограничительной по сравнению с ближайшими аналогами в генераторах Coco/R и LightParse. Также она более предсказуема и требует меньших накладных расходов в сравнении с концепцией «ограниченных морей», внедрённой в PetitParser. На базе алгоритма реализован генератор компиляторов со встроенным языком описания островных грамматик. Как показано в разделе экспериментов, сгенерированный по островной грамматике языка C# толерантный парсер может быть успешно применён для анализа крупных промышленных проектов.

Специализация - это оптимизация программ на основе использования наперёд заданной информации о значении части переменных. Методы специализации программ развиваются с 1970-х годов (смешанные вычисления, частичные вычисления, суперкомпиляция). Однако удивительно, что после трёх десятилетий разработанные специализаторы до сих пор не достигли того уровня, когда они станут пригодны для широкого практического применения. Возникает вопрос: в чём же причина? Наша гипотеза состоит в том, что задача специализации требуют гораздо большего участия человека в управлении процессом специализации, анализе результатов, проведении компьютерных экспериментов, чем в случае обычной оптимизации программы в компиляторах. Требуется погружение специализаторов в привычные для программистов интегрированные среды разработки, включая создание соответствующих диалоговых средств. В данной статье описываются результаты разработки и реализации методов интерактивной специализации на основе частичных вычислений для подмножества языка Java. Реализация выполнена в рамках популярной среды разработки (IDE) Eclipse. Разрабатываются сценарии человеко-машинного диалога с подсистемой специализации, интерактивные средства для составления задания на специализацию и управление процессом специализации. Приводится пример успешного применения разработанного специализатора. Остаточная программа работает в несколько раз быстрее чем исходная.

Встраиваемые системы с гетерогенной архитектурой, рассматриваемые в данной работе, состоят из одного управляющего и одного или нескольких периферийных процессоров. Разработка ПО для таких систем представляет заметные сложности, требуя различные наборы инструментов для каждой составляющей гетерогенной системы. Достижение высокой эффективности также становится более сложной задачей. Кроме того, во многих сценариях встраиваемые системы требуют настройки во время исполнения, что непросто обеспечить с использованием стандартных средств. Эта работа представляет C-подобный предметно-ориентированный язык (DSL) для метапрограммирования и библиотеку, предоставляющую единый интерфейс для программирования периферийных процессоров с использованием этого языка. Это позволяет разрешить упомянутые проблемы. DSL встроен в C++ и позволяет свободно манипулировать написанными на нем выражениями и, таким образом, представляет собой реализацию идеи генеративного программирования, когда выразительная мощь высокоуровневого языка используется для многоступенчатой генерации низкоуровневого DSL кода. Вместе с другими возможностями, например, обобщенными DSL функциями, это делает данный язык гибким инструментом для динамической кодогенерации. Подход, используемый в библиотеке, - это динамическая компиляция. Код, написанный на предметно-ориентированном языке, транслируется в LLVM IR и затем компилируется в машинный код во время исполнения. Это открывает возможность динамических оптимизаций кода, например, специализации функций для определенных значений, известных только во время исполнения. Гибкая архитектура библиотеки обеспечивает простую расширяемость на любые платформы, поддерживаемые LLVM. В конце работы также приводятся апробация библиотеки на нескольких системах и демонстрация возможности динамических оптимизаций.

На сегодняшний день в авиационной отрасли существует актуальная проблема - как инструментально поддержать и обеспечить сертифицируемость разработки критичных по безопасности сложных систем в соответствии с международными и отечественными отраслевыми стандартами, нормативными документами, такими как КТ-178С, КТ-254, Р-4754, Р 4761 и др. В статье рассматривается процесс управления конфигурацией при разработке по КТ-178С как основной источник критериев для осуществления выбора инструментального средства поддержки разработки. Выделенные критерии могут быть применены к инструменту поддержки всего жизненного цикла разработки авиационного ПО в соответствии с КТ-178С, а также к инструментам, отвечающим за поддержку отдельных процессов жизненного цикла. Мероприятия процесса управления конфигурацией обеспечивают работу с данными жизненного цикла, их хранение, целостность, безопасность, управляемость, информационную поддержку обмена данными между остальными процессами жизненного цикла, ведение истории изменений и т.п. Соблюдение принципов процесса управления конфигурацией позволяет осуществлять контроль разработки, обеспечить требуемые качество и надежность продукта, его сертифицируемость и необходимый уровень доверия к безопасности, снизить финансовые и временные затраты на разработку. В качестве примера использования критериев приведен анализ одного из распространенных в отрасли инструментов разработки и управления требованиями на соответствие указанным критериям.

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

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

Верификация и анализ распределенных систем являются чрезвычайно важными задачами, особенно сейчас, когда многие компьютерные системы реализуют критически важные сервисы. Для моделирования и верификации систем полезно сочетать разные методы анализа. В частности, это позволяет применять тот формализм и ту технику анализа, которые лучше подходят для того или иного компонента системы. Комбинация из раскрашенных сетей Петри (CPN, Coloured Petri Nets) и конечных автоматов представляет собой успешную формальную методику моделирования и верификации распределенных систем. В связи с этим в данной статье рассматривается инструмент Prosega/CPN (Protocol Sequence Generator and Analyzer), расширение CPN Tools для поддержки автоматного анализа и верификации. Инструмент реализует несколько функций, таких как генерация минимизированного детерминированного конечного автомата из графа достижимости (occurrence graph) раскрашенной сети Петри, генерация языка и сопоставление конечных автоматов. Это решение поддерживается функцией Simulator Extensions, развитие которой обусловлено необходимостью интеграции раскрашенных сетей Петри с другими формализмами. Инструмент предназначен для поддержки формальной методологии верификации коммуникационных протоколов; однако он может использоваться для верификации других систем, анализ которых включает сравнение моделей на разных уровнях абстракции, например, бизнес-стратегий и бизнес-процессов. В статье приведен подробный пример, в котором инструмент Prosega/CPN используется для анализа части спецификации службы управления соединениями MAC IEEE 802.16.

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

Конечные автоматы широко используются при построении проверяющих тестов для управляющих систем с гарантированной полнотой обнаружения неисправностей. В ряде случаев такие тесты достигают экспоненциальной длины относительно размеров автомата-спецификации, что мотивирует исследования по оптимизации проверяющих тестов. Существование последовательностей, различающих каждую пару состояний в автомате-спецификации, может существенно сократить длину теста, если такие последовательности достаточно короткие. Более того, при описании современных систем часто приходится учитывать опциональность неформальной спецификации, и соответственно, использовать методы синтеза тестов для недетерминированных автоматов; последнее в большинстве случаев повышает длину тестов. Адаптивные различающие последовательности существуют чаще, чем безусловные, и, как правило, имеют меньшую длину, что делает их выбор более предпочтительным для синтеза тестов. В настоящей работе мы исследуем свойства адаптивных различающих последовательностей и оптимизируем метод построения таковых для полностью определённых, возможно, недетерминированных конечных автоматов. Предложенный подход основан на ограничении размеров различающего автомата, по которому строится различающий тестовый пример, служащий удобной формой представления адаптивной различающей последовательности. Проведённые эксперименты позволили оценить длину и вероятность существования адаптивных различающих последовательностей для случайно сгенерированных автоматов с различной степенью недетерминизма. Также в работе рассмотрен специальный класс так называемых автоматов без слияний, которые описывают широкий класс реальных систем и обладают «хорошими» для синтеза тестов свойствами; в частности, для таких автоматов практически всегда существуют адаптивные различающие последовательности, если для каждой пары «состояние, входной символ» существует не более трех различных переходов, т.е. степень недетерминизма в автомате не больше трех.

Системы электронного голосования являются будущей альтернативой традиционным способам проведения голосования. Как и для любой системы, важным является верификация ключевых алгоритмов, на которых основана её безопасность. В работе рассматривается анализ безопасности криптографического протокола на этапе регистрации, который используется в созданной авторами системе электронного голосования на основе слепых посредников. Проведено описание протокола регистрации, показаны передаваемые между сторонами сообщения и объяснено их содержимое. При моделировании протоколов предполагается использование модели угроз Долева-Яо. В качестве инструмента для анализа безопасности выбранного протокола используется система Avispa. Протокол описан на языке CAS+ и впоследствии транслирован в специальный язык HLPSL (High-Level Protocol Specification Language), с которым работает используемый инструмент. Описание протокола включает в себя роли, данные, ключи шифрования, порядок передаваемых сообщений между сторонами, знание сторон и злоумышленника, цели проверки. Поставлены цели верификации криптографического протокола на устойчивость к атакам на аутентификацию, секретность и replay-атакам. Установлены данные, которыми может владеть потенциальный злоумышленник. Произведен анализ безопасности протокола регистрации. Анализ показал, что выдвинутые цели проверки были достигнуты. Отображена подробная схема передачи сообщений и их содержимого при наличии злоумышленника, осуществляющего MITM-атаку (Man in the middle). Показана эффективность защиты протокола от действий злоумышленника.

Данная статья описывает текущие исследования по теме автоматической калибровки и синхронизации камеры и МЭМС-датчиков. Результаты исследования применимы к любой системе, имеющей камеру и МЭМС-датчики, примером которых является гироскоп. Основная задача нашего исследования - нахождение таких параметров системы камера-датчики, как фокусное расстояние камеры и разница во времени между считыванием показания датчика и считыванием кадра камеры, вызванная необходимостью предобработки “сырого” кадра и переводом его в определенный формат. Автоматическая калибровка позволяет применять алгоритмы компьютерного зрения (цифровая видео стабилизация, 3D-реконструкция, сжатие видео, дополненная реальность), использующие кадры видео и показания датчиков, на большем количестве устройств, оснащенными камерой и МЭМС-датчиками. Также автоматическая калибровка позволяет полностью абстрагироваться от характеристик конкретного устройства и разрабатывать алгоритмы, работающие на различных платформах (мобильные платформы, встраиваемые системы, экшн-камеры). Статья описывает общую математическую модель, необходимую для реализации данной функциональности, используя методы компьютерного зрения и показания МЭМС-датчиков. Авторы проводят обзор и сравнение существующих подходов к автоматической калибровке, а также предлагают свои улучшения, повышающие качество существующих алгоритмов.

Извлечение различной значимой медицинской информации из КТ и МРТ снимков - это одна из наиболее важных и трудных задач в сфере анализа медицинских изображений. Недостаток автоматизации в этих задачах становится причиной необходимости скрупулезной обработки данных экспертом, что ведет к возможности ошибок, связанных с человеческим фактором. Несмотря на то, что некоторые из методов решения задач могут быть полуавтоматическими, они все еще опираются на человеческие компетенции. Основной целью наших исследований является создание инструмента, который максимизирует уровень автоматизации в задачах обработки медицинских снимков. Наш проект состоит из двух частей: набор алгоритмов для обработки снимков, а также инструменты для интерпретирования и визуализации результатов. В данной статье мы представляем обзор лучших существующих решений в этой области, а также описание собственных алгоритмов для актуальных проблем, таких как сегментация костных глазных орбит и опухолей мозга, используя сверточные нейронные сети. Представлено исследование эффективности различных моделей нейронных моделей при классификации и сегментации для обеих задач, а также сравнительный анализ различных нейронных ансамблей, применяемых к задаче выделения опухолей головного мозга на медицинских снимках. Также представлено наше программное обеспечение под названием «MISO Tool», которое создано специально для подобного рода задач и позволяет выполнять сегментирование тканей с использованием предварительно обученных поставляемых вместе с ПО нейронных сетей, производить различные манипуляции с пиксельными данными DICOM-изображения, а также получать 3D-реконструкция сегментированных областей.

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

В работе рассмоторены онлайновые алгоритмы для классических задач упаковки Bin Packing и Strip Packing и их обобщений: задач Multidimensional Bin Packing, Multiple Strip Packing и задаче об упаковке в полосы различной ширины. Для последней задачи описан анализ в худшем случае; для остальных задач приведен как анализ в худшем случае, так и анализ в среднем (вероятностный анализ). Рассмотрены лучшие известные нижние и верхние оценки. Приведены основные алгоритмы и описаны методы их анализа.