Моделирование многокомпонентных систем при помощи взаимодействующих X-машин тема диссертации и автореферата по ВАК РФ 05.13.18, кандидат физико-математических наук Соболев, Михаил Сергеевич

• Соболев, Михаил Сергеевич
• кандидат физико-математических наук
• 2010

Оглавление диссертации кандидат физико-математических наук Соболев, Михаил Сергеевич

ВВЕДЕНИЕ.

ГЛАВА 1. СУЩЕСТВУЮЩИЕ ПОДХОДЫ К МОДЕЛИРОВАНИЮ

МНОГОКОМПОНЕНТНЫХ СИСТЕМ.

1.1. Модели данных.

1.2. Машина Тьюринга.

1.3. Сети Петри.

1.4. Конечные автоматы.

1.5. Диаграммы состояний.

1.6. Х-машины.

1.7. Вычислительные способности Х-машин.

1.8. Взаимодействующие Х-машины.

1.8.1. Взаимодействие через матрицу коммуникаций.

1.9. Выводы.

ГЛАВА 2. СИСТЕМЫ ВЗАИМОДЕЙСТВУЮЩИХ Х-МАШИН.

2.1. Поэтапное построение взаимодействующих Х-машин.

2.2. Пример: модель перекрестка со светофорами.

2.3. Расширение системы.

2.4. Выводы.

ГЛАВА 3. ФОРМАЛЬНАЯ ВЕРИФИКАЦИЯ Х-МАШИН.

3.1. Логика СТЬ.

3.2. ЛогикаХ-СТЬ

3.3. Пример.

3.4. Выводы.

ГЛАВА 4. ЯЗЫК ОПИСАНИЯ СИСТЕМ Х-МАШИН.

4.1. Краткое описание используемых ХМЬ-технологий.

4.2. Описание конструкция языка ХЕ)Ь.

4.2.1. Параметры.

4.2.2. Псевдонимы.

4.2.3. Типы данных.

4.2.4. Описание Х-машины.

4.2.5. Описание системы Х-машин.

4.3. Библиотека для моделирования Х-машин.

4.3.1. Общее описание библиотеки.

4.3.2. Типы данных.

4.3.3. Ввод и вывод.

4.3.4. Детали реализации.

4.4. Выводы.

ГЛАВА 5. МОДЕЛЬ РАСПРЕДЕЛЕННОГО ХРАНИЛИЩА ДАННЫХ.

5.1. Распределенное хранилище данных.

5.2. Общее описание модели.

5.3. Модель узла.

5.3.1. Взаимодействие с сервером приложений.

5.3.2. Выполнение команд хранилища.

5.4. Модель хранилища.

5.4.1. Отправка отсроченных сообщений.

5.4.2. Чтение и запись.

5.5. Производительность распределенного хранилища.

5.6. Выводы.

Введение диссертации (часть автореферата) на тему «Моделирование многокомпонентных систем при помощи взаимодействующих X-машин»

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

Замена такого оборудования компьютеризированными аналогами часто представляется более универсальным, гибким и экономически эффективным подходом. При этом проектирование прибора как такового во многом заменяется проектированием программного обеспечения для компьютерного контроллера. Часто несколько компьютеризированных приборов или программных комплексов работают в составе одной системы, обмениваясь данными и сообщениями. В таком случае совокупность программ этих приборов составляет многокомпонентную программную систему. К надежности такой системы предъявляются очень высокие требования: ошибка в проектировании может привести к самым серьезным последствиям.

Жесткие требования предъявляются также к надежности и производительности многокомпонентных систем — серверным приложениям, на которые приходится большая часть функциональной нагрузки в клиент-серверных системах. Кроме того, в серверных приложениях широко используется параллельное программирование, что затрудняет поиск ошибок и оценку производительности. Часто традиционные методы отладки, используемые при разработке клиентских приложений, не обеспечивают должного уровня тестирования.

Математическое описание программной системы и требований к ней позволяет улучшить качество критически важных систем, в частности многокомпонентных^].

При моделировании многокомпонентных систем можно выделить два аспекта: моделирование данных и моделирование алгоритмов. Большинство из существующих формальных методов-позволяют полно описать только один из этих аспектов. Для моделирования данных обычно используют иерархические, сетевые или реляционные модели, а для описания алгоритмов — модели, основанные на автоматах (машинах состояний): конечные автоматы, автоматы с магазинной памятью, машины Тьюринга[2].

