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

п

На правах рукописи

Бендума Тахар

Специализированные модели для проектирования, разработки и реализации информационных систем

Специальность: 05.13.11 - математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей.

Автореферат

диссертации на соискание ученой степени кандидата физико-математических наук

Казань - 2009 0034895 18

003489518

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

Научный руководитель: Кандидат физико-математических наук,

доцент Казанского государственного университета Еникеев Арслан Ильясович

Официальные оппоненты: 1. Доктор физико-математических наук,

профессор Казанского государственного университета, Елизаров Александр Михайлович.

2.Кавдвдат физико-математических наук, доцент Татарского государственного гуманитарно-педагогического университета, Гайфуллин Рашид Рахматуллович

Ведущая организация: Казанский государственный технический

университет им. А.Н. Туполева

Защита диссертации состоится 21 Января 2010г. в 17:00 на заседании диссертационного совета Д. 212.081.24 при Казанском государственном университете им. В.И. Ульянова-Ленина по адресу: 420008, г. Казань, ул. Кремлевская, Д.18, конференц-зал научной библиотеки им. Н.И.Лобачевского.

С диссертацией можно ознакомиться в научной библиотеке им. Н.И. Лобачевского Казанского государственного университета. Автореферат диссертации опубликован на сайте ГОУ ВПО «КГУ» (www.ksu.ru).

Автореферат разослан « ЛЧ »декабря 2009 г. Учёный секретарь диссертационного Совета Д 212.081.24 при, КГУ, кандидат физико-математических наук, доцент^-^^/^г

А.И.Еникеев

Общая характеристика работы

Актуальность темы исследования.

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

\

\

Цель работы.

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

Перечень решаемых задач.

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

2. Создание специализированных средств моделирования информационных систем на основе соединения средств описания диаграмм UML с формальным аппаратом теории CSP-OZ.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Апробация работы.

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

• XV Международная конференция « Проблемы Теоретической

Кибернетики » (Казань, Россия, 2-7 июня, 2008), Казань, Июнь 2008.

• 27 ème congrès INFORSID2009, section Jeunes Chercheurs, (du 26 au

29 Mai 2009 à Toulouse), Toulouse- France, Mai 2009.

• Итоговые научные конференции Казанского государственного

университета.

Публикации.

По теме диссертации опубликовано 6 работ, в том числе 1 - в журнале, входящем в Перечень ВАК РФ.

Структура и объем работы.

Диссертация состоит из введения, пяти глав, заключения и списка использованной литературы из 99 наименований, включая работы автора. Объем диссертации составляет 94 страниц машинописного текста.

Краткое содержание работы

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

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

Во второй главе приводится обзор используемых методов: теории СБР-ОЪ и языка ЦМЬ. Основное внимание в этой главе уделяется предлагаемому в диссертации подходу к разработке информационных систем, Подход включает в себя следующие представленные ниже этапы (см. Рис.1):

а) Моделирование в иМЬ: данные и средства их обработки представляются диаграммами иМЬ, специализированными для описания информационных систем (диаграммы классов, диаграммы состояния и диаграммы сотрудничества).

б) Генерация спецификаций из диаграмм иМЬ, определенных на предыдущем этапе, в соответствующие спецификации СБР-Ог. Диаграммы ЦМЬ не имеют строгой формализации семантики, поэтому цель этого этапа (перевод в С8Р-02) заключается в соответствующей формализации. Полученная спецификация СБР-Ог состоит из трех главных компонентов: всех данных, представляющих состояние системы, всех базовых операций, и наконец, всех каналов интерфейса, использующих базовые операции и обеспечивающих взаимодействие системы с другими компонентами (программами или другими системами).

в) Реализация: на этом этапе создается код, соответствующий полученной спецификации СБР-С^. Этот этап кодирования позволяет определить схему базы данных и связанные базовые операции (вставка, удаление, и т.д.) с одной стороны, а с другой стороны, определить классы на языке программирования, позволяющие эффективную реализацию средств обработки данных.

Рис.1. Иллюстрация метода.

Этот подход основан на переводе графических спецификаций иМЬ в формальные спецификации СБР-Ог.

Формальные методы разделяются на: основанные на состояниях, и основанные на событиях.

Формальные методы, основанные на событиях, ориентированы на описание динамических аспектов системы, а формальные методы, основанные на состояниях, предназначены для описания структурных аспектов системы и средств обработки структур данных.

К методам, основанным на событиях, относится СБР (теория взаимодействующих процессов), а к методам, основанным на состояниях, относится Объект^ (объектно-ориентированное расширение языка 2).

Теория СБР-С^ является результатом интеграции языка Объект^ с теорией СЭР. Спецификация СБР-Ог описывает систему, как множество взаимодействующих объектов, каждый из которых задается описанием структуры и поведения. Взаимодействие между объектами выполняется через каналы аналогично взаимодействию процессов.

• Основные понятия теории CSP-OZ.

Теория СБР-Ог представляет собой формализованный аппарат, построенный на основе теории взаимодействующих систем СБР для спецификации динамического поведения и языка Объект-2 (объектно-ориентированное расширение языка Ъ) для описания статических структурных аспектов систем.

• CSP (теория взаимодействующих процессов).

Теория CSP используется для описания динамических аспектов (поведения) систем на основе собьггийно-управляемого подхода. Центральными понятиями теории являются синхронное взаимодействие через каналы между различными процессами, параллельная композиция и механизм сокрытия внутренних точек взаимодействия.

В CSP процессы определяются как:

Pr::= Fail | Skip I с->Р | P/s | Р\А I P;Q [ PaQ \ PY1Q | PAQ[x I P\\\Q (Р |[ Q.

А

Fail - пустой процесс, который "ничего не делает", а процесс Skip также "ничего не делает", но в отличие от процесса Fail завершает свою работу успешно, (с—*Р) трактуется как процесс активации события с, после которого запускается процесс Р; (P/s) (Р после s) -поведение процесса Р после выполнения следа s, представляющего собой последовательность событий; (Р\А) - сокрытие событий, принадлежащих множеству А, например:

( a-^b-+c—*P)\{a, c}=(b-+P)\ (P;Q) - операция последовательной композиции процессов Р и Q (сначала выполняется процесс Р, а затем процесс Q, при условии нормального завершения процесса Р; (PaQ) - операция альтернативной композиции процессов Р и Q (трактуется как Р или Q); процесс (РП0 представляет собой внутренний недетерминированный выбор, который может вести себя либо как Р, либо как Q, без влияния окружающей среды (например, пользователь или другой процесс); в альтернативной же композиции PaQ, поведение процесса полностью определяется взаимодействием с окружающей средой; (PAQ) - это тоже вид последовательной композиции, но в отличие от процесса P;Q процесс PAQ ведет себя как Р до тех пор, пока выполнение Р не будет заблокировано, после чего процесс Р останавливается и PAQ ведет себя как Q (interrupt), обычно процесс Q в этом случае - это процесс перезагрузки или восстановления после блокировки; (pX:A.F(XJ) - обозначение рекурсивного определения процесса X, где Л-алфавит процесса X, то есть множество событий процесса X, (предполагается, что уравнение X-F(X) имеет единственное решение в алфавите А), например: Часы = (тик —> Часы); ||| обозначает параллельную композицию без синхронизации, а || обозначает параллельную композицию с

в

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

(с!т-*Р) || (с?х—>Р(х)) = (с-»(Р||Дт)), где событие с определяет точку взаимодействия параллельных процессов. Таким образом, все события, являющиеся общими для параллельно выполняемых процессов, определяют точки взаимодействия этих процессов.

Средствами СЭР можно определить широкий спектр процессов, составляющих основу модели поведения.

• Ъ и Объект-^

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

_ Название_

——---Название = [Декларации | Предикаты]

Предикаты „ ,

- — - б) Горизонтальная форма схемы

а) Вертикальная форма схемы.

Рис.2. Представления схем операций

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

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

р. название класса___

Определения типов Определения констант Схема состояния Схема инициализации состояния Схемы операции

Рис.3. Основная структура класса OZ.

• CSP-OZ.

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

натсание класса_■______

Chan хазеание_тнала:.. [QiücatiueKamwe]

main =... [CSP часть]

Охрсдаекия mur.as и ючсташ [OZ часть] Схема состояния и инициализации состояния Схемы операции

Рис.4. Основная структура CSP-OZ класса

Описание каналов определяет интерфейс класса. Описание задается в виде Channel с: [pi'.iyy, ...; p„:ty„], где с - название канала, ptt ..., р„ - названия параметров, tyK...,tyn - типы параметров.

CSP-часть представлена в виде CSP-название = CSP-процесс. Каналы каждого процесса в CSP-части должны принадлежать множеству каналов, объявленных в интерфейсе. В CSP-части должен быть определен процесс main (стартовый процесс, с которого начинается работа). Этот процесс используется для определения семантики CSP-части.

В Z-часть включаются определения типов и констант, схема состояния и схема инициализации состояния (то же самое, как в Объект-Z). Схемы и имена переменных, используемые в Z-части, должны быть связаны с названиями, которые используются в CSP-части.

Чтобы связать схемы операций Z с поведением, используются специальные ключевые слова enable и effect, где enable - определяет условия, при которых можно применить операцию, effect - определяет соответствующий переход из одного состояния в другое.

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

Третья глава описывает предложенный в диссертации метод моделирования и правила перевода графической спецификации UML

в формальную спецификацию CSP-OZ.

Механизм перевода из UML в CSP-OZ включает в себя две основные части: перевод статических аспектов в Объект-Z и перевод динамических аспектов в CSP.

а) Статический аспект.

Классы.

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

такими как атрибуты, операции и отношения с другими объектами. Эта интерпретация характеризует семантику класса как тип. С другой стороны, когда класс интерпретируется как компонент диаграммы класса иМЬ, класс представляет ряд уже созданных до момента перевода экземпляров этого класса. Ниже приводится методика перевода классов:

• Каждый класс может тогда быть переведен в пару схем Объект^. Первая- это схема типа, которая соответствует структуре класса, а вторая-это схема таблицы, в которой объявляется набор всех экземпляров класса, используемых в соответствующей информационной системе.

• Название класса иМЬ используется для названия схемы типа, а для названия схемы таблицы добавляется префикс ТаЪ_.

• Все атрибуты класса иМЬ объявляются как переменные в части декларации соответствующей схемы типа.

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

• Кроме того, каждая операция в классе 11МЬ переводится в схему операции Объект^.

аЦ Ш2

Ор1 Ор2

ГА_

аП Ш2

К.едшгес1 аП

Ор1_

ДА

, ТаЪ_А. .4А:РА

_Ор2_ Е.4

Рис.5. Перевод класса в Объект^.

Ассоциация.

-Ассоциация «многие к одному» (и «один к одному») становятся внешними ключами, т.е. образуется копия уникального идентификатора класса на конце связи «один», и соответствующие столбцы составляют внешний ключ таблицы, соответствующей классу на конце связи «многие» (см. Рис.6);

-Для перевода ассоциации «многие ко многим» между классами А и В создается дополнительная схема Z, имеющая помимо ее собственных атрибутов, еще два атрибута, один из которых содержит уникальные

идентификаторы класса А, а другой - уникальные идентификаторы класса В (см. Рис.7).

А С в

atl at2 ш Ы2

;г 1 0.1

Opl Ор2 Opl Ор2

м

at2 btl

Required btl

\

Tab J.. AA:PA

Рис.6. Перевод ассоциации «многие к одному» (или «один к одному»).

А С В

atl м2 btl Ы2

* *

Opl Ор2 ctl ct2 Opl Ор2

-С.

ш btl

cil ct2

Required atl

Tab_C_ CC:PC

Рис.7. Перевод ассоциации «многие ко многим».

Схемы классов и отношений в Объект-Z.

Каждый из классов и их отношений переводится в Объект-Z в виде пары схем (схема типа и схема таблицы), ниже следует детализация этих схем.

Схема типа. Все атрибуты класса (или отношения) перечисляются как переменные в части декларации схемы типа, а в части предикатов перечисляются все атрибуты, которые не могут иметь свойство Null-Значение (с помощью конструкции REQUIRED) и так же все статические ограничения

атрибутов (если они есть) перечисляются как постоянные предикаты в части предикатов схемы типа.

-С-

AN, :ЛТ; ANг: ЛТ2

AN,,: А Т„_

REQUIRED Щ REQUIRED ANt

REQUIRED AN,„

CS

Рис.8. Схема типа класса в Объект^.

Здесь С название класса, АЩ, АЫ2,..., АЫ„ атрибуты, АТ]г АТъ...,АТп их типы данных, и А>^ , АЫК, АИм атрибуты, которые не могут быть пустыми, и СБ статические ограничения.

Схема таблицы. В части декларации схемы таблицы определяется конечное множество всех экземпляров этого типа, а в части предикатов определяются первичный.

.ТаЪ_С-

с: Р С

Vrl, г2: rcl • rl=r2 о rl.AN¿= r2.ANK

Рис.9. Схема таблицы класса в Объект-г.

Здесь Шк первичный.

Общая схема состояния.

Схема группирует все схемы таблиц в части декларации, а в части предикатов определяются все внешние ключи и динамические ограничения (если они есть).

--,-

ТаЬ_с!а$$1

ТаЪ_с!аззд

- Tab_classi3rm. Tal>^cldssm»ri.foreign_ key=rm.p?imary^key Vi%: Tab_clqssk B-'fip Tab^ddssj • Ц Jbreign_ key =rd.primcay_key

Рис.10. Общая схема состояния.

Схема инициализации состояния.

Схема определяет начальное состояние, показывая, что все ее схемы таблиц являются пустыми.

Init_______... .,

Tab_c!arsi = {} А . Tab_c!ass] = {} л

Tab_dassg = {}

Рис.11. Схема инициализации состояния.

Схемы базовых операций.

Список базовых операций диаграмм классов UML включает в себя такие операции, как вставка, обновление и удаление.

А) Вставка.

В декларативной части схемы операции вставки объявляются новые переменные Д Tab_class и new_rel, где Tab_class это схема таблицы к которой хотим добавить новый экземпляр new_rel. (здесь Д обозначает, что значение таблицы Tab_class изменится при выполнении операции). В части предикатов определяется следующее состояние схемы Tab_class с помощью операции объединения в объект-Z.

-.Insert_

& Tab_class newRel T. С

с - с U newRel ?

Рис.12. Схема вставки.

Б) Удаление.

При выполнении операций удаления (а также модификации) базы данных применяются стратегии поддержания ссылочной целостности:

• CASCADE (КАСКАДНОЕ УДАЛЕНИЕ) - выполняет удаление экземпляра, а также выполняет каскадное удаление всех тех экземпляров в дочернем классе, которые ссылаются на удаляемый экземпляр.

Delete_

Л Tab_class dcRcl ?: С

T =={/:Tab__dasscu;j i t.foreign_key=deRefi.primary_key)

V r :2* • Del_Tab_dassCmИ

с' = с \ {deRel?}_

Рис.13. Схема каскадного удаления.

Здесь Tab_classa,nd это дочерний класс, a delRel? это экземпляр, который удаляется.

• RESTRICT (ОГРАНИЧЕННОЕ УДАЛЕНИЕ) - не разрешает удаление, если имеется хотя бы один экземпляр в дочернем классе, ссылающийся на удаляемый экземпляр.

Delete_;_■ _

A Tab_class deRel ?: С_

Г=={г. Tab_ dassc;nij | t.foreign_key = deReti primaryJcey) if Г={} then с' = с \ {¿etfei?} _ else с = с ...........

Рис.14. Схема ограничения операции удаления .

• SET NULL (УСТАНОВИТЬ В NULL) - выполняет удаление экземпляра, а во всех экземплярах дочернего класса, ссылающихся на удаляемый экземпляр, меняет значения внешних ключей на null-значение.

r Delete ____

A Tabjclass

A Tab_dassch~j deRel Т. REL

Vt Tab_class,cm I t.fireign_key = deRell.prmiary_key • i.foreigpJ<zy=Null. rel' — ret \{deRe!l}

Рис. 15. Схема, удаления с установкой в Null.

Схема класса базы данных в Объект-Z.

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

DBC?__

Tab_classL Tab_classm Tab_cla$s0 • rL.prmgn_ key =r'„primary_key • ^.foreign_ key =r&primary_key

Vrj Tab_classi 3 rm: Tabjdass? Vr;,: Tab_classk 3 r/. Tab_classd

Inti

Tab classi = {} A

Tab_class2 = {} A

Tab_classg = {}

Insert Tab class/ Delete Tab classj

Jnsert_Tab_class2 DeleteJTab_cIass2

insert Tab class*; Delete Tab classg

Рис.16. Схема класса базы данных в Объект-Z.

б) Динамический аспект.

Динамический аспект образуется из диаграммы состояния и диаграммы сотрудничества. В CSP-OZ, поведение описывается с помощью CSP части.

Правила перевода.

Начальное состояние представляет собой частный случай состояния, которое не содержит никаких внутренних действий (псевдосостояние). В этом состоянии объект находится по умолчанию в начальный момент времени.

Начальное состояние переводится в ключевое слово CSP main, как определение поведения всей системы, или как определение подсистемы.

Рис.17, начальное состояние.

• Конечное (финальное) состояние представляет собой частный случай состояния, которое также не содержит никаких внутренних действий (псевдосостояние). В этом состоянии объект будет находиться по умолчанию после завершения работы процесса в конечный момент времени.

Завершение работы переводится в конструкцию Skip, которая в теории CSP приводит к завершению работы процесса.

Рис.18. Завершение работы.

• Переход в новое состояние. Состояния представляются в CSP как процессы, и все стрелки (events) как события.

а-

Рис.19. Переход в новое состояние.

• Последовательность представляется с помощью последовательной композиции.

оператора

Рис.20. Последовательная композиция.

• Выбор представляется с помощью операций альтернативной композиции (□), или внутреннего недетерминированного выбора (п).

Рис.21. Выбор состояния.

• Параллельное выполнение переводится в СБР с помощью оператора параллельной композиции. ( ]|: параллельная композиция с синхронизацией, а |||: параллельной композиции без синхронизации).

fzzr р \ 1шф р\т *

#-1 « J

Рис.22. Параллельное выполнение.

Пример:

Рис.23. Пример: диаграмма состояния лифта. Перевод в CSP: main ША\\ В А = request ?/—► А Б й start -> Бj Б j = cJoseDoor —> В2 В2 = up В3 о down -* В3 В3 = passed —+В3 □ stop—* В4 В 4 = openDoor —* В

Спецификация системы в CSP-OZ будет представлена в следующем виде (см. Рис.24):

_DBcsf-oz-—

chan Iitsert_ classj() chan lnsert_class2()

chan De!ete_c!assi(J dian Dehte_chss:()

naain..=Init -*proc

proc = baert_ c!ass„—-proc в DeUie_classg—»proc □ Insert_ class,—*pro □ De!eie_ rfassa—*proc

Tab^chssi Tab_c!assm

Tab_c!assg

Vii: Tab_ciassi 3 rm: Tab_classm • n-foreig;u_ hey =rm.primary_key Vгь : Tcb_class;, 3 r£. Tab_c!assj • i\/oreigii_ key=ri.prima!y_key

Init _

Tab_c!assi = {} Л

Tab_class; = {} Л Tab_classQ = {}

Er.aile_lnsert_Tab_chsSi EnabIe_Delete_Tab_classj

Effect_lmeriJTab_clasS2 Effect_De!ete_Tab_class2

Ejfect_Insert_Tabj:lasss EffectJ>eleie_Tab_cldssx

Рис.24. Схема класса базы данных в СБР-Ог.

В четвертой главе приводится описание демонстрационной модели системы управления и резервирования авиабилетов с целью обоснования работоспособности предлагаемых в диссертации средств и методов. На этом примере показано, как из диаграмм иМЬ (диаграммы классов, диаграммы состояний и диаграммы сотрудничества) поэтапно выполняется перевод в спецификацию системы в СБР-Ог (см. рис.25.).

P- DBCSPOZ_

Chan Addjlight (NewFlJd?: NFLIGHT, NewFI_Date?:Date) Chan Add_Client (NewCIJd?: CLIENT JD, NewCl_Name?:NAME,

NewCl_age?: AGE, NewCljConr.CONTACT) Chan Addjlightj>rg (NewFpJd?: NFLIGHT, NewFp_From: AIRPORT,

NewFpJo: AIRPORT.: NewFp_Airplane : TYPE; NewFpJapacity: N) Chan Addjeservation {NewCIJd?: CLIENT_ID, NewFlJd?: NFLIGHT,

Nev/JDate?: Date) Chan Delete Jlight (DelFlJd?: NFLIGHT DelFlJtae?:Date) Chan Delete Client (DelClJd,?: CLIENT JD) Chan Delete_Flightj>rg (DelJlightjprg?: NFLIGHT) Chan CancelJeservation (DelClJd?: CLIENT JD, DelFlJd?: NFLIGHT,

DelJDate?: Dale)

Chan Checking Jlight (FIJd?: NFLIGHT, FIJDate?: Date, Result!: Boolean) Chan Checking Jeservation (ClJd?: CLIENT JD, FIJd?: NFLIGHT,

Rev_Date?: Date, Result!: Boolean) Chan CheckingClient {CIJd?: CLIENT JD, Result!: Boolean) Chan Checking Flightj>rg (Fpjd?: NFLIGHT, FpJrom?: AIRPORT,

Fp to?: AIRPORT, Res!: Boolean) Chan Reservation^/Client (ClJd?: CLIENT JD, Res_Cls!: Seq RESERVATION) Chan Clients_o/Jlight (SelectFlight ?: NFLIGHT, Cls_Flight!: Seq CLIENT JD)

main = In it —*PROC PROC = CLa FLa RE

CL =Checlcing_Client!Resullat—»(-^ResultatA Addjlient □

Resultat^{Delete_cIientaReservation_o/J21ient)) -» PROC FL =CheckingJlight!Resultat—*( -^Resultat A Add_Flight a

ResultatA(DeleteJlightaREaClientsj>fJlight)) -* PROC RE =CheckingJeservation!Resultat-^>( ResultatA Addjeservation Q Resultat^Delele Jeservation) -»PROC

Tab_FIightj>rg Tab_Flight TabjClient Tab Reservation

V/: Tab Jlight 3 p: Tab Jlight_prg •/. N Jlight = p. N Jlight_prg

V R: Tab Jeservation 3 с: TabjClient • R. Client Jd- c. Client Jd

V R: TabJReservation 3 f: TabJlight •

R. N_Flight = f. N Jlight A R.DateJFlight = / DateJFlight

Checking Flight_prg CheckingjOlient

Checking Jlight Checking_Reservation

Addjlight DeleteJlight

Addjlient DeletejClient

Addjlight_prg Delete Jlight_prg

Addjeservation Cancel Jeservation

Reservations of Client Clients j>j' Flight

Рис.25. Представление основной части демонстрационного примера с помощью класса СЗР-СЙ.

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

Заключение

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

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

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

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

Публикации по теме диссертации

Работа опубликованная в журнале, входящем в Перечень ВАК :

1. Бендума Т. Специализированные объектно-ориентированные модели программных систем / Т. Бендума // Системы управления и информационные технологии. - 2008. - № 4.1(34). - С. 155-159.

Другие публикации :

2. Еникеев А.И, Бендума .Т, Камашев М. А. Специализированные объектно-ориентированные модели программных систем // Проблемы теоретической кибернетики: Материалы XV Международной конференции. (Казань, 2008, 2-7 июня). - Казань: Изд-во «Отечество», 2008.-С. 36-37.

3. BENDOUMA T. La combinaison de UML avec la méthode formelle CSP-OZ pour le développement d'applications bases des données // Section Jeunes Chercheurs, 27 ème congrès INFORSID2009 (du 26 au 29 mai 2009 à Toulouse). -Toulouse, 2009. - P. 481-482.

4. Бендума T. Специализированные объектно-ориентированные модели программных систем / Т. Бендума // Информационные технологии моделирования и управления. - 2009. -№ 1(53). - С. 52-59.

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

6. Бендума Т. Комбинация средств UML и CSP-OZ для разработки приложений баз данных / Т. Бендума И Молодой ученый. - 2009. - №7 -

С.37-48.

Отпечатано с готового оригинала-макета в типографии издательства Казанского государственного университета Тираж 100 экз. Заказ 52/12

420008, ул. Профессора Нужина, 1/37 тел.: 233-73-59, 292-65-60

ВВЕДЕНИЕ

Цель работы

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

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

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

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

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

Выводы

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.

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

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

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