Архитектура, системное, инструментальное и прикладное программное обеспечение, методы анализа и верификации информационно-вычислительных комплексов и сетей новых поколений

Объектом исследования являются различные аспекты организации высокопроизводительных вычислений, обработки и хранения данных: теоретические и практические исследования по автоматической верификации программ и развитию методов доказательного программирования, применение методов интеллектуальной обработки данных, инструментальные средства параллельного программирования, энергоэффективные аппаратные платформы для хранения сенсорных и других видов данных, алгоритмы потокового сжатия сенсорных данных. Цель исследований – создание теоретического базиса, аппаратных платформ и программных инструментальных средств для высокопроизводительных вычислений и обработки данных для различных областей науки и для практического применения. В отчете по НИР описаны исследования, применяемая методология и полученные результаты по следующим направлениям: - Развитие методов анализа и верификации моделей вычислительных систем и алгебраических объектов на основе средств функционального и логического программирования. Доказанные теоремы и методы, разработанные по данному направлению, относятся к технологии доказательного программирования (технология разработки программ с доказательствами правильности – отсутствия ошибок в программах). Верификация выполняется средствами суперкомпиляции, методы программно реализуются в разрабатываемых компиляторах и библиотеках. Возможные области применения: верификация параметризованных недетерминированных коммуникационных протоколов; верификация программных моделей аудита (sanitization) скриптов, пересылаемых по электронной сети с целью автоматического выполнения на компьютере клиента; разработка оптимизирующих компиляторов; для автоматических рассуждений, дополняющих прямые программные вычисления; верификация математических доказательств; верификация и анализ функциональных программ и цифровых устройств; системы автоматически проверяемых удостоверений (proof certificates). - Развитие методов оптимизации программ на объектно-ориентированных языках с помощью специализации на основе частичных вычислений. Разработан специализатор для языка JAVA, реализующий анализ программы времен связывания. Методы повышают продуктивность разработки программ (создается универсальная программа, которая затем cпециализируется под конкретные условия применения) и качество результата: специализатор гарантирует отсутствие ошибок в силу эквивалентности исходной программы и результата. - Развитие средств интеллектуальной обработки различных видов данных: изображений, полученных с помощью ДЗЗ (и не только), данных телеметрии, медицинских снимков, входных данных систем компьютерного зрения и беспилотной навигации. Обработка данных реализуется с помощью нейросетевых методов. Для каждого вида исходных данных выполнен поиск наиболее подходящих видов нейронных сетей (НС), способов подготовки данных и оптимальных значений различных параметров и настроек. Для улучшения точности и скорости распознавания предложены комбинированные методы обработки данных: многоступенчатая обработка, применение различных НС (или их сочетаний) и различных значений параметров настройки НС на разных этапах обработки, сочетание нейросетевых и других методов обработки. Предложен новый способ и математическая модель калибровки оптической стереосистемы, которая является частью системы беспилотной навигации мобильных роботов. - Развитие различных систем параллельных и распределенных вычислений и обработки данных. Для каждой из систем предложены свои средства повышающие эффективность обработки: потоковая обработка данных (стриминг), планирование и диспетчеризация нагрузки (динамические и статические методы), «горячая» адаптация распределения нагрузки под изменяющуюся конфигурацию вычислительной сети (и как следствие – отказоустойчивость), гибридные режимы вычислений для максимизации производительности, реализованные языковыми средствами. Для экспериментальной проверки принятых решений реализованы прикладные приложения. - Разработка технологий сенсорных сетей: аппаратных средств и алгоритмов обработки и хранения для сенсорных данных. Выполнено аппаратное прототипирование узла хранения данных для распределенной плавно масштабируемой системы хранения сенсорных (и других видов) данных с высокой доступностью; проведено экспериментальное исследование технических характеристик узла. Особенность такой системы – низкая стартовая стоимость, децентрализованная архитектура (нет одной точки уязвимости), возможность отказа от облачного хранения в целях безопасности с сохранением всех преимуществ распределенной архитектуры. Разработаны новые алгоритмы (и доказана их высокая эффективность) потокового сжатия сенсорных данных на сенсорных узлах в условиях ограниченной оперативной памяти. Алгоритмы экономят пропускную способность сети и ресурс автономного источника электропитания узла, увеличивают время автономной работы узлов при работе в режиме с эпизодической связности.