Специализированные модели для проектирования, разработки и реализации информационных систем тема диссертации и автореферата по ВАК РФ 05.13.11, кандидат физико-математических наук Бендума Тахар

• Бендума Тахар
• кандидат физико-математических наук
• 2010

Оглавление диссертации кандидат физико-математических наук Бендума Тахар

ВВЕДЕНИЕ

Цель работы

Методы исследования

Научная новизна

Практическая ценность результатов

На защиту выносятся

Связанные работы

Выводы

1. МОДЕЛИ ПРОГРАММНЫХ СИСТЕМ

1.1. Введение

1.2. Способы представления моделей

1.2.1. Неформальное моделирование

1.2.2. Полуформальное моделирование 13 Функциональные методы (картезианские методы) 13 Систематические методы 14 Объектно-ориентированные Методы

1.2.3. Формальное моделирование

1.2.4. Выводы

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

1.3.1. Графическая визуализация существующих языков формальной спецификации

1.3.2. Создание новых методов

1.3.3. Преобразование полуформальной спецификации в формальную

1.3.4. Выбор подхода

Введение диссертации (часть автореферата) на тему «Специализированные модели для проектирования, разработки и реализации информационных систем»

Одним из важных факторов разработки современного программного обеспечения является формализованный подход, обеспечивающий строгое и однозначное описание требований к создаваемому программному продукту. Наилучший эффект применения формализованных средств достигается в случае их адекватного использования на всех необходимых этапах разработки, начиная от постановки задачи до этапа непосредственной реализации и внедрения программного продукта. Такой подход обеспечивает возможность компактного описания и принятия обоснованных решений по методам реализации. Основу формализованного подхода составляет построение формальной модели, с помощью которой обеспечивается не только описание соответствующих компонент программного продукта на всех этапах жизненного цикла программного обеспечения, но и проведение предварительных исследований по выбору адекватных методов разработки и реализации. В большинстве современных разработок различных приложений используются полуформальные методы (ОМТ, UML,.), основанные главным образом на графических системах обозначения (диаграмме классов, диаграмме состояний и т.п.), которые дают интуитивное представление о разрабатываемой системе. Эти методы представляют бесспорные преимущества для моделирования, создавая идеальную поддержку для общения между различными участниками системы, но в этих методах отсутствуют средства анализа и проверки спецификаций на основе формального доказательства свойств, получаемых при моделировании. Формальные методы (В, VDM, Z, CSP, CCS.), основанные на строгом математическом подходе, предоставляют возможность адекватной концептуализации и позволяют не только создавать точные конструкции, но и анализировать их. Одной из наиболее интересных работ в этом направлении является теория CSP-OZ, представляющая собой формализованный аппарат на основе языка Объект-Z (объектно-ориентированное расширение языка Z) для описания статических структурных аспектов систем, и теории взаимодействующих процессов CSP для спецификации динамического поведения. Однако формализм этих методов, построенный на сложных математических средствах высокого уровня является труднодоступным для понимания большинством пользователей и, как правило, создает серьезные проблемы на этапе практической реализации моделей. Поэтому задача интеграции традиционных полуформальных методов с формальными представляется весьма актуальной. Опыт соответствующих разработок в этой области показывает, что универсальные подходы к решению указанной выше задачи не дают желаемых результатов и наибольший эффект достигается на пути построения специализированных систем моделирования.

Цель работы

Основной целью диссертационной работы является методология построения специализированной модели, ориентированной на разработку информационных систем, на основе соединения средств описания диаграмм UML с формальным аппаратом теории CSP-OZ. Такое соединение дает интуитивное и визуальное представление от графических обозначений с одной стороны, а с другой стороны точность и возможность анализировать и доказывать свойства полученных спецификаций на основе формальных методов. Предлагаемый подход демонстрируется на примере системы управления и резервирования авиабилетов, входящей в группу информационных систем. Кроме этого рассматривается методика реализации спецификаций теории CSP-OZ средствами системы SQL.

Методы исследования

В работе используются язык графического описания для объектного моделирования UML (унифицированный язык моделирования) и теория CSP

Введение 7

0Z, которая является комбинацией теории взаимодействующих процессов CSP, и языка Объект-Z (объектное расширение языка формальной спецификации Z).

Научная новизна

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

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

