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

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

Модели мандатного контроля целостности в операционных системах, как правило, накладывают ограничения на доступы активных компонент системы к пассивным и представляют эти доступы непосредственно. Такое представление можно использовать в случае операционных систем с монолитной архитектурой, где части системы, обеспечивающие доступ к ресурсам, входят в доверенную вычислительную базу. Однако доказательство отсутствия ошибок в таких компонентах и, следовательно, соответствия такой модели реальной системе является чрезвычайно трудной задачей. KasperskyOS – операционная система, основанная на микроядре и позволяющая организовать доступ к ресурсам с помощью компонентов, не обязательно входящих в доверенную вычислительную базу. Для KasperskyOS была разработана и реализована модель мандатного контроля целостности, учитывающая наличие таких компонентов и возможность их некорректного функционирования. В данной статье представлен процесс формализации этой модели и автоматизированного доказательства свойств, обеспечиваемых моделью. Описана разработка модели на языке Event-B и отражен опыт ее верификации с использованием платформы Rodin.

Текущий стандарт надежного программного обеспечения для бортовых контроллеров – это многораздельная операционная система реального времени, которая способна реагировать на события от устройств с ожидаемой скоростью, а также делить процессорное время и память между изолированными разделами. Верификация на основе модели – это метод формальной проверки программного обеспечения, при котором разрабатывается программная модель, а затем она автоматически проверяется на соответствие формальным требованиям. Этот метод позволяет доказать правильность работы модели на всех возможных входных данных, всех возможных способов переключения процессов и взаимодействий. В этой статье описывается формализованная модель открытой многораздельной операционной системы POK, реализованная на языке Promela средства SPIN для формальной верификации методом Model Checking и предназначенная для моделирования поведения: планировщика разделов и процессов; системных вызовов через программное прерывание; библиотеки ядра для работы с примитивами синхронизации и ожиданием процессов; пользовательский код, осуществляющий работу нескольких процессов в разных разделах, которые синхронизируются через семафоры. Данный подход может быть использован для проверки корректности синхронизации, работы алгоритмов планировщика, корректного доступа к данным из разных разделов путем задания соответствующих требований в виде формул темпоральной логики линейного времени.

Эргодичность систем характеризуется сохранением стационарности распределения состояний. Для компьютерных систем важно не допустить деградацию свойств системы со временем. Эргодичность особенно необходима для критически важных систем в ответственных отраслях. Разработка ПО на основе требований функциональной безопасности стандарта МЭК 60880 категории A реализуется только на вновь создаваемом ПО, отвечающим данным, наиболее жестким требованиям для АЭС, при невозможности использовать стандартные ОС и компиляторы. Для данных целей был реализован прототип среды исполнения и прикладного ПО дисплейной системы командного управления (ДСКУ). Среда исполнения (рантайм) создавалась на основе Active Oberon системы A2. A2 представляет собой однопользовательскую многозадачную систему. Область применения – промышленные встроенные системы реального времени, системы повышенной надежности. Среда исполнения ДСКУ реализована существенной переработкой минимального подмножества A2 для обеспечения требований стандарта. Система ограничений, формируемая по требованиям стандарта, дает возможность создавать компьютерные системы с новыми свойствами. Использование данных ограничений приводит к доказательству отсутствия возможности появления вызываемых ими сбоев и позволяет рассматривать компьютерную систему исходя из презумпции неэргодичности.

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

В работе описывается внутрипроцедурный анализ отдельных функций, использующийся в инструменте статического поиска ошибок Svace. Отличительные особенности анализа: анализ по графу потока управления, символьное выполнение с объединением состояний анализа в точках слияния путей, анализ только части путей в функциях с циклами, одновременный запуск всех анализаторов, моделирование достижимых ячеек памяти, нумерация значений переменных.

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

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

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

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

Сети Петри с временными дугами – это временное расширение сетей Петри (TaPN-сети), которое позволяет присваивать таймеры фишкам. Система динамических точек на метрическом графе (DP-система) это другая динамическая модель, которая рассматривается в теории геометрических дискретных динамических систем и, исторически, ее изучение мотивировано изучением распространения локализованных гауссовых волновых пакетов по тонким структурам; кроме того, DP-системы могут использоваться для приближенного представления динамики распространения сообщений в распределенных системах. В этой работе, мы описываем новый подход для автоматического анализа DP-систем используя трансляцию в TaPN сеть, которая реализована как расширение инструмента TAPAAL. Подход позволяет использовать мощные инструменты верификации (TAPAAL/UPPAAL) для анализа динамических характеристик DP-систем, представленных на языке TCTL. В работе продемонстрировано, как можно кодировать временно-темпоральные свойства DP-систем в рамках предложенного подхода, и приведены результаты экспериментальных тестов.

Рассмотрено моделирование технических задач и задач прикладной математики, их алгоритмизация и программирование. Дается характеристика численного моделирования технических задач и прикладной математики: физико-технических экспериментов, энергетических, баллистических и сейсмических методов И.В Курчатова, начиная с математических методов 17-20 вв., первых ЭВМ и компьютеров. Дан анализ первых технических задач и задач прикладной математики, их моделирование, алгоритмизация и программирование с помощью граф-схемного языка А.А.Ляпунова, адресного языка и языков программирования. Представлены численные методы, реализованные под руководством А.А. Дородницына, А.А.Самарского, О.М. Белоцерковского и других ученых на современных суперкомпьютерах. Приведены примеры математического моделирования биологической задачи лечения глаз и предмета «Вычислительной геометрии» в Интернет.

В настоящей работе разрабатывается архитектура решателя, реализующего новую трехмерную математическую модель для описания динамики потоков на склонах с учётом захвата и отложения материала. Также проводится сравнение двух подходов для описания динамики потоков на склонах: с использованием осреднённых по глубине уравнений механики сплошной среды (уравнений типа мелкой воды) и с использованием трёхмерного моделирования, основанного на полных, не осреднённых по глубине, уравнениях механики сплошной среды. С применением этих двух подходов проведено моделирование экспериментов по спуску потока в лотке и взаимодействию потока с комплексом заградительных сооружений. Проведено сравнение численных решений с экспериментальными данными. Кроме того, оба подхода применены к расчёту снежной лавины в 22-ом лавинном очаге горы Юкспор (Хибины). Дальность выброса лавины и форма лавинных отложений сравнивалась с натурными данными, полученными по результатам измерения реальной лавины, сошедшей в данном очаге. В процессе численного эксперимента были получены распределения таких величин, как скорость потока, глубина, плотность, молекулярная и турбулентная вязкость, значения плотности турбулентной кинетической энергии, диссипации турбулентной кинетической энергии, значение напряжения сдвига на дне потока. С использованием полученных данных разрабатывается математическая модель для описания захвата потоком материала подстилающей поверхности при её разрушении и отложения материала потока на склон. Для реализации полученной математической модели разработана архитектура решателя multiphaseEulerChangeFoam, реализующего трёхфазную многоскоростную модель с фазовыми переходами между материалом подстилающей поверхности и материалом движущегося потока. В качестве основы для разрабатываемого решателя взят классический решатель multiphaseEulerFoam из пакета OpenFOAM.

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