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

ВВЕДЕНИЕ.з

Глава 1. ТРЕБОВАНИЯ ЭФФЕКТИВНОСТИ И ФОРМАЛЬНЫЕ МЕТОДЫ РАЗРАБОТКИ.

1.1. Нефункциональные требования в технологическом процессе.

1.2. Формальные методы разработки.

1.3. Разработка распределенных вычислительных систем.

Глава 2. ФОРМАЛЬНАЯ СПЕЦИФИКАЦИЯ МОДЕЛЕЙ ВЫЧИСЛЕНИЙ.за

2.1. Частичная интерпретация.

2.2. Модели анализа машинной арифметики.

Глава 3. МОДЕЛИРОВАНИЕ АРХИТЕКТУРЫ МАШИННОЙ АРИФМЕТИКИ.

3.1. Проблема отображения и архитектура арифметики.

3.2. Логика Лукасевича и ее обогащения.бз

3.3. Представление машинной арифметики в логике Лукасевича.

Глава 4. АРХИТЕКТУРА ВРЕМЕНИ В РАСПРЕДЕЛЕННЫХ СИСТЕМАХ.

4.1. Коммуникационное время.

4.2. Архитектурные подсистемы распределенных систем.

4.3. Математические методы архитектурной декомпозиции.

4.4. Шаблоны проектирования распределенных систем.

Глава 5. ВОПРОСЫ РЕАЛИЗАЦИИ РАСПРЕДЕЛЕННЫХ ВЫЧИСЛИТЕЛЬНЫХ СИСТЕМ.т

5.1. Модели вычислений языков программирования.

5.2. Логические основы инспектирования программ.

5.3. Реализация распределенных систем.1 п

Актуальность работы. Объемы вычислений, которые требуются для решения научных и прикладных задач, часто превышают возможности отдельного компьютера. Поэтому вычисления распределяются по нескольким одновременно функционирующим аппаратным единицам, объединенным в вычислительную сеть. При этом возникает ряд факторов, без учета которых не удается добиться реального выигрыша в эффективности [14]: сложные взаимные зависимости между фрагментами задачи, гетерогенность используемой аппаратуры, случайные колебания загрузки аппаратных ресурсов. Имеющиеся подходы к решению таких проблем слабо интегрированы с современными общеупотребительными технологиями программирования, в том числе по причине относительной малочисленности и узкой специализации традиционных крупномасштабных распределенных вычислительных систем. Как пользователи, так и разработчики таких систем обычно отбираются среди высококвалифицированных научных и инженерных кадров, способных овладевать сложными «недружественными» программно-аппаратными средами. В свою очередь, организа-^ ции-заказчики таких проектов, как правило, принадлежат к привилегированным секторам экономики, таким как фундаментальная наука или военно-промышленный комплекс, что существенно понижает риск этих проектов оказаться в числе «безнадежных».

Однако в настоящее время удешевление вычислительной аппаратуры и появление технологий класса GRID [91], позволяющих распределять вычисления по свободным ресурсам узлов сети Интернет, стимулируют создание распределенных информационно-вычислительных служб для широкого круга по-■jf- требителей. Примерами таких служб являются прикладные системы обработки текстов и мультимедиа, анализа финансовых или медицинских данных. Доступ к таким службам организуется путем динамической интеграции персональных устройств (в том числе карманных компьютеров и интеллектуальных сотовых телефонов) в распределенную инфраструктуру сервисных вычислительных центров. Таким образом, намечается массовое возрождение вычислительных технологий, берущих начало еще от кластеров мэйнфреймов (mainframe) с ав-.i? томатической диспетчеризацией задач, на качественно новом уровне. Для удовлетворения спроса на такие решения необходимо адаптировать современные методы разработки к данному классу систем.

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

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

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

Достижение этой цели требует решения следующих задач:

- идентификация характеристик эффективности распределенных вычислительных систем и оценка возможности обеспечения ограничений на их значения посредством различных формальных методов;

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