3. Построение демонстрационной модели на примере системы управления и резервирования авиабилетов с целью обоснования работоспособности предлагаемых в диссертации средств и методов.

4. Создание интегрированной среды разработки информационных систем, обеспечивающих реализацию моделей информационных систем на основе SQL средств.

Практическая ценность результатов

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

На защиту выносятся

1. Специализированная среда моделирования информационных систем на основе интеграции полуформальных методов с формальными методами.

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

3. Демонстрационная модель на примере системы управления и резервирования авиабилетов.

4. Интегрированная среда разработки информационных систем, обеспечивающая реализацию моделей информационных систем на основе SQL средств.

Связанные работы

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

- [1,2] - получение формальных спецификаций в Z из объектной модели Fusion;

- [3,4] - получение формальных спецификаций в Z из диаграммы классов UML;

- [5] - получение формальных спецификаций в В из моделей вида сущность-связь;

- [6,7,8] — перевод объектно-ориентированных моделей в формальные спецификации в В;

- Подход UML-B [9,10] позволяет формализовать полуформальные описания диаграмм классов UML, используя формальный язык спецификации В.

Введение 9

- [11] - перевод моделей ОМТ в формальные спецификации в В;

- [12,13,14] - получение формальных спецификаций в В, Z ++ или VDM++ из объектно-ориентированных моделей;

- [15]- предлагает методы, используемые в Fusion и Объект-Z;

- [16] - устанавливается связь диаграмм классов UML с классами Объект-Z.

- Подход UML-EB3 [17], позволяющий переводить UML в ЕВЗ "Entity-Based Black-Box" - формальный язык спецификации, Для описания главных функциональных возможностей информационных систем, синтаксис языка ЕВЗ заимствует основные средства CSP [18], CCS [19] и LOTOS [20].

1.6.5. Выводы.

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

С другой стороны, если спецификация динамических свойств становится легче при использовании языков спецификаций, основанных на событиях, как CSP, CCS и ЕВЗ, то спецификация статических аспектов, напротив становится труднее.

В нашей работе представляется подход для проектирования и разработки информационных систем на основе соединения средств описания диаграмм UML с формальным аппаратом теории CSP-OZ, представляющей собой комбинацию двух формальных языков CSP и Объект-Z позволяющих таким образом достаточно адекватно описывать оба аспекта информационных систем (статический и динамический).

Заключение диссертации по теме «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей», Бендума Тахар

ЗАКЛЮЧЕНИЕ

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

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

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

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

1. R. France, J. M. Bruel. M. Larrondo-Petrie. An Integrated Object Oriented and Formal Modeling Environment. Journal of Object Oriented Programming, pages: 25-34. November/ December 1997.

2. M. Shroff, R. B. France, Towards a Formalization of UML Class Structures in

3. Z, In 21st International Computer Software and Applications Conference -COMPSAC'97. Washington. USA. IEEE Computer Society. 1997.

4. N. NAGUI-RAISS. A Formal Software Specification Tool using the Entity

5. Relationship Model, Proceeding of the 13th International Conference on the Entity-Relationship Approach, LNCS, Springer-Verlag, Manchester, RU, Decembre 1994.

6. P. Facon, R. Laleau. Des modeles d'objets aux specifications formelles ensemblistes. Ingenierie des systemes d'informations. 4(2), pages: 275239. 1996.

7. P. Facon, R. Laleau, Н.Р. Nguyen. Mapping Object Diagrams into В specifications. In A.Brayant and L.Semmens. editeur. Method Integration Workshop. Electronic Workshop in Computing. Leeds. March 1996. Springer Verlag.

8. H.P. Nguyen. Derivation de specifications formelles В a partir de specificationssemi-formelles. PhD thesis. Conservatoire National des Arts et Metiers. 1998

9. A. Mammar. Un environnement formel pour le developpement d'applications base de donnees. PhD thesis, CNAM, France, 2002.

10. E. Meyer, J. Souquieres. A Systematic Approach to Transform OMT Diagrams to а В Specification. In FM'99, volume 1708 of LNCS, pages: 875-895. Toulouse, France, 20-24 September 1999. Springer-Verlag.

11. K. Lano. Formal object-oriented development. Springer. 1995.

12. K. Lano, S. Goldsack. Integrated Formal and Object-Oriented Methods : The VDM++ Approach, A. Bryant & L.Seemmens Editor, Springer Verlag, Method Intergration Workshop, Leeds, RU, Mars 1996.

13. K. Lano, H. Haugthon, P. Wheeler. Integrated Formal and Structured Methods in Object Oriented System Development. In Formal Methods and Object technology. Chapitre 7. Springer. 1996.

14. М. Frappier, R. St-Denis. ЕВЗ: an entity-based black-box specification method for information systems. Software and Systems Modeling, 2(2), pages: 134149, July 2003.

15. C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.

16. R. Milner. Communication and Concurrency. Prentice-Hall, 1989.

17. T. Bolognesi, E. Brinksma. Introduction to the ISO specification language LOTOS. Computer Networks and ISDN Systems, 14(1), pages: 25-59. 1987.

18. M.D. Fraser, K. Kumar, V. Vaishnavi. Strategies for incorporating formal specifications in software development. Communications of the ACM, 37(10), pages: 74-84, October 1994.

19. P. Chen. The entity-relationship model Toward a unifying view of data. ACM Transactions on Database Systems, 1(1). Pages: 9—36, March 1976.

20. D. Marca, C. McGowan. SADT: Structured Analysis and Design Technique. McGraw-Hill, New-York, 1988.

21. G. Booch, I. Jacobson, J. Rumbaugh. The Unified Modeling Language— User Guide. Addison-Wesley, 1998.

22. J. L. Peterson. Petri nets. ACM Computing Surveys, 9(3). pages: 223-252, 1977.

23. P.Caspi, N. Halbwachs, D. Pilaud, J. Plaice. LUSTRE, a declarative language for programming synchronous systems. Dans 14th Symposium on Principles of Programming Languages (POPL 87), Munich, pages: 178-188. ACM, 1987.

24. J.M. Spivey. The Z notation: a Reference Manual. Prentice-hall International, 1992.

25. M.D. Fraser, K. Kumar, V. Vaishnavi. Informal and Formal Requirement Specification Languages: Bridging the Gap. IEEE Transactions on Software Engineering, 17(5), pages: 454-465, Mai 19911. Список литературы 88

26. J.P. Giraudin. Evolution de la modelisation des systemes d'information. Dans EC2 et Cie, editeur, 8me Journees Internationales on Software Engineering and its applications, Paris, Novembre 1995.

27. E.Yourdon, L.L. Constantine. Structured Design. Prentice-Hall, 1979.

28. M.A. Jackson. System Development. Prentice HaLL, 1983.

29. H. Tardieu, A. Rochfeld, C. Rolland. La methode Merise : Principes et Outils. Editions d'Organisation, Paris, 1983.

30. C. Rolland, O. Foucault, F. Benci. Conception des systemes d'information : La methode REMORA. Eyrolles, Paris, 1988.

31. F.Bodart, Y. Pigneur. Conception assictee des applications informatique: etude d'opportunite et analyse conceptuelle. Masson, Paris, 1983.

32. J. Rumbaugh, M. Blaha, M. Premerani, F. Eddy, W. Lorensen. Object-Oriented Modeling and Design. Prentice-hall International, 1991.

33. G. Booch. Object-Oriented Analysis and Design with Applications. Addison-Wesley. 1994.

34. I. Jacobson, M. Christerson, G. Overgaard. Object-Oriented Software Engineering A Use Case Driven Approach. Addison-Wesley, 1992.

35. D.Coleman, P. Arnold, B. Bodoff, C. Dollin, H. Gilchrist, F. Hayes, P. Jeremaes. Fusion : La methode orientee-objet de la 2e generation. Masson, 1996.

36. C. Gane, T. Sarson. Structured Systems Analysis : Tools and Techniques. Prentice-Hall, 1979.

37. P. Pellaumail. La methode AXIAL. Editions d'Organisation, 1986.

38. I. Jacobson. Object-Oriented Software Engineering A Use Case Driven Approach. Addison-Wesley, 1994.

39. P.A. Muller. Modtelisation objet avec UML. Eyrolles, 1997.1. Список литературы89

40. Groupe Technologie Objet. La technologie a objets Domaines et utilisations. Ingenierie des systemes d'informations, 3(6). pages: 739-776, 1995.

41. UML Partners. United Modeling Language version 1.1 Rapport de recherche ad/97-08-11, OMG doucument, 1997. http://www.rational.com.

42. C. Kobryn. UML 2001: a standardization odyssey. Communications of the ACM, 42(10), pages: 29-37, October 1999.

43. C. Petersohn, W. P. de Roever, C. Huizing, J. Peleska. Formal Semantics for Ward and Mellors's Transformation. Dans D. Till, editeur, 6th Refinement Workshop, Workshop in Computing, pages: 14-41. Springer-Verlag. 1994.

44. D. Harel. Statecharts : A visual formalism for complex systems. Science of Computer Programming, 8(3). pages : 231—274, 1987.

45. G. Berry, G. Gonthier. The Esterel Synchronous Programming Language : Design, Semantics, Implementation. Science of Computer Programming, 19(2). pages: 87-152, 1992.

46. Y. Gurevich. Evolving Algebras : An attempt to discover semantics. In Current Trends in Theoretical Computer Science. World Scientific, 1993.

47. R.J. Back, R. Kurki-Suonio. Decentralisation of process nets with centralised control. In 2nd ACM SIGACT-SIGOPS Symp. On Principles of Distributed Computing, pages: 131-142, 1983. Montreal, Canada, 17-19 August 1983.

48. C.B. Jones. Systematic Software Development using VDM. 2nd edition Prentice-Hall, 1990.

49. G. Smith. The Object-Z Specification Language. Kluwer Academic Publishers, 2000.

50. J.R. Abrial. The B-Book. Cambridge University Press, 1996.

51. J.L. Peterson. Petri Net Theory and the Modeling of Systems. Prentice-Hall, 1981.1. Список литературы 90

52. Т. Bolognesi, Е. Brinksma. Introduction to the ISO specification language LOTOS. Computer Networks and ISDN Systems, 14(1). pages: 25-59. 1987.

53. Sommerville. Software Engineering, 4th edition. Addison Wesley, 1992.

54. H. Habrias. Les specifications formelles pour les systemes d'information: Quoi? Pourquoi ? Comment ? Ingenierie des systemes d'information, 3(2), pages: 205-253, 1995.

55. Ковалёв С. П. Применение формальных методов для обеспечения качества вычислительных систем // Вестник Новосибирского государственного университета. Серия математика, механика, информатика". 2004. Т. IV, № 2. С. 49-74.

56. P. Andre. Methodes formelles et a objet pour le developpement du logiciel: etudes et propositions. PHD thesis, Universite de Rennes, Juillet 1995.

57. A. Hall. Seven myths of formals methods. IEEE Software, Septembre 1990.

58. J. Bowen, M. Hinchey. Seven more myths of formals methods. IEEE Software, pages: 34-41, Juillet 1995.

59. J. Dick, J. Loubersac. Integrating Structured and Formal Methods: a visualjapproach to VDM, 3 International Conference ESEC'91, pages: 37-59. Milan, October 1991, Springer-Verlag.

60. A. Malioukov. An Object-Based Approach to the В Formal Method, B'98 : Recent Advances in the Development and Use of the В Method, 2nd International В Conference, Montpelier, France, April 1998, LNCS n° 1393.

61. D. Jackson. Alloy : lightweight object modelling notation. http://sdg.lcs.mit.edu/publications.html, Juillet 1999.

62. P. Facon, R. Laleau. Des specifications informelles aux specifications formelles : compilation ou interpretation?, Actes du 13ёте congres INFORSID, Grenoble, Juin 1995.

63. К. Lano, Н. Haugthon, Improving the Process of System Specification and Refinement in B, 6th Refinement Workshop, D. TILL Editor, Springer-Verlag, Workshops in Computing, 1994.

64. N. Hadj-Rabia, H. Habrias. Formal specification from NIAM model: A Bottom Up Approach, IS CIS XI (11th International Symposium on Computer and Information Sciences), 6-8 Novembre 1996, Antalya, Turkey.

65. R. B. France, J. M. Bruel, M. M. Larrondo-Petrie, E. Grant, Rigorous Object-Oriented Modeling : Integrating Formal and Informal Notations, Proceedings of the 6th International AMAST Conference, Decembre 1997.

66. M. Shroff, R. B. France, Towards a Formalization of UML Class Structures in Z, In 21s' Lnternational Computer Software and Applications Conference -COMPSAC'97. Washington. USA. IEEE Computer Society. 1997.

67. P. G. Larsen, N. Plat, H. Toetenel, A Formal Semantics of Data Flow Diagrams, Formal aspects of computing, vol.6-n°6, pages: 586-606. December, 1994.

