1. Введение.
В большинстве современных разработок различных приложений баз данных используются полуформальные методы (OMT, UML,…) [1], основанные главным образом на графических системах обозначения (диаграмме классов, диаграмме состояний,…), которые дают интуитивное представление о разрабатываемой системе. Эти методы представляют бесспорные преимущества для моделирования, создавая идеальную поддержку для общения между различными участниками системы, но в этих методах отсутствуют средства анализа и проверки получаемых спецификаций на основе формального доказательства свойств, получаемых при моделировании. Формальные методы (B, VDM, Z, CSP, CCS...) [2,3,4], основанные на строгом математическом подходе, предоставляют возможность адекватной концептуализации и позволяют не только создавать точные конструкции, но и анализировать их. Формальные методы можно разделить на: ориентированные на описание статических аспектов (B, Z, VDM,…), и ориентированные на описание динамических аспектов (CSP, CCS,…). Более актуальным представляется подход, основанный на комбинации статических аспектов с динамическими. Одной из наиболее интересных работ в этом направлении является CSP-OZ [5], представляющая собой формализованный аппарат на основе языка Object-Z (объектно-ориентированное расширение языка Z) для описания статических структурных аспектов систем и теории взаимодействующих систем CSP для спецификации динамического поведения.
В работе предлагается один из подходов к построению специализированной модели для разработки приложений баз данных, основанный на соединении средств описания диаграмм UML [1] с формальным аппаратом CSP-OZ. Предлагаемый подход демонстрируется на реляционной модели данных. Такое соединение дает интуитивное и визуальное представление от графических обозначений с одной стороны, а с другой стороны, точность и возможность анализировать и доказывать полученные спецификации на основе формальных методов. Кроме этого рассматривается методика реализации спецификаций теории CSP-OZ средствами SQL.
2.Основные понятия теории CSP-OZ.
2.1. CSP (теория взаимодействующих процессов) используется для описания динамических аспектов (поведения) систем на основе событийно-управляемого подхода [4,6,7]. Центральными понятиями теории являются синхронное взаимодействие через каналы между различными процессами, параллельная композиция и механизм сокрытия внутренних точек взаимодействия.
В CSP процессы определяются как:
Pr::= Fail½Skip½c→P½ P/s ½P\A½P;Q½P□Q½PPQ½PΔQ½X ½P|||Q½PQ.
Fail – пустой процесс, который “ничего не делает”, а процесс Skip также “ничего не делает”, но в отличие от процесса Fail завершает свою работу успешно. (c→P) трактуется как процесс активации события c, после которого запускается процесс P; (P/s) (P после s) –поведение процесса P после выполнения следа s, представляющего собой последовательность событий; (P\A) - сокрытие событий, принадлежащих множеству A, например: ( a→b→c→P)\{a, c}=(b→P); (P;Q) – операция последовательной композиции процессов P и Q (сначала выполняется процесс P, а затем процесс Q, при условии нормального завершения процесса P; (P□Q) – операция альтернативной композиции процессов P и Q (трактуется как P или Q); процесс (PPQ) представляет собой внутренний недетерминированный выбор, который может вести себя либо как P, либо как Q, без влияния окружающей среды (например, пользователь или другой процесс); в альтернативной же композиции P□Q, поведение процесса полностью определяется взаимодействием с окружающей средой; (PΔQ) – это тоже вид последовательной композиции, но в отличие от процесса P;Q процесс PΔQ ведет себя как P до тех пор, пока выполнение P не будет заблокировано, после чего процесс P останавливается и PΔQ ведет себя как Q (interrupt), обычно процесс Q в этом случае - это процесс перезагрузки или восстановления после блокировки; (μX:A.F(X)) – обозначение рекурсивного определения процесса X, где A–алфавит процесса X, то есть множество событий процесса X, (предполагается, что уравнение X=F(X) имеет единственное решение в алфавите А), например: Часы = (тик → Часы); ||| обозначает параллельную композицию без синхронизации, а обозначает параллельную композицию с синхронизацией на всех событиях множества B, то есть события из множества B представляют общие точки взаимодействия параллельных процессов.
Для передачи данных от одного процесса к другому в теории CSP используются каналы передачи данных. Вводятся две операции: c!m -операция передачи сообщения m через канал c, а c?x - операция приема сообщения из канала с в переменную x . В теории CSP рассматривается случай синхронного взаимодействия процессов, который предусматривает одновременное выполнение операций c!m и c?x. Таким образом, одновременное выполнение этих операций позволяет трактовать его как единое неделимое событие взаимодействия процессов. Последнее определяется следующим соотношением:
(c!m→P) || (c?x→F(x)) = (c→(P||F(m)), где событие c определяет точку взаимодействия параллельных процессов.Таким образом, все события, являющиеся общими для параллельно выполняемых процессов, определяют точки взаимодействия этих процессов.
Средствами CSP можно определить широкий спектр процессов, составляющих основу модели поведения.
2.2. Zи Object-Z. Z является формальным языком спецификаций, используемым для описания и моделирования вычислительных систем [3,8]. Спецификация в Z обычно включает в себя схемы состояний и операций. Схемы состояний группируют переменные, и определяют отношения между их значениями. Схемы операций определяют отношения между значениями переменных 'до' и 'после' выполнения операции.
Рис 1. Вертикальная форма схемы.
Схемы операций отличаются от других схем тем, что они имеют в своем составе еще и ∆-список для выделения переменных, значения которых могут измениться при применении операций.
Object -Z – это объектно-ориентированное расширение Z, основным элементом которого является схема класса; Класс включает в себя определение локальных типов и констант, одну схему состояния и связанную с ней схему инициализации состояния со всеми схемами операций [9,10,11].
Рис 2. Основная структура класса OZ.
2.3 CSP-OZ.
Теория CSP-OZ [5,12,13,14] построена на основе комбинирования теории Object -Z с теорией CSP. Спецификация CSP-OZ описывает систему как множество взаимодействующих объектов, каждый из которых задается описанием структуры и поведения. Взаимодействие между объектами выполняется через каналы аналогично взаимодействию процессов в теории CSP. Класс CSP-OZ имеет следующую структуру:
Рис 3. Основная структура CSP-OZ класса.
Описание каналов определяет интерфейс класса. Описание задается в виде Channel c: [p1:ty1; …; pn:tyn], где c - название канала, p1, …, pn - названия параметров, ty1,…,tyn - типы параметров.
CSP-часть представлена в форме уравненийвида CSP-название = CSP-процесс. Каналы каждого процесса в CSP-части должны принадлежать множеству каналов, объявленных в интерфейсе. В CSP-части должен быть определен процесс main (стартовый процесс, с которого начинается работа). Этот процесс используется для определения семантики CSP-части.
В Z-часть включаются определения типов и констант, схема состояния и схема инициализации состояния (то же самое, как в Объект-Z). Схемы и имена переменных, используемые в Z-части, должны быть связаны с названиями, которые используются в CSP-части.
Чтобы связать схемы операций Z с поведением, используются специальные ключевые слова enable и effect, где enable – определяет условия, при которых можно применить операцию, effect - определяет соответствующий переход из одного состояния в другое.
В следующем разделе рассмотрим более подробно предлагаемый метод, основанный на соединение CSP-OZ с UML для получения спецификации, подлежащей проверки и анализу, а также легко реализуемой на языках программирования.
3. Предлагаемый метод.
Метод, предлагаемый здесь, включает в себя следующие представленные ниже этапы (см. Рис.4).
а) Моделирование в UML: данные и средства обработки данных представляются диаграммами UML, специализированными для описания информационных систем (диаграммы классов, диаграммы состояния и диаграммы сотрудничества).
б) Генерация спецификаций реляционной модели из диаграмм UML, определенных на предыдущем этапе, в спецификацию CSP-OZ. Диаграммы UML не имеют строгой формализации семантики, поэтому цель этого этапа (перевод в CSP-OZ) заключается в соответствующей формализации. Полученная спецификация CSP-OZ состоит из трех главных компонентов: всех данных представляющих состояние системы, всех базовых операций, и наконец, всех каналов интерфейса, использующих базовые операции и обеспечивающих взаимодействие системы с другими компонентами (программами или другими системами).
в) Создание кода SQL: на этом этапе создается код, соответствующий полученной спецификации CSP-OZ. Этот этап кодирования позволяет определить схему базы данных и связанные базовые операции в SQL (вставка, удаление, и т.д.) с одной стороны, а с другой стороны, определить классы на языке программирования, позволяющие эффективную реализацию средств обработки в базе данных.
Рис.4.
4. Перевод диаграмм UML в CSP-OZ.
В этом разделе рассматривается методика преобразования диаграмм UML в соответствующие спецификации в CSP-OZ. Методика демонстрируется с помощью примеров.
4.1. Алгоритм преобразования диаграммы классов в реляционную схему.
Процесс преобразования построен на основе классического алгоритма перевода из концептуальной модели данных в реляционную модель [19].
Он состоит из следующих основных этапов:
- все классы в диаграмме классов преобразуются в таблицы;
- отношения «многие к одному» (и «один к одному») становятся внешними ключами, т.е. образуется копия уникального идентификатора класса на конце связи «один», и соответствующие столбцы составляют внешний ключ таблицы, соответствующей классу на конце связи «многие»;
- для построения отношения «многие ко многим» между классами A и B создается дополнительная таблица, имеющая помимо ее собственных атрибутов, еще два столбца, один из которых содержит уникальные идентификаторы класса A, а другой – уникальные идентификаторы
класса B.
Пример:
Рис 5. Диаграмма классов “Университет”.
PROF ≙ [ProfID :PROFID; ProfName :STRING; PrDepNum : DEPNUM].
DEPT ≙ [DepNum : DEPNUM; ChairDep : PROFID;NbPrf: NBPRF].
CRS ≙ [CrsNum : CRSNUM; CrDepNum: DEPNUM].
PRF-CRS ≙ [ProfID : PROFID; CrsNum : CRSNUM;Schedule: SCHEDULE; Term: TERM].
4.2. Статический аспект (Диаграмма классов).
Для получения формального описания структуры базы данных из диаграммы классов необходимо выполнить следующие этапы:
4.2.1.Определение доменов в Z. В реляционной модели, домен каждого атрибута должен быть атомарным (неделимым).
STUDENT_ID = = Integer
STUDENT_Name = = String
AGE = = {a: Integer ● 15<a <80}.
SEX == Male | Female.
4.2.2. Определение атрибутов и кортежей.
Все атрибуты перечисляются как переменные в части декларации схемы кортежа (строки), а все статические ограничения атрибута (если они есть) перечисляются как постоянные предикаты в части предикатов схемы REL.
Рис 6. Схема кортежа в Z.
Пример:
Рис 7. Схема кортежа “профессора” в Z.
4.2.3. Определение отношений (таблицы).
В части декларации схемы отношения определяется конечное множество всех кортежей этого отношения, а в части предикатов определяется первичный ключ (с помощью предиката уникальности) и все атрибуты, которые не могут иметь свойство Null-Значение (с помощью оператора REQUIRED).
Рис 8. Схема отношения в Z.
Пример:
Рис 9. Схема отношения “профессор кафедры” в Z.
4.2.4. Определение схемы состояния базы данных.
Схема группирует все определения базы данных, включая все схемы отношений в части декларации, а в части предикатов определяются все внешние ключи (с помощью предиката) и динамические ограничения (если они есть).
Рис 10. Схема состояния базы данных в Z.
Пример:
Рис 11. Схема состояния базы данных “Университет” в Z.
Отметим, что последний предикат определяет, что число профессоров кафедры (NbPrf) является производным атрибутом.
4.2.5. Определение схемы инициализации базы данных.
Схема инициализации состояния базы данных определяет начальное состояние базы данных, показывая, что все ее отношения пустые.
Пример:
Рис 12. Схема инициализации состояния DB в Z.
4.2.6. Определение базовых операций.
Список базовых операций диаграмм классов UML включает в себя такие операции, как вставка, обновление и удаление.
а) Вставка.
В декларативной части схемы операции вставки (Insert_rel) объявляются новые переменные ΔRelat и new_rel, где Relat это отношение (таблица) к которой хотим добавить новый кортеж new_rel. (здесь Δ обозначает, что значение отношения или таблицы Relat изменится при выполнении операции). В части предикатов определяется следующее состояние отношения Relat с помощью операции объединения в Z.
Рис13. Схема операции вставки в Z.
Пример.
Рис 14. Схема операции вставки в Z (пример).
Б) Удаление.
При выполнении операций удаления (а также модификации) базы данных применяются стратегии поддержания ссылочной целостности, представленные в книге Дейта [16]:
• CASCADE (КАСКАДНОЕ УДАЛЕНИЕ) - выполняет удаление кортежа, а также выполняет каскадное удаление всех тех кортежей в дочернем отношении, которые ссылаются на удаляемый кортеж.
Рис 15. Схема каскадного удаления в Z.
• RESTRICT (ОГРАНИЧЕННОЕ УАЛЕНИЕ) - не разрешает удаление, если имеется хотя бы один кортеж в дочернем отношении, ссылающийся на удаляемый кортеж.
Рис 16. Схема ограничения операции удаления в Z.
• SET NULL (УСТАНОВИТЬ В NULL) - выполняет удаление кортежа, а во всех кортежах дочернего отношения, ссылающихся на удаляемый кортеж, меняет значения внешних ключей на null-значение.
Рис 17 Схема удаления с установкой в Null в Z.
Примеры.
Рис 18. Схема удаления “профессора” в Z.
Рис 19. Схема удаления “кафедры” в Z.
4.2.7. Определение класса базы данных в Object - Z.
Класс базы данных включает в себя схему состояния базы данных, схему инициализации базы данных и все схемы базовых операций.
Рис 20. Класс DBOZ для базы данных.
Пример.
Рис 21. Класс DBOZ для базы данных “Университет”.
4.3. Динамический аспект.
Динамический аспект образуется из диаграммы состояния и диаграммы сотрудничества. В CSP-OZ поведение описывается с помощью CSP. Процесс main это стартовый процесс, с которого начинается работа. Для каждой базовой операции op определяются схемы enable_op и effect_op (где enable_op описывает условия выполнения операции op, а effect_op-соответствующий переход из одного состояния в другое) и для этих операций определяются каналы, через которые одни классы могут взаимодействовать с другими классами.
Рис 22. Класс RDB.
Пример.
Рис 23. Класс RDB для базы данных “Университет”.
5. Перевод на SQL:
Полученная спецификация CSP-OZ описывает оба аспекта баз данных (структуру и поведение). Если реализацию спецификации CSP-OZ, соответствующей данным и базовым операциям, можно выполнить, используя только язык SQL, то перевод поведения (порядок выполнения, взаимодействие, манипуляции с таблицами…) требует использования языка программирования более высокого уровня (JAVA, DELPHI,C и т.д.).
Ниже рассматривается перевод (реализация) на SQL, и представляются основные этапы этого перевода.
5.1. Статический аспект.
- Каждый тип данных CSP-OZ переводится в соответствующие типы SQL. Например, типы INTEGER и STRING переводятся в INT и CHARACTER STRING(n) в SQL, где n - максимальная длина строки.
- Каждая схема отношения в CSP-OZ переводится в таблицу в SQL.
- Предикаты первичного ключа, внешнего ключа и конструкция REQUIRED переводятся в PRIMARY KEY, REFERENCES и NOT NULL.
- Статические и динамические ограничения переводятся с помощью конструкции CHECK.
5.2. Динамический аспект.
Каждая операция вставки insert_rel(NewRel) переводится в SQL как INSERT INTO relat VALUES NewRrel.
Каждая операция удаления Del_rel(DeRel) переводится в SQL как DELETE FROM relat WHERE.
Создаются классы на выбранном языке программирования (например, на JAVA, DELPHI, Visual FoxPro и т.п.) позволяющие манипуляцию с таблицами, созданными на предыдущем этапе.
Создаются классы, соответствующие спецификациям CSP-OZ, полученным из диаграмм сотрудничества и состояний (для описания поведения и взаимодействия).
Заключение
Основной целью представленной здесь модели является создание специализированной интегрированной среды разработки, ориентированной на построение различных приложений в области так называемых информационно-расчетных задач. К информационно–расчетным задачам относятся задачи компьютерной бухгалтерии, делопроизводства, статистики и т.п. В настоящее время на основе СУБД Visual FoxPro и MS SQL проводятся работы по разработке и реализации упомянутой выше интегрированной среды.
Списокиспользуемой литературы:
1. Буч Г., Якобсон А., Рамбо Дж. UML. Классика CS.2-изд./ Пер.с англ.; Под общей редакцией проф. С.Орлова – СПб.: Питер, 2006. –736 с.
2. Abrial J. R. The B-Book: Assigning Programs to Meanings. Press Syndicate of the University of Combridge, 1996. –P.779.
3. Spivey J.M. The Z Notation: A Reference Manual, 2nd edition, Prentice-Hall International Series in Computer Science, 1992. –P.158.
4. Хоар Ч. Взаимодействующие последовательные процессы: Пер. с англ. М: Мир, 1989. –264 с.
5. Fischer C. Combination and Implementation of Processes and Data: From CSP-OZ to Java. Ph.D. Thesis, Bericht Nr. 2/2000, University of Oldenburg, April 2000. –P.353.
6. Brookes S.D., Hoare C.A.R., Roscoe A.W. A theory of communicating sequential processes, Journal of the ACM 31 (1984). –P. 560–599.
7. Roscoe A. W. The Theory and Practice of Concurrency. Prentice-Hall, Published 1997, revised to 2005. –P.605.
8. Woodcock J., Davies J. Using Z-Specification, Refinement, and Proof, Prentice-Hall, 1996. –P.386.
9. Smith G. The Object-Z Specification Language. Advances in Formal Methods. Kluwer Academic Publishers, 2000. –P.160.
10. Duke R., Rose G., Smith G. Object-Z: A specification language advocated for the description of standards, Computer Standards and Interfaces 17 (1995).–P. 511–533.
11. Smith G. A fully abstract semantics of classes for Object-Z, Formal Aspects of Computing 7 (1995). –P. 289–313.
12. Fischer C., Smith G. Combining CSP and Object-Z: Finite or infinite trace-semantics? in: T. Mizuno, N. Shiratori, T. Higashino, A. Togashi (Eds.), Proceedings of FORTE/PSTV’97, Chapmann & Hall, 1997. –P. 503–518.
13. Fischer C. 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, Chapman & Hall, 1997. –P. 423–438.
14. Fischer C., Wehrheim H. Model-checking CSP-OZ specifications with FDR, in: K. Araki, A. Galloway, K. Taguchi (Eds.), Integrated Formal Methods, Springer, 1999. –P. 315–334.
15. Codd E. F. A relational model of data for large shared data banks. Communications of the ACM, 13(6) June 1970. –P. 377-387.
16. Дейт К. Введение в системы баз данных, 8-е издание.: Пер. с англ. — М.: Издательский дом "Вильяме", 2005. –1328 с.: ил. - Парал. тит. англ. ISBN 5-8459-0788-8 (рус.)
17. Кузнецов С.Д. Введение в системы управления базами данных //СУБД. – 1995. - №1,2,3,4, 1996. - №1,2,3,4,5.
18. Джексон Г. Проектирование реляционных баз данных для использования с микро-ЭВМ Пер. с англ. М.: Мир, 1991. – 252 с.
19. Batini, Ceri, Navathe. Conceptual Database Design: An Entity Relationship Approach, the Benjamin/Cummings Publishing Company, 1992. –P.470.