Одним из немногих методов, позволяющих сочетать достоинства обоих подходов, является моделирование на основании.Х-машин. В определении X-машины к состояниям конечного автомата добавляется память, позволяющая хранить типизированные данные. Это дает возможность описывать как динамические, так и статические аспекты системы.

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

Необходимым условием возможности применения-рассматриваемого метода на практике является существование достаточно развитого языка для описания систем взаимодействующих Х-машин, а также программного обеспечения для осуществления моделирования динамического поведения системы.

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

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

Таким образом, в работе решаются следующие задачи:

1. Разработка теоретических основ и метода построения систем взаимодействующих Х-машин, допускающих асинхронное взаимодействие между Х-машинами и поэтапное проектирование;

2. Формальная верификация Х-машин, позволяющая осуществлять тестирование компонентов систем взаимодействующих Х-машин;

3. Описание языка для создания спецификаций систем взаимодействующих Х-машин, а также комплекса программ позволяющего моделировать программные системы;

4. Моделирование распределенного хранилища данных с использованием предложенного метода.

Заключение диссертации по теме «Математическое моделирование, численные методы и комплексы программ», Соболев, Михаил Сергеевич

5.6. Выводы

В разделе предложена модель распределенного хранилища данных, реализованная в виде системы взаимодействующих Х-машин. Поскольку асинхронная коммуникация является важной частью РХД, реализация такой модели с использованием существующих методов построения систем Х-машин была бы сильно затруднена. Кроме того модели для узла и хранилища независимы и могут быть подвергнуты тестированию по отдельности, а также могут быть использованы в качестве составных частей других систем. Показано, что язык ХОЬ является достаточно выразительным и удобным средством для практического описания систем взаимодействующих Х-машин.

Значения производительности при разных параметрах, полученные при помощи разработанной модели, хорошо согласуются с экспериментально измеренными в распределенном хранилище 8са1еОШ: 81а1е8егуег значениями. Данная модель может быть применена для расчета оптимального количества реплик, обеспечивающего наилучшую производительность конкретной системы.

ЗАКЛЮЧЕНИЕ

В работе были получены следующие результаты:

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

2. Предложена темпоральная логика Х-СТЬ для формальной верификации Х-машин. Доказана достаточность минимального набора операторов.

3. Разработан язык ХОЬ для описания систем взаимодействующих X-машин. Создан программный комплекс в виде 1ауа-библиотеки для моделирования динамического поведения программных систем по их ХОЬ-спецификациям.

4. Предложенный метод использован для моделирования распределенного хранилища данных.

Список литературы диссертационного исследования кандидат физико-математических наук Соболев, Михаил Сергеевич, 2010 год

1. Young W. Formal Methods versus Software Engineering: Is There a Conflict? // 4th Symposium on Testing, Analysis and Verification. 1991. Victoria.

2. Соболев M.C. Автоматные модели вычислений // Современные проблемы фундаментальных и прикладных наук. Часть VII. Управление и прикладная математика: Труды 52-й научной конференции. М. - Долгопрудный: МФТИ, 2009. - С. 122-123.

3. Spivey J.M. Understanding Z : a specification language and its formal semantics. // Cambridge tracts in theoretical computer science. 1988, Cambridge Cambridgeshire ; New York: Cambridge University Press, viii, 131 p.

4. Jones C.B. Systematic software development using VDM. 2nd ed. Prentice Hall international series in computer science. 1990, New York: Prentice Hall, xiv, 333 p.

5. Futatsugi K., Jouannaud J-P., Meseguer J. Principles of OBJ2. // Proc.l2th. ACM Symp. Principles of Prog. Lang., 1985: p. 52-66.

6. Jacob I. Using Formal Specifications in the Design of a HumanComputer Interface. // Comm. ACM, 1983. 26(4): p. 259-264.

7. Huzing C. Introduction to Design Choices in the Semantics of Statecharts. // Information Processing, 1991.31.

8. Марков A.A., Нагорный H.M Теория алгоритмов. Мат. логика и основания математики. 1984, М.: Наука. 432 с.

9. Turing A.M. On Computable Numbers, with an Application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, 1937. 2(42): p. 230-65.

10. Hopcroft J.E., Motwani R., Ullman J.D. Introduction to automata theory, languages, and computation. 3rd ed. 2007, Boston: Pearson/Addison Wesley, xvii, 535 p.

11. Booth T.L. Sequential machines and automata theory. 1967, New York,: Wiley, xiv, 592 p.

12. Boas P.E. Machine Models and Simulations. Handbook of Theoretical Computer Science, 1990. Algorithms and Complexity: p. 3-66.

13. Peterson J.L. Petri net theory and the modeling of systems. 1981, Englewood Cliffs, N.J.: Prentice-Hall, x, 290 p.

14. Girault C. Petri nets for systems engineering : a guide to modeling, verification, and applications. 2003, New York: Springer, xvi, 607 p.

15. Нее K.M., Valk R. Applications and theory of Petri nets : 29th international conference, PETRI NETS 2008, Xi'an, China, June 2327, 2008 : proceedings. Lecture notes in computer science,. 2008, Berlin ; New York: Springer, xiii, 428 p.

16. Axo A.B:, Хопкрофт Д.Э., Улъман Д.Д Структуры данных и алгоритмы. 2010, Москва: Вильяме. 391 с.

17. Хопкрофт Д., Мотвани Р., Улъман Д. Введение в теорию автоматов, языков и вычислений. 2. изд. 2002, М.: Вильяме. 527 с.

18. Серебряков В.А. Лекции; по конструированию компиляторов Рос. АН, ВЦ; 1994, М.: ВЦ РАН. 174 с.

19. Wagner F. Modeling software with finite state machines.: a practical approach: 2006, Boca Raton, FL: Auerbach. xix, 369 p.

20. Harel Di, Politi M. Modeling reactive systems with statecharts : the statemate approach. 1998, New York: McGraw-Hill, xiv, 258 p;

21. Drusinsky D. Modeling and5 verification using UML statecharts : a working guide to reactive system design, runtime monitoring, and execution-based; model checking. 2006; Burlington, MA: Newnes. xii, 306 p.

22. Eilenberg S. Automata, languages, and? machines. Pure and applied mathematics a series of monographs and! text books, 58 i e 59. 1974, New York,: Academic Press.

23. Holcombe M. What are X-Machines? Formal aspects of computing, 2000. 12(6): p. 418-422.

24. Holcombe M. X-machines as a basis for dynamic system specification. Software Engineering Journal 1988. 3(2): p. 69-76.

25. Соболев M.C. Автоматные модели вычислений. Моделирование и обработка информации. -М.: МФТИ, 2009: С 76-85, 2009.

26. Aguado J. Systems of Communicatin X-machines for Specifying Distributed Systems. 2002, University of Sheffield.

27. Cowing A.J.G., Vertran C. A structured way to use channels for communication in X-machines systems. Formal aspects of computing, 2000. 12: p. 485-500.

28. Gheorgescn H. A New Approach to Communicating X-machines Systems. Journal of Universal Computer Science, 2000. 6(5): p. 490502.

29. Barnard J. COMX: a design methodology using Communicating X-machines. Information and Software Technology, 1998. 40: p. 271280.

30. Balanescn T.C., Gheorgescu H., Gheorghe M., Holcombe M., Vertran C. Communicating Stream X-machines are no more than X-machines. Journal of Universal Computer Science, 1999. 5(9): p. 494-507.

31. Kefalas P.E.,Kehris E. Communicating X-machines: a practical approach for formal and modular specification of large systems. Information and Software Technology, 2003. 45(5): p. 269-280.

32. Соболев M.С. Описание больших систем при помощи Х-машин // Современные проблемы фундаментальных и прикладных наук. Часть VII. Управление и прикладная математика: Труды 51-й научной конференции. М. - Долгопрудный: МФТИ, 2008. - С.20-22.

33. Соболев М.С. Описание больших систем при помощи Х-машин // Моделирование и обработка информации: Сб.ст./Моск.физ.-тех.ин-т. М., 2008. -С. 236-245.

34. Chan W.A., Beame R.J., Burns P. Model Checking Large Software Specifications. IEEE Transactions on Software Engineering, 1998. 24(7).

35. Соболев М.С. Описание систем при помощи Х-машин Информационные технологии и вычислительные системы, 2009. 4: р. 22-27.

36. Кларк Э.М., Грамберг С., Пелед Д. Верификация моделей программ: Model Checking. 2002, M.: Изд-во Моск. центра непрерыв. мат. образования. 416 с.

37. Ноаге С: An axiomatic basis for computer programming. Communications of the ACM, 1969.39.