68. Бендума Т. Специализированные объектно-ориентированные модели программных систем// Системы управления и информационные технологии. Научно-технический журнал №4.1(34). Воронеж: Изд-во «Научная книга», 2008. - С. 155-159. ISSN 1729-5068.

69. Бендума Т. Специализированные объектно-ориентированные модели программных систем// Информационные технологии моделирования и управления. Международный научно-технический журнал № 1(53). -Воронеж: Изд-во «Научная книга», 2009. С. 52-59. ISSN 1813-9744

70. Бендума Т. Специализированная Модель для Разработки Приложений Баз Данных на Основе Комбинации UML и CSP-OZ. // Актуальные проблемы гуманитарных и естественных наук. №6 Июнь 2009, Москва. С. 40-50.ISSN 2073-0071.

71. Бендума Т. Комбинация средств UML и CSP-OZ для разработки приложений баз данных. // Молодой ученый. №7, Июль 2009. С.37-48. Чита. ISSN 2072-0297.

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

73. C.A.R. Hoare, Communicating sequential processes, САСМ 21. pages: 666677. 1978.

74. S.D. Brookes, C.A.R. Hoare, A.W. Roscoe, A theory of communicating sequential processes, Jo urnal of the A CM 31, pages: 560-599. 1984.

75. A. W. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall, 1997.1. Список литературы 93

76. J. Woodcock, J. Davies, Using Z-Specification, Refinement, and Proof, Prentice-Hall, 1996.

77. J. R. Abrial. Manuel du language Z (Z/13). Rapport de recherche. Electricite de France. 1977.

78. G. Smith. The Object-Z Specification Language. Advances in Formal Methods. Kluwer Academic Publishers, 2000.

79. R. Duke, G. Rose, G. Smith, Object-Z: A specification language advocated for the description of standards, Computer Standards and Interfaces 17,pages: 511-533.1995.

80. G. Smith, A fully abstract semantics of classes for Object-Z, Formal Aspects of Computing 7, pages: 289-313. 1995.

81. C. Fischer, G. Smith, Combining CSP and Object-Z: Finite or infinite trace-semantics? in: T. Mizuno, N. Shiratori, T. Higashino, A. Togashi (Eds.), Proceedings ofFORTE/PSTV'97, Chapmann & Hall, page: 503-518, 1997.

82. C. Fischer. CSP-OZ: A combination of Object-Z and CSP. In H. Bowmann and J. Derrick, editors, Formal Methods for Open Object-Based Distributed Systems (FMOODS '97), volume 2, pages: 423-^138. Chapman & Hall, 1997.

83. C. Fischer, H. Wehrheim, Model-checking CSP-OZ specifications with FDR, in: K. Araki, A. Galloway, K. Taguchi (Eds.), Integrated Formal Methods, Springer, pages: 315-334. 1999.

84. C. Fischer, Combination and Implementation of Processes and Data: From CSP-OZ to Java. Ph.D. Thesis, Bericht Nr. 2/2000, University of Oldenburg, April 2000.

85. Ernst-Rtidiger Olderog, Heike Wehrheim: Specification and (property) inheritance in CSP-OZ. Science of Computer Programming. 55(1-3). Pages: 227-257. (2005).

86. Буч Г., Якобсон А., Рамбо Дж. UML. Классика CS-2-изд./ Пер.с англ.; Под общей редакцией проф. С.Орлова СПб.: Питер, 2006. -736 с.1. Список литературы ^-94

87. OMG. Unified Modeling Language Specification, BetaRl Release. "Object Management Group., April 1999.

88. Дейт К. Введение в системы баз данных / Пер. с англ. 8-е изд. — М.: Издательский дом "Вильяме", 2006. — 1328 е.: ил. — Парал. тит. англ. ISBN 5-8459-0788-8 (рус.).

89. Бен Форта. Освой самостоятельно язык запросов SQL / Пер. с англ. — 3-е изд. — М.: Диалектика, 2005. — 288 с. ISBN 5-8459-0827-2.98. http://www.visual-paradigm.com/product/vpuml/.

90. Кватрани Т. Rational Rose 2000 и UML Визуальное моделирование: Пер. с англ. -М.: ДМК Пресс, 2001. — 176 с. ISBN: 5-94074-131-2