Содержание к диссертации
ВВЕДЕНИЕ _ , „ з
Глава 1. ТРЕБОВАНИЯ ЭФФЕКТИВНОСТИ И ФОРМАЛЬНЫЕ
МЕТОДЫ РАЗРАБОТКИ а
Нефункциональные требования в технологическом процессе s
Формальные методы разработки 19
Разработка распределенных вычислительных систем 32
Глава 2. ФОРМАЛЬНАЯ СПЕЦИФИКАЦИЯ МОДЕЛЕЙ
ВЫЧИСЛЕНИЙ» за
Частичная интерпретация 38
Модели анализа машинной арифметики _ м
Глава 3. МОДЕЛИРОВАНИЕ АРХИТЕКТУРЫ МАШИННОЙ
АРИФМЕТИКИ - S3
Проблема отображения и архитектура арифметики 53
Логика Лукасевича и ее обогащения сз
Представление машинной арифметики в логике Лукасевича 68
Глава 4. АРХИТЕКТУРА ВРЕМЕНИ В РАСПРЕДЕЛЕННЫХ
СИСТЕМАХ. 82
КоММуНИКаЦИОННОе ВреМЯ 82
Архитектурные ПОДСИСТеМЫ распределенных СИСТеМ 88
Математические методы архитектурной декомпозиции 91
Шаблоны проектирования распределенных систем юг
Глава 5. ВОПРОСЫ РЕАЛИЗАЦИИ РАСПРЕДЕЛЕННЫХ
ВЫЧИСЛИТЕЛЬНЫХ СИСТЕМ. ю?
Модели вычислений языков программирования ю?
Логические основы инспектирования программ иг
Реализация распределенных систем і п
ЗАКЛЮЧЕНИЕ. из
Список литературы
Введение к работе
Актуальность работы. Объемы вычислений, которые требуются для
"г* решения научных и прикладных задач, часто превышают возможности отдель-
ного компьютера. Поэтому вычисления распределяются по нескольким одновременно функционирующим аппаратным единицам, объединенным в вычислительную сеть. При этом возникает ряд факторов, без учета которых не удается добиться реального выигрыша в эффективности [14]: сложные взаимные зависимости между фрагментами задачи, гетерогенность используемой аппаратуры, случайные колебания загрузки аппаратных ресурсов. Имеющиеся подходы
г к решению таких проблем слабо интегрированы с современными общеупотре-
бительными технологиями программирования, в том числе по причине относительной малочисленности и узкой специализации традиционных крупномасштабных распределенных вычислительных систем. Как пользователи, так и разработчики таких систем обычно отбираются среди высококвалифицированных научных и инженерных кадров, способных овладевать сложными «недружественными» программно-аппаратными средами. В свою очередь, орган иза-
л\ ции-заказчики таких проектов, как правило, принадлежат к привилегированным
секторам экономики, таким как фундаментальная наука или военно-промышленный комплекс, что существенно понижает риск этих проектов оказаться в числе «безнадежных».
Однако в настоящее время удешевление вычислительной аппаратуры и появление технологий класса GRID [91], позволяющих распределять вычисления по свободным ресурсам узлов сети Интернет, стимулируют создание распределенных информационно-вычислительных служб для широкого круга по-
if- требителей. Примерами таких служб являются прикладные системы обработки
текстов и мультимедиа, анализа финансовых или медицинских данных. Доступ к таким службам организуется путем динамической интеграции персональных устройств (в том числе карманных компьютеров и интеллектуальных сотовых телефонов) в распределенную инфраструктуру сервисных вычислительных центров. Таким образом, намечается массовое возрождение вычислительных технологий, берущих начало еще от кластеров мэйнфреймов (mainframe) с ав-
4і} тематической диспетчеризацией задач, на качественно новом уровне. Для удов-
летворения спроса на такие решения необходимо адаптировать современные методы разработки к данному классу систем.
Использование абстрактного математического языка для постановки вы
числительных задач предрасполагает к применению формальных методов при
анализе и разработке автоматизированных систем для их решения. Такие мето
ды позволяют создавать формальные функциональные спецификации и модели
^ архитектуры систем, а также осуществлять их преобразование в программы с
последующей верификацией (проверкой правильности) [54]. Набольшая отдача от формальных методов достигается путем создания формальных шаблонов, пригодных для многократного использования при разработке конкретных систем. Имеются CASE-средства, обеспечивающие поддержку различных формальных методов. Корректность получаемых результатов гарантируется математическим аппаратом, опирающимся на достижения алгебры, логики и
1 »^ дискретной математики, и в особенности теории моделей.
; С помощью аппарата теории моделей удается формализовать не только
функциональные требования к системам, но и характеристики их эффективности. Технологические стандарты выделяют ряд нефункциональных характеристик, например, производительность и надежность [104]. Недостаточное внимание к их анализу при создании распределенных вычислительных систем приводит к тому, что наблюдаемые показатели эффективности выполнения задач
і ^ отстают как от асимптотических оценок временной и ресурсной сложности ал-
горитмов, так и от паспортных значений пропускной способности коммуникационных каналов. Известны примеры, когда системы, ведущие себя в полном соответствии с формальной функциональной спецификацией, оказывались вообще непригодными для практического использования в силу недопустимо медленной работы или постоянных потерь данных в ненадежной комму никаци-
1 онной среде [79]. Однако технологические подходы к формализации нефунк-
циональных характеристик стали рассматриваться исследователями только в
"$ последние годы, поэтому «зрелые» технологии профаммирования позволяют
лишь частично учитывать требования эффективности. Наибольшую ценность
I представляют аспектно-ориентированные подходы, сочетающие формальные
: нотации для спецификации таких требований с методами их обеспечения в ходе
разработки [128]. Таким образом, актуальным является создание формальных
методов анализа эффективности при разработке распределенных вычислитель
ных систем.
V,"' Цель работы: разработать формальные методы анализа распределенных
вычислительных систем, ориентированные на обеспечение требований эффективности.
Достижение этой цели требует решения следующих задач:
- идентификация характеристик эффективности распределенных вычис
лительных систем и оценка возможности обеспечения ограничений на их зна
чения посредством различных формальных методов;
Л* - разработка формальной процедуры учета ограничений на объем дос-
тупных ресурсов при анализе требований к вычислительным системам;
разработка математического метода построения моделей алгоритмов, обеспечивающего эффективное отображение проблем вычислительной математики на архитектуру гетерогенных компьютерных систем и сетей;
построение формальных методов архитектурной декомпозиции распределенных систем с учетом требований к производительности.
Ч/ Эти задачи решены в работе с использованием методов теории моделей.
Научная новизна работы состоит в том, что предложены следующие математические методы анализа распределенных вычислительных систем, ориентированные на обеспечение требований к производительности, ресурсоемко сти и надежности в ходе разработки:
- частичная интерпретация теории первого порядка, отражающей функ
циональные требования к системе, конечной моделью заданной мощности;
л - представление модели вычислений слабо полным классом функций
подходящей многозначной логики, обогащающей логику Лукасевича;
- архитектурная декомпозиция распределенной системы на основе мо
делирования сценариев обмена данными посредством частично упорядоченных
множеств.
Корректность предложенных методов обоснована рядом теорем, снабженных подробными доказательствами.
Практическая ценность работы заключается в возможности использо-
і вать предложенные методы при разработке распределенных вычислительных
систем, в том числе для решения следующих практических задач:
выбор формального метода разработки, позволяющего наиболее адекватно учесть нефункциональные требования к создаваемой системе;
обеспечение корректности модели вычислений при соблюдении ограничений на объем ресурсов, выделяемых для хранения числовых данных;
- эффективное отображение алгоритмической модели па архитектуру
jtj гетерогенной компьютерной системы;
- верификация вычислений с использованием техники доказательства
теорем многозначной логики (в том числе автоматизированного);
- архитектурная декомпозиция распределенных систем на основе анализа условий взаимной синхронизации компонентов.
Методы, представленные в работе, использовались автором при разра
ботке распределенных вычислительных систем для задач ядерной физики, об-
* работки мультимедиа-данных, семантического анализа текстов, а также при
модернизации Сети Интернет Новосибирского научного центра. Кроме того, сформулированный подход положен в основу общего курса лекций «Сетевые технологии», который читается автором для студентов Факультета информационных технологий Новосибирского государственного университета.
Апробация работы. Результаты работы докладывались на следующих
международных конференциях: Международная конференция «3 Смирновские
"^ чтения» (Москва, 2001); Международная конференция «Мальцевские чте-
ния'2001» (Новосибирск, 2001); Международная конференция «Мальцевские
чтения'2002» (Новосибирск, 2002); Международный конгресс «Математика в
XXI веке» (Новосибирск, 2003); Семинар «Наукоемкое программное обеспече
ние» V Международной конференции «Перспективы систем информатики»
(Новосибирск, 2003). Также работа была представлена на научных семинарах
Института вычислительных технологий СО РАИ, Института математики СО
и\ РАН, Института автоматики и электрометрии СО РАН, Института физики по-
лупроводников СО РАН.
Публикации. По результатам выполненных исследований опубликовано 7 печатных работ.
Структура и объем работы. Диссертация состоит из введения, пяти глав, заключения и списка литературы. Общий объем работы - 123 страницы, библиография содержит 140 наименований.
