Автореферат диссертации на соискание ученой степени

Вид материалаАвтореферат диссертации

Содержание


Общая характеристика работы
Цель работы
Научная новизна
Практическая ценность
Апробация работы
Структура и объем работы
Основное содержание работы
T – множества предложений подходящего языка первого порядка. Затем фиксируется некоторое конечное множество C
D0(A) – множество бескванторных предложений сигнатуры 0, истинных в A. Полиморфной структурой
S и хотя бы одну константу. Начальным отрезком
Y называется отношение t
X – предикат, истинный, если X
X отношения # на подмножество X
Основные выводы и результаты работы
Основные публикации по теме диссертации
Подобный материал:
  1   2



На правах рукописи


КОВАЛЁВ Сергей Протасович


АНАЛИЗ РАСПРЕДЕЛЕННЫХ ВЫЧИСЛИТЕЛЬНЫХ СИСТЕМ

С ПРИМЕНЕНИЕМ ТЕОРЕТИКО-МОДЕЛЬНЫХ МЕТОДОВ




Специальность: 05.13.11 – математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей


Автореферат

диссертации на соискание ученой степени

кандидата физико-математических наук


Новосибирск – 2003


Работа выполнена в Институте вычислительных технологий СО РАН


Научный руководитель: член-корреспондент РАН

Федотов Анатолий Михайлович


Официальные оппоненты: доктор физико-математических наук

Вирбицкайте Ирина Бонавентуровна

кандидат физико-математических наук

Шрайнер Павел Александрович


Ведущая организация: Институт динамики систем и теории управления СО РАН


Защита состоится 29 декабря 2003 г. в 12 часов на заседании диссертационного совета Д003.060.01 по адресу:

просп. Ак. Лаврентьева, 6,

Новосибирск, 630090,

Россия


С диссертацией можно ознакомиться в читальном зале Отделения вычислительной математики и информатики ГПНТБ и ИВТ СО РАН.


Автореферат разослан 25 ноября 2003 г.


Ученый секретарь

диссертационного совета Л.Б. Чубаров

д.ф.-м.н., проф.

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ



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

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

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

Цель работы: разработать формальные методы анализа распределенных вычислительных систем, ориентированные на обеспечение требований эффективности.

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

Эти задачи решены в работе с использованием методов теории моделей.

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

Корректность предложенных методов обоснована рядом теорем, снабженных подробными доказательствами.

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

Методы, представленные в работе, использовались автором при разработке распределенных вычислительных систем для задач ядерной физики, обработки мультимедиа-данных, семантического анализа текстов, а также при модернизации Сети Интернет Новосибирского научного центра. Кроме того, сформулированный подход положен в основу общего курса лекций «Сетевые технологии», который читается автором для студентов Факультета информационных технологий Новосибирского государственного университета.

Апробация работы. Результаты работы докладывались на следующих международных конференциях: Международная конференция «3 Смирновские чтения» (Москва, 2001); Международная конференция «Мальцевские чтения'2001» (Новосибирск, 2001); Международная конференция «Мальцевские чтения'2002» (Новосибирск, 2002); Международный конгресс «Математика в XXI веке» (Новосибирск, 2003); Семинар «Наукоемкое программное обеспечение» V Международной конференции «Перспективы систем информатики» (Новосибирск, 2003). Также работа была представлена на научных семинарах Института вычислительных технологий СО РАН, Института математики СО РАН, Института автоматики и электрометрии СО РАН, Института физики полупроводников СО РАН.

Публикации. По результатам выполненных исследований опубликовано 7 печатных работ.

Структура и объем работы. Диссертация состоит из введения, пяти глав, заключения и списка литературы. Общий объем работы – 123 страницы, библиография содержит 140 наименований.