Требования к программному обеспечению достаточно трудно объективно измерить по критериям качества без вовлечения в процесс оценки непосредственно самих заинтересованных сторон. Оценка качества документов спецификации требований в автоматическом режиме может существенно сократить расходы бюджета проекта и также предотвращает появление скрытых дефектов в программном обеспечении на более поздних этапах разработки. Качество требований может быть оценено, основываясь на широком разнообразии атрибутов качества, но значение каждого такого атрибута достаточно расплывчато и не имеет строгой привязки к какой-либо измеримой метрике. Использование метода GQM (Goal-Question-Metric) в процессе построения модели оценки может помочь выявить наиболее важные критерии качества и установить связь между атрибутами и конкретными метриками, которые могут быть собраны и вычислены автоматически. Текст требований к программному обеспечению, написанный на естественном языке, может быть проанализирован при помощи инструментов NLP (Natural Language Processing) с целью выявления наиболее слабых слов и фраз, которые делают предложения неоднозначными и двусмысленными. Метрики для таких критериев качества как неоднозначность, единственность, субъективность, полнота и удобочитаемость предложены в данной работе. Описанная модель оценки качества была реализована при помощи сторонних инструментов с открытым исходным кодом для требований, написанных на русском языке.
Обоснована и показана на конкретном примере возможность применения технологии машинного обучения для решения задачи анализа проектов с целью поддержки принятия решения об участии в тендере на выполнение проекта. Изложены подходы и показан процесс решения задачи бинарной классификации проектов с использованием библиотек языка Python. Уделено внимание проблеме выбора алгоритма построения функции принадлежности, задаче формирования и анализа исходных данных, оценки точности решения. Показано, что для рассматриваемой задачи наилучшее решение обеспечивает алгоритм логистической регрессии.
Повсеместное использование облачных технологий позволяет оптимизировать экономические издержки на содержание ИТ-инфраструктуры предприятий, но при этом увеличивает вероятность кражи конфиденциальных данных. Одним из механизмов для защиты данных от кражи является криптография. Использование классических примитивов симметричного и ассиметричного шифрования не позволяет обрабатывать данные в зашифрованном виде. Для обработки конфиденциальных данных используют гомоморфное шифрование. Гомоморфное шифрование позволяет производить арифметические действия с зашифрованным текстом и получать зашифрованный результат, который соответствует результату операций, выполненных с открытым текстом. Одним из перспективных направлений для построения гомоморфных шифров является гомоморфные шифры, основанные на обучении с ошибками. В статье мы исследуем криптографические свойства существующих гомоморфных шифров (CKKS, BFV) на основе обучения с ошибками, сравниваем их технические характеристики: криптостойкость и избыточность данных, скорость кодирования и декодирования данных, скорость выполнения арифметических операций сложения и умножения данных, скорость выполнения операции KeySwitching.
Система прерываний является важной частью микропроцессоров. Прерывания широко используются для взаимодействия с оборудованием и реагирования на сигналы. Современные микропроцессорные системы прерываний включают аппаратную поддержку виртуализации. Аппаратная поддержка помогает повысить производительность виртуальных машин. Однако добавление дополнительной функциональности может привести к появлению потенциальных ошибок. В статье представлен обзор подходов, используемых для систем прерывания в многоядерных микропроцессорах с аппаратной поддержкой виртуализации. Описаны некоторые определения и характеристики систем прерываний, которые необходимо учитывать в процессе проверки. Представлена общая схема автономной среды верификации. Universal Verification Methodology была применена для построения тестовой системы. Для упрощения разработки модуля проверки использовалась эталонная модель с учетом временных характеристик. Последовательности первичных запросов и автоматически генерируемые вторичные запросы в специальных модулях авто генерации использовались для рандомизации поведения тестовой системы. Были описаны некоторые трудности, обнаруженные в процессе верификации, а также соответствующие методы их решения. Представлены обобщенные этапы алгоритма тестирования. Были рассмотрены некоторые другие методы проверки корректности работы системы прерываний. В заключение приведены примеры применения предложенных подходов для верификации системы прерываний микропроцессоров с архитектурой Эльбрус и «SPARC-V9», разработанной АО МЦСТ. Представлены результаты и дальнейший план развития тестовой системы.
Производительность современных микропроцессоров существенно зависит от устройства их подсистемы памяти. Таким образом, программная модель подсистемы памяти является ключевым компонентом потактово-точных симуляторов, и качество этой модели в значительной степени определяет итоговую точность моделирования всего микропроцессора. Данная статья посвящена потактово-точному симулятору уровня приложений, специализированного на моделировании микропроцессоров архитектуры «Эльбрус». В статье дано описание общей структуры рассматриваемого потактово-точного симулятора. Вслед за этим описаны программная модель подсистемы памяти и особенности ее интеграции как части потактово-точного симулятора. Далее изложены результаты оценки точности разработанного потактово-точного симулятора на наборе тестов SPEC CPU2006 и проведен анализ ошибок моделирования. Завершает статью сравнение производительности симуляторов микропроцессоров «Эльбрус» различных типов.
Система команд – это стержень, вокруг которого строится весь остальной процессор. Ошибки или негибкость в решениях, однажды заложенные в систему команд, остаются с этим поколением процессоров навсегда. Поэтому одна из ключевых причин, по которой рост производительности современных CPU замедлился, заключается в том, что исходный код процессоров «испортился» в прямом и переносном смысле этого слова: процессоры внутри становятся сложными, из-за чего их дальнейшее развитие затрудняется. Разработка современных ЭВМ (CPU, GPU или специализированных систем) – это крайне дорогостоящий процесс, состоящий из большого количества затратных статей. Поэтому вопрос цены, или, скорее, целесообразности разработки процессора является ключевым. В данной работе мы провели исследование существующих популярных систем команд процессора и сделали выводы о перспективности в настоящее время направления RISC-V и других открытых систем команд CPU. Мы постарались ответить на следующие вопросы: почему система команд процессора – это действительно важно? Почему именно RISC-V, чем он лучше остальных? Какие возможности RISC-V открывает для российских разработчиков и какие у него есть аналоги?
На сегодняшний день трудоемкой и нетривиальной задачей является автоматизация мониторинга дисковых носителей в кластерной инфраструктуре при использовании системы управления контейнерами Kubernetes. В работе рассматриваются существующие подходы к мониторингу дисковых носителей в системе оркестрации контейнеров Kubernetes и приведен их сравнительный анализ. На основе представленного анализа делается вывод о необходимости совершенствования и автоматизации подходов. Для этого в работе предлагается подход автоматизации сбора метрик с дисковых носителей за счет реализации Kubernetes «оператора» для инструмента, с помощью которого можно эффективно получать информацию о состоянии дисковых носителей в системе. В качестве результатов приведены временные характеристики сбора информации о дисках с использованием существующих подходов и предлагаемого подхода. Приведены численных результаты и графики, демонстрирующие выигрыш предлагаемого подхода.
При дедуктивной верификации Си-программ как с помощью различных платформ верификации (Why3, Frama-C/WP, F*), так и с помощью систем интерактивного доказательства теорем (Isabelle, HOL4, Coq) достаточно широко используются SMT-решатели. Их разрешающие алгоритмы полны для некоторых комбинаций логических теорий (логик), в частности для логики QF_UFLIA. В то же время при верификации Си-программ часто необходимо оперировать формулами в других разрешимых логиках, поддерживаемых не всеми SMT-решателями. Типичными примерами таких логик могут служить комбинации QF_UFLIA c теориями ограниченных целых как с переполнением (для беззнаковых целых в Си), так и без переполнения (для знаковых целых), а также теорией конечных интерпретируемых множеств (для поддержки рамочных условий) и др. Одним из возможных способов поддержки таких логик является их непосредственная реализация в SMT-решателях, однако этот способ часто является трудоемким, а также недостаточно гибким и универсальным. Другим способом является реализация пользовательских стратегий инстанцирования кванторов для сведения формул в неподдерживаемых логиках к формулам в широко распространенных разрешимых логиках, таких как QF_UFLIA. В данной статье представлена процедура инстанцирования лемм для трансляции формул в теории ограниченных целых без переполнения в логику QF_UFLIA. Для процедуры трансляции даны доказательства корректности и полноты, а также описана формализация этих доказательств в системе Isabelle/HOL. Аналогичный подход можно использовать для формулирования и доказательства полноты процедур трансляции формул в других теориях, таких как теория ограниченных целых с переполнением и теория ограниченной адресной арифметики.
Модели с конечным числом состояний широко используются при решении задач анализа и синтеза дискретных систем, и минимизация конечных автоматов является известной проблемой оптимизации, которая позволяет уменьшить количество состояний конечного автомата, описывающего поведение дискретной системы, на основе использования его приведенной формы. Такая форма единственна с точностью до изоморфизма для классических конечных автоматов, что, в частности, является основой для соответствующих методов синтеза тестов с гарантированной полнотой относительно «черного ящика», таких как W-метод и его модификации. Поскольку поведение современного программного и аппаратного обеспечения зачастую зависит от временных аспектов, в настоящее время классические автоматы расширяются временной переменной и связанными с ней входными и выходными таймаутами. Существующие подходы к минимизации временных автоматов охватывают оптимизацию как состояний, так и временных аспектов, и позволяют получить единственную минимальную форму для неинициальных детерминированных временных автоматов. В то же время для инициальных временных автоматов, т.е. автоматов с выделенным начальным состоянием, могут существовать различные попарно неизоморфные минимальные формы. В настоящей работе мы определяем классы инициальных временных автоматов, для которых минимальная форма единственна с точностью до изоморфизма.
Теория формальных языков активно изучается и находит широкое применение во многих областях. Например, в биоинформатике в задачах распознавания и классификации иногда требуется найти подпоследовательности генетических цепочек, обладающие некоторыми характерными чертами, которые могут быть описаны с помощью грамматики. Задача поиска этих подпоследовательностей сводится к проверке их принадлежности некоторому формальному языку, заданному грамматикой. При этом часто требуется эффективная обработка больших объёмов данных, что приводит к необходимости усовершенствования существующих методов синтаксического анализа. На данный момент среди алгоритмов синтаксического анализа, работающих с произвольной КС-грамматикой, одним из самых быстрых является алгоритм Валианта, основанный на использовании матричных операций. В данной работе предложен алгоритм, который является модификацией алгоритма Валианта. Его основным достоинством является возможность разбиения матрицы разбора на подслои непересекающихся подматриц, которые могут быть обработаны независимо. Доказана корректность и приведена оценка сложности предложенного алгоритма. Проведенные эксперименты показывают, что он сохранил основные преимущества исходного алгоритма, главное из которых – высокая производительность, полученная за счет использования эффективных методов перемножения матриц. Также предложенный алгоритм позволил заметно уменьшить время, затрачиваемое на поиск подстрок, сократив большое количество избыточных вычислений.
Языково-ориентированный подход становится все более популярным при разработке информационных систем, однако существующие DSM-платформы, реализующие эту парадигму, имеют существенные ограничения, включающие недостаточные выразительные возможности моделей, используемых для реализации редакторов визуальных моделей для сложных предметных областей, и ограниченные возможности для трансформации визуальных моделей. Визуальные языки обычно основаны на графовых моделях, однако используемые типы графов имеют определенные ограничения, такие как недостаточная выразительность, сложность представления моделей большой размерности, а также трудоёмкость выполнения операций. Для создания инструмента, не имеющего описанных выше ограничений, необходима разработка новой формальной модели. HP-графы могут стать решением данной проблемы. Имеется не только возможность создавать новые визуальные языки для различных предметных областей на их основе, но и разработать эффективные алгоритмы для выполнения различных операций над моделями, построенными с использованием этих языков. В статье дано определение HP-графа, а также приведено обоснование выразительной мощности предложенной модели, описаны основные операции для HP-графов. Выбранный графовый формализм объединяет возможности различных типов графов для представления визуальных моделей и позволяет создать на его основе гибкий редактор моделей для DSM-платформы, реализовать эффективные алгоритмы выполнения операций, в частности, трансформации моделей.
Рандомизированное тестирование приложений (фаззинг, фаззинг-тестирование) является одним из широко используемых методов поиска ошибок. Цель фаззинг-тестирования – определить стабильность приложений при обработке псевдослучайно сгенерированных входных данных. В ходе тестирования приложение запускается на множестве произвольных входных данных, которые могут быть недействительными/неожиданными. Современное программное обеспечение часто предоставляет программный интерфейс (Application programming interface) для расширения возможностей программы. Это еще больше усложняет тестирование программного обеспечения, поскольку становится необходимым учитывать все возможные сценарии использования предоставленных интерфейсных функций. Применение фаззинга для генерации разных сценариев использования программного интерфейса приложения и соответствующих входных данных позволяет эффективным образом выявить ошибки в реализации функций программного интерфейса. В данной статье описывается новый метод фаззинг-тестирования для Android приложений и библиотек, написанных на языке Java. Разработанный инструмент фаззинг-тестирования выявил 15 уникальных дефектов, приводящих к аварийному завершению приложения SmartThings, разработанного компанией Samsung.
Авиационная отрасль в Российской Федерации сталкивается с трудностями организации инструментальной поддержки процессов разработки. Активный курс государства в сторону цифровизации экономики не способствует решению данной проблемы. Выбор инструмента является важным критерием успешной разработки сложного сертифицируемого ПО - бортовых авиационных систем. Подобная ситуация наблюдается и в других отраслях промышленности. В настоящее время на российском ИТ-рынке представлено достаточное количество программного обеспечения, способного в различной степени покрыть те или иные процессы жизненного цикла разработки сложного сертифицируемого программного обеспечения в сфере авионики. В рамках данной статьи анализируется текущая ситуация на российском рынке программного обеспечения и влияние политики импортозамещения Российской Федерации на разработчиков программного обеспечения и его потребителей - промышленных предприятий. Детали нормативного документа КТ-178С для разработки бортового программного обеспечения показывают важность выбора инструментальной среды проекта. Авторы определили основные группы функциональных возможностей инструментов, которые обеспечивают поддержку жизненного цикла разработки бортового программного обеспечения. Российские и зарубежные PLM (Product Lifecycle Management) и PDM (Product Data Management) системы, а также другое программное обеспечение были проверены на соответствие необходимой функциональности. Для сравнительного анализа был предложен метод, основанный на аддитивной верификации программного обеспечения по заданным критериям. Результаты исследований позволили авторам сделать вывод о современном уровне российского программного обеспечения в сравнении с зарубежными аналогами. На основании результатов анализа получили обоснование перспективы дальнейшей эволюции российского программного обеспечения. Также результаты анализа позволили сформулировать рекомендации по направлениям разработки и доработки программного обеспечения и систем. Анализ, представленный в статье, может быть полезен для предприятий авионики и других отраслей, перед которыми стоят задачи выбора программного обеспечения для поддержки процессов жизненного цикла разработки в новых и текущих проектах разработки сложных систем. Также данные о продуктах и выводы могут быть полезны специалистам, интересующимся текущим состоянием российской ИТ-индустрии.
ISSN 2220-6426 (Online)
