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

Статья посвящена теоретическим и практическим работам по тестированию конформности (conformance testing), которые выполнялись в ИСП РАН c 1994-го года и по настоящее время. Развитие теории конформности шло по нескольким направлением и в целом носило характер обобщения используемых семантик взаимодействия, моделей и конформностей. Необходимость такого обобщения диктовалась, прежде всего, требованиями практического тестирования. Это касается таких свойств систем как недетерминизм, частичная определённость, асинхронность, разнообразие тестовых воздействий и наблюдений над поведением реализации и т.п. При этом в центре внимания всегда находилась эффективность тестирования, определяемая как оптимизацией тестовых наборов, так и алгоритмами генерации тестов, в том числе on-fly. Мы рассматриваем основные вехи этого пути в кратком и неформальном обсуждении, уделяя внимание не деталям, а основным проблемам и способам их решения, пытаясь выявить общую тенденцию развития.

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

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

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

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

В работе описывается разрабатываемый в ИСП РАН инструмент автоматического статического анализа Svace. Инструмент позволяет находить ошибки и потенциальные уязвимости в исходном коде программ на языках Си/Си++. Особенностью инструмента являются простота использования, широкий набор поддерживаемых типов предупреждений, масштабируемость до программ в миллионы строк кода и приемлемое качество анализа (30-80% истинных предупреждений)

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

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

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

В статье описывается метод двухфазной компиляции программ на языках Си/Си++, позволяющий распространять приложения в промежуточном представлении LLVM. Описывается модификация компонентов LLVM с целью сокращения времени генерации кода. Описываются разработанные оптимизации с использованием профиля выполнения программы. Рассматривается организация специализированного облачного хранилища приложений.

В статье описываются разработанные в ИСП РАН методы запутывания программ, направленные на противодействие методам статического анализа программ. Рассматриваемые методы запутывания реализованы в обфусцирующем компиляторе на базе LLVM. Приводится оценка замедления и увеличения объема потребляемой памяти.

В статье рассматривается рабочий цикл оптимизации производительности приложений для заданной процессорной архитектуры на примере открытых компиляторов GCC и LLVM. Приводятся примеры выполненных оптимизаций и их результаты тестирования на известных наборах тестов. Также описывается инструмент TACT автоматической настройки компилятора на заданное приложение и его примерное использование как прикладным разработчиком, так и компиляторным инженером, приводятся результаты работы инструмента.

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

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

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

Одним из перспективных подходов организации эффективного взаимодействия науки, образования и индустрии является концепция web-лабораторий. Такая лаборатория представляет собой web-среду, которая поддерживает проведение научных исследований с использованием методов математического моделирования междисциплинарными коллективами узких специалистов, распределённых географически и административно. Возможности web-лаборатории включают: проведение численных экспериментов; составление отчетов, подготовку статей; обсуждение результатов на семинарах и совещаниях; планирование деятельности лаборатории; поддержку учебного процесса (проведение учебных курсов, практических занятий, лабораторных работ и т.п.) студентов и аспирантов. Полноценная реализация данной концепции связана с необходимостью обеспечить возможность использования различных аппаратных средств (суперкомпьютеров, высокопроизводительных кластеров, в том числе, с ускорителями вычислений, средств 2D и 3D визуализации, серверов, систем хранения и обработки больших массивов данных, пр.) и программных пакетов. При этом также должны быть обеспечены высокая масштабируемость на всех уровнях, надёжность и безопасность. Современным методом решения данной задачи является использование модели облачных вычислений, когда перечисленные выше ресурсы предоставляются удаленно в виде набора масштабируемых сервисов разного уровня с обслуживанием по запросу. В статье представлена разработанная в модели облачных вычислений архитектура web-лаборатории. Рассмотрены особенности реализации на ее основе программной платформы развертывания полноценных web-лабораторий UniHUB. Данная программная платформа интегрирована в состав свободного пакета поддержки облачных сред OpenStack и использует его сервисы в качестве основы.

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

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

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

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