- разработка математического метода построения моделей алгоритмов, обеспечивающего эффективное отображение проблем вычислительной математики на архитектуру гетерогенных компьютерных систем и сетей;

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

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

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

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

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

- архитектурная декомпозиция распределенной системы на основе моделирования сценариев обмена данными посредством частично упорядоченных множеств.

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

Практическая ценность работы заключается в возможности использовать предложенные методы при разработке распределенных вычислительных систем, в том числе для решения следующих практических задач:

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

- обеспечение корректности модели вычислений при соблюдении ограничений на объем ресурсов, выделяемых для хранения числовых данных;

- эффективное отображение алгоритмической модели на архитектуру гетерогенной компьютерной системы;

- верификация вычислений с использованием техники доказательства теорем многозначной логики (в том числе автоматизированного);

- архитектурная декомпозиция распределенных систем на основе анализа условий взаимной синхронизации компонентов.

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

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

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

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

ЗАКЛЮЧЕНИЕ

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

1. Построена модель качества на базе стандарта КОЛЕС 9126, в рамках которой формализованы нефункциональные требования к алгебраической абстрактности, производительности, ресурсоемкости и надежности, характеризующие эффективность распределенных вычислительных систем. Проанализированы подходы к обеспечению этих требований в ходе разработки.

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

3. Для обеспечения эффективного отображения вычислительных задач на архитектуру гетерогенных компьютерных систем предложен язык моделирования и анализа алгоритмов АБЬ, основанный на аппарате многозначной логики Лукасевича и ее обогащений. Модели вычислений представляются средствами этого языка в виде базисов логических функций.

4. Разработаны математические методы компонентной декомпозиции распределенных систем с учетом требований к производительности, основанные на моделировании сценариев обмена данными посредством частично упорядоченных множеств. Проанализированы такие шаблоны проектирования распределенных систем, как многоопорные и кластерные архитектуры.

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

1. Андрианов А.Н., Бугеря А.Б., Ефимкин КН., Задыхайло И.Б. Норма. Описание языка. Рабочий стандарт // Препринт ИПМ им. М.В.Келдыша РАН. N120, 1995.

2. Антимиров В.М., Воронков A.A., Дегтярев А.И., Захаръящев М.В., Прог(ен-ко B.C. Математическая логика в программировании. Обзор // Математическая логика в программировании. М.: Мир, 1991. С. 331-407.

3. Арестова М.Л., Быковский А.Ю. Методика реализации оптоэлектронных схем многопараметрической обработки сигналов на основе принципов многозначной логики // Квантовая электроника. Т. 22, №10, 1995. С. 980984.

4. Астелс Д., Миллер Г., Новак М. Практическое руководство по экстремальному программированию. М.: «Вильяме», 2002.

5. Ахо A.B., Хопкрофт Дж., Ульман Дж. Построение и анализ вычислительных алгоритмов. М.: Мир, 1979.

6. Ахо A.B., Хопкрофт Дж., Ульман Дж. Структуры данных и алгоритмы. М.: «Вильяме», 2001.

7. Бауэр Ф.Л., ГоозГ. Информатика. Вводный курс. Т. 1-2. М.: Мир, 1990.

8. Бочвар Д.А., Финн В.К. О многозначных логиках, допускающих формализацию антиномий. 1 // Исследования по математической лингвистике, математической логике и информационным языкам. М.: Наука, 1972. С. 238295.

9. Брадис В.М. Четырехзначные математические таблицы. 56-е изд. М.: Просвещение, 1988.

10. Брукс Ф. Мифический человеко-месяц. СПб.: Символ-Плюс, 1999.

11. Буч Г. Объектно-ориентированный анализ и проектирование с примерами приложений на С++. 2-е изд. М.: Бином, СПб.: Невский Диалект, 1999.

12. Важенин А.П. Параллельные вычисления с динамической длиной операндов: проблемы и перспективы // Системная информатика. Вып. 7. Новосибирск: Наука, 2000. С. 225-274.

13. Воеводин В.В. Отображение проблем вычислительной математики на архитектуру вычислительных систем // Вычислительные методы и программирование. Т.1, 2000. С. 37-44.

14. Воеводин В.В., Воеводин Вл.В. Параллельные вычисления. СПб.: БХВ-Петербург, 2002.

15. Волков Д.А. Универсальный сервер Unis // Открытые системы, №11-12, 1999. С. 17-20.

16. Гамма Э., Хелм Р., Дэ/сонсон Р., Влассидес Дж. Приемы объектно-ориентированного проектирования. Паттерны проектирования. СПб.: Питер, 2001.

17. Гашков С.Б., Чубариков В.Н. Арифметика. Алгоритмы. Сложность вычислений. М.: Высшая школа, 2000.

18. Голдблатт Р. Логика времени и вычислимости. М.: ОИЛКРЛ, 1992.

19. Гончаров С.С., Ершов Ю.Л., СамохваловК.Ф. Введение в логику и методологию науки. М.: Интерпракс, 1994.

20. Данные в языках программирования. М.: Мир, 1982.

21. Замулин A.B. Императивная спецификация динамических систем // Системная информатика. Вып. 7. Новосибирск: Наука, 2000. С. 82-111.

22. Калбертсон Р., Браун К., Кобб Г. Быстрое тестирование. М.: «Вильяме», 2002.

23. Калиткин H.H. Численные методы. М.: Наука, 1978.

24. Камер Д. Э. Сети ТСРЛР. Т. 1. Принципы, протоколы и структура. 4-е изд. М.: «Вильяме», 2003.

25. Карпенко A.C. Логики Лукасевича и простые числа. М.: Наука, 2000.

26. Карпенко A.C. Многозначные логики // Логика и компьютер. Вып. 4. М.: Наука, 1997.

27. Касьянов В.Н., Евстигнеев В.А. Графы в программировании: обработка, визуализация и применение. СПб.: БХВ-Петербург, 2003.

28. Касьянов В.Н., Поттосин И.В. Методы построения трансляторов. Новосибирск: Наука, 1986.

29. КейслерГ., Чэн Ч.Ч. Теория моделей. М.: Мир, 1977.

30. Керниган Б., Наш Р. Практика программирования. М.: Бином, СПб.: Невский Диалект, 2001.

31. Клещев A.C., Артемьева И.Л. Необогащенные системы логических отношений. Ч. 1 // НТИ. Сер. 2, №7, 2000. С. 18-28.

32. Клещев A.C., Артемьева И.Л. Необогащенные системы логических отношений. Ч. 2 // НТИ. Сер. 2, №8, 2000. С. 8-18.

33. Ковалев С.П. Аналитические модели машинной арифметики // Сибирский журнал индустриальной математики. Т. 6, №3, 2003. С. 88-102.

34. Ковалев С.П. Архитектура времени в распределенных информационных системах // Вычислительные технологии. Т. 7, №6, 2002. С. 38-53.

35. Ковалев С.П. Логика Лукасевича как архитектурная модель арифметики // Сибирский журнал индустриальной математики. Т. 6, №4, 2003. С. 32-50.

36. Ковалев С.П. Применение законов логики к решению инженерных задач // Труды научно-исследовательского семинара Логического центра Института Философии РАН. Вып. XV. М.: ИФРАН, 2001. С. 46-56.

37. Ковалев С.П. Принципы профессионального программирования // Смирновские чтения. 3 Международная конференция. М.: ИФРАН, 2001. С. 4244.

38. Кормен Т., Лейзерсон Ч., Ривест Р. Алгоритмы: построение и анализ. М.: МЦНМО, 2002.

39. Котов В.Е. Сети Петри. М.: Наука, 1984.

40. Кремнев Г.П. Управление производительностью и качеством. 17-модульная программа для менеджеров «Управление развитием организации». Модуль 5. М.: ИПФРА-М, 1999.

41. Кузнецов A.B. О средствах для обнаружения невыводимости и невыразимости//Логический вывод. М.: Наука, 1979. С. 5-33.

42. Лавров С.С. Программирование. Математические основы, средства, теория. СПб.: БХВ-Петербург, 2001.

43. Леоненков А. Самоучитель UML. СПб.: БХВ-Петербург, 2002.

44. Логическое программирование. М.: Мир, 1988.

45. Марка Д.А., Мак-Гоуэн К. Методология структурного анализа и проектирования. М.: Метатехнология, 1993.

46. Минскнй М. Фреймы для представления знаний. М.: Энергия, 1979.

47. Немет Э., Снайдер Г., Сибасс С., Хеш Т. UNIX: руководство системного администратора. СПб.: БХВ-Петербург, 1999.

48. Непейвода H.H. Прикладная логика. Новосибирск: НГУ, 2000.

49. Непомнящий В.А., Шилов Н.В., Бодин Е.В. REAL: язык для спецификации и верификации систем реального времени // Системная информатика. Вып. 7. Новосибирск: Наука, 2000. С. 174-224.

50. Одинцов И.О. Профессиональное программирование. Системный подход. СПб.: БХВ-Петербург, 2002.

51. Пратт Т., Зелковиц М. Языки программирования: разработка и реализация. 4-е изд. СПб.: Питер, 2002.

52. Смелянский Р.Л. Методы анализа и оценки производительности вычислительных систем. М.: МГУ, 1990.

53. Смит К.У., Уильяме Л.Дэ/с. Эффективные решения. Практическое руководство по созданию гибкого и масштабируемого программного обеспечения. М.: «Вильяме», 2003.

54. Соммервшл И. Инженерия программного обеспечения. 6-е изд. М.: «Вильяме», 2002.

55. Столлингс В. Современные компьютерные сети. 2-е изд. СПб.: Питер, 2003.

56. Таненбаум Э. Архитектура компьютера. 4-е изд. СПб.: Питер, 2002.

57. Таненбаум Э., ван Стеен М. Распределенные системы. Принципы и парадигмы. СПб.: Питер, 2003.

58. Тарский А. Введение в логику и методологию дедуктивных наук. Биробиджан: ИП «ТРИВИУМ», 2000.

59. Тыугу Э.Х. Концептуальное программирование. М.: Наука, 1984.

60. Уоррен Г. Алгоритмические трюки для программистов. М.: «Вильяме», 2003.

61. Флетчер К. Вычислительные методы в динамике жидкости. Т. 1-2. М.: Мир, 1991.

62. Френкель А., Бар-Хиллел И. Основания теории множеств. М.: Мир, 1966.

63. Хоар Ч. Взаимодействующие последовательные процессы. М.: Мир, 1989.

64. Цимбал A.A., Аншина M.JI. Технологии создания распределенных систем. СПб.: Питер, 2003.

65. Четверушкгш Б.Н. Кинетические схемы и высокопроизводительные многопроцессорные вычисления в газовой динамике // Вычислительные технологии. Т. 7, №6, 2002. С. 65-89.

66. Яблонский C.B. Введение в теорию функций £-значной логики // Дискретная математика и математические вопросы кибернетики. T. I. М.: Наука, 1974. С. 9-66.

67. Яблонский C.B. Функциональные построения в fc-значной логике // Труды МИАН им. В.А.Стеклова. Т. 51, 1958. Стр. 5-142.

68. Якобсон А., Буч Г., РамбоДэ/с. Унифицированный процесс разработки программного обеспечения. СПб.: Питер, 2002.

69. Allen R. J., Garlan D. A formal basis for architectural connection // ACM Trans, on Software Engineering and Methodology, 6(3), 1997. P. 213-249.

70. Allen R. J., Garlan D. Formal modeling and analysis of the HLA component integration standard // Proc. 6th ACM SIGSOFT Symp. on the Foundations of Software Engineering. Lake Buena Vista: ACM Press, 1998. P. 70-79.

71. Alur R., Henzinger T. Logics and models of real time: a survey I I Lecture Notes in Computer Science. Vol. 600,1991. P. 74-106.

72. Barnett M., Schulte W. Runtime verification of .NET contracts I I Journal of Systems and Software, 65(3), 2003. P. 199-208.

73. Beavers G. Automated theorem proving for Lukasiewicz logics // Studia Lógica. Vol. 52, N2,1993. P. 183-195.

74. Belov S.D., Bredikhin S.V., Kovalyov S.P., Kulagin S.A., Musher S.L., Scher-bakova N.G., Shabalnikov I.V. The emerging Internet landscape in Siberia // Computer Networks, 30, 1998. P. 1657-1662.

75. Bertoni A., Mauri G., Miglioli P. On the power of model theory to specify abstract data types and to capture their recursiveness // Fundamenta Informaticae, IV.2, 1983. P. 129-170.

76. Bolognesi T., Brinksma E. Introduction to the ISO specification language LOTOS // Computer Networks, 14(1), 1987. P. 25-59.

77. Bonner A., Kifer M. A logic for programming database transactions // Logics for Databases and Information Systems. Amsterdam: Kluwer Academic Publishers, 1998. P. 117-166.

78. Botella P., Burgués X., Franch X., Huerta M., Salazar G. Modeling nonfunctional requirements // Proc. JIRA'2001. Sevilla: 2001. http://www.lsi.us.es/~amador/JIRA/Ponencias/JIRA Botella.pdf.

79. Breitman K.K., Leite J.C.S.P., Finkelstein A. The world's a stage: a survey on requirements engineering using a real-life case study // J. Brazilian Computer Society, 6(1), 1999. P. 13-37.

80. Bull J.M., Smith L.A., Pottage L., Freeman R. Benchmarking Java against C and Fortran for scientific applications // Proc. ACM 2001 Java Grande Conf. Stanford: ACM, 2001. P. 97-105.

81. Bunn J., Newman 11. Data-intensive Grids for high-energy physics // Grid Computing: Making the Global Infrastructure a Reality. New York: Wiley & Sons, 2003. P. 859-906.

82. Chung L., Nixon B. A., Yu E., Mylopoulos J. Non-Functional Requirements in Software Engineering. Boston: Kluwer Academic Publishing, 2000.

83. Clarke E., Wing J. Formal methods: state of the art and future directions // ACM Computing Surveys, 28(4), 1996. P. 626-643.

84. Craigen D., Gerhart S., Ralston T.J. An international survey of industrial applications of formal methods. Vols. 1-2. NIST Report GCR-626. U.S. National Institute of Standards and Technology, 1993. http://his-sa.ncsl.nist.gov/pubs/soft dev.html#formal.

85. Dashofy E.M., van der Hoek A., Taylor R.N. An infrastructure for the rapid development of XML-based architecture description languages // Proc. 24th ICSE. Orlando: ACM Press, 2002. P. 266-276.

86. Enterprise Solution Patterns Using Microsoft .NET. Redmond: Microsoft Corp., 2003. http://msdn.microsoft.com/architecture/patterns/.

87. Epstein G., Frieder G., Rine D.C. The development of multiple valued logic as related to computer science // IEEE Computer, 7(9), 1974. P. 20-32.

88. Evans J., Trimper G. Itanium Architecture for Programmers: Understanding 64Bit Processors and EPIC Principles. Englewood Cliffs, NJ: Prentice Hall, 2003.

89. Evans T., Schwartz P.B. On Slupecki T-functions // J. Symbolic Logic. Vol. 23, 1958. P. 267-270.

90. Fidge C.J. Logical time in distributed systems // IEEE Computer, 24(8), 1991. P. 28-33.

91. Foster I. The Grid: A New Infrastructure for 21st Century Science // Grid Computing: Making the Global Infrastructure a Reality. New York: Wiley & Sons, 2003. P. 51-64.

92. Fu Q., Harnois P., Logrippo L., Sincennes J. Feature interaction detection: a LOTOS-based approach // Computer Networks, 32(4), 2000. P. 433-448.

93. Futatsugi K., Goguen J.A., Jouannaud J.-P., Meseguer J. Principles of OBJ2 // Proc. 12th ACM Symp. on Principles of Programming Languages. New Orleans: ACM Press, 1985. P. 52-66.

94. Goad C.A. Proofs as descriptions of computations // Lecture Notes in Computer Science. Vol. 87, 1980. P. 39-52.

95. Goguen J. An introduction to algebraic semiotics, with applications to user interface design // Computation for Metaphor, Analogy and Agents. Springer Lecture Notes in Artificial Intelligence. Vol. 1562, 1999. P. 242-291. •

96. Gorlatch S. Send-recv considered harmful? Myths and truths about parallel programming // Lecture Notes in Computer Science. Vol. 2127, 2001. P. 243-257.

97. Gruber T.R. Toward principles for the design of ontologies used for knowledge sharing // Intl. Journal of Human-Computer Studies, 43, 1995. P. 907-928.

98. Gurevich Y. Evolving Algebras 1993: Lipari Guide // Specification and Validation Methods. Oxford: Oxford University Press, 1995. P. 9-36.

99. Gurevich Y., Rosenzweig D. Partially ordered runs: a case study // Lecture Notes in Computer Science. Vol. 1912, 2000. P. 131-150.

100. Haupt T., Pierce M.E. Distributed object-based Grid computing environments // Grid Computing: Making the Global Infrastructure a Reality. New York: Wiley~ & Sons, 2003. P. 713-728.

101. Houston I., King S. CICS project report: experiences and results from the use of Z // Proc. VDM'91. Lecture Notes in Computer Science. Vol. 551, 1991. P. 588596.

102. ISO/IEC 12207. Information Technology Software Life Cycle Processes. Geneva: ISO/IEC, 1995.

103. ISO/IEC 14598. Information Technology Software Product Evaluation. Parts 1-6. Geneva: ISO/IEC, 2000.

104. ISO/IEC 9126. Information Technology Software Quality Characteristics and Metrics. Parts 1-4. Geneva: ISO/IEC, 1998.

105. ISO 9000. International Standards for Quality Management. Geneva: ISO, 2000.

106. Jones C. B. Systematic Software Development using VDM. London: Prentice-Hall, 1990.

107. Kahan W. Lecture Notes on the Status of IEEE Standard 754 for Binary Floating-Point Arithmetic. Berkeley: 1996. http://www.cs.berkeley.edu/~wka-han/ieee754statu sZIEEE754.pdf.

108. Kifer M., Lausen G., Wu J. Logical foundations of object-oriented and frame-based languages // Journal of the ACM, 42(4), 1995. P. 741-843.

109. Kovalyov S.P. On foundations of software engineering // 5th Intl. Conf. PSI'03. Bull. Workshop "Science Intensive Software". Novosibirsk: IIS SB RAS, 2003. P. 34-38.

110. Leavens G.T., Pigozzi D. A complete algebraic characterization of behavioral subtyping // Acta Informatica, 36(8), 2000. P. 617-663.

111. Lieberherr K.J. Adaptive Object-Oriented Software: The Demeter Method. Boston: PWS Publishing Company, 1996.

112. Luckham D.C. The Power of Events: An Introduction to Complex Event Processing in Distributed Enterprise Systems. Wokingham: Addison Wesley, 2002.

113. Luckham D.C., Kenney J. J., Augustin L.M., Vera J., Bryan D., Mann W. Specification and analysis of system architecture using Rapide // IEEE Trans. Software Engineering, 21(4), 1995. P. 336-355.

114. Mazzocca N. Rak M., Villano U. MetaPL: a notation system for parallel program description and performance analysis // Proc. PaCT2001. Lecture Notes in Computer Science. Vol. 2127, 2001. P. 80-93.

115. Mathai J. Problems, promises and performance: some questions for real-time system specification // Lecture Notes in Computer Science. Vol. 600, 1991. P. 315-324.

116. Mattern F. Virtual time and global states of distributed systems // Proc. Parallel and Distributed Algorithms Conf. Amsterdam: North Holland, 1988. P. 215-226.

117. McNaughton R. A theorem about infinite valued sentential logic // J. Symbolic Logic. Vol. 16, 1951. P. 1-13.

118. Medvidovic N. Taylor R.N. A classification and comparison framework for software architecture description languages // IEEE Trans. Software Engineering, 26(1), 2000. P. 70-93.

119. Mills D.L. Internet time synchronization: the network time protocol // IEEE Trans. Communications, 39(10), 1991. P. 1482-1493.

120. Monson-Haefel R. Enterprise Java Beans. 3rd ed. Sebastopol: O'Reilly, 2001.

121. Mount D. Bioinformatics. Sequence and Genome Analysis. Cold Spring Harbor: CSHL Press, 2001.

122. Onneweer S.P., Kerkhoff H.G. High-radix current-mode CMOS circuits based on the truncated-difference operator // 17th Intl. Symp. on Multiple-Valued Logic. Boston: IEEE, 1987. P. 188-195.

123. OWL Web Ontology Language guide. W3C working draft. W3 Consortium, 2003. http://www. w3.org/TR/2003/WD-owI-guide-20030331 /.

124. Owre S., Rajan S., Rushby J.M., Shankar N. Srivas M.K. PVS: combining specification, proof checking, and model checking // Proc. CAV'96. Lecture Notes in Computer Science. Vol. 1102, 1996. P. 411-414.

125. Pratt V.R. Modeling concurrency with partial orders // Intl. Journal of Parallel Programming. 15(1), 1986. P. 33-71.

126. Prowell S.J., Trammell C.J., Linger R.C., Poore J.H. Cleanroom Software Engineering: Technology and Process. Reading: Addison-Wesley Longman, 1999.

127. Raynal M., Singhal M. Logical time: capturing causality in distributed systems // IEEE Computer, 29(2), 1996. P. 49-56.

128. Rosa N.S., Justo G.R.R., Cunha P.R.F. Incorporating non-functional requirements into software architecture // Lecture Notes in Computer Science. Vol. 1800, 2000. P. 1009-1018.

129. Rosenberg LG. Completeness properties of multiple-valued logic algebras // Computer science and multiple-valued logic. Amsterdam: North Holland, 1977. P. 144-186.

130. Sannella D. A survey of formal software development methods // Software Engineering: A European Prospective. IEEE Computer Society Press, 1993. P. 281-297.

131. Schmidt D.C., Stal M., Rohnert //., Buschmann F. Pattern-Oriented Software Architecture. Vol. 2. Patterns for Concurrent and Networked Objects. New York: Wiley & Sons, 2000.

132. Shaw M., Garlan D. Formulations and formalisms in software architecture // Computer Science Today. Lecture Notes in Computer Science. Vol. 1000, 1996. P. 307-323.

133. Smith C.U., Williams L.G. Performance engineering of object-oriented systems with SPE ED // Lecture Notes in Computer Science. Vol. 1245, 1997. P. 135154.

134. Specification and Description Language. ITU-T Recommendation Z.100. Geneva: ITU, 1999.

135. Spivey J.M. The Z Notation: a reference manual. 2nd Edition. London: Prentice Hall, 1992.

136. Stevens W. UNIX Network Programming Networking APIs: Sockets and XTI. 2nd ed. Englewood Cliffs, NJ: Prentice-Hall, 1998.

137. Tierney B., AydtR., Gunter D., Smith W., Swany W., Taylor V., WolskiR. A Grid Monitoring Architecture. Argonne: Global Grid Forum, 2002.

138. Tse T.H., Pong L. An examination of requirements specification languages // The Computer Journal, 34, 1991. P. 143-152.

139. TMS320C3x General-Purpose Applications User's Guide. Austin: Texas Instruments, 1998. http://www-s.ti.com/sc/psheets/spru 194/spru 194.pdf.

140. Wolter U. A coalgebraic introduction to CSP // Proc. CMCS'99. Elsevier Electronic Notes in Theoretical Computer Science. Vol. 19, 1999. http://www.else-vier.nl/cas/tree/store/tcs/free/entcs/store/tcsl9/tcsl9006.ps.