Содержание к диссертации
Введение
Методы формализации информационных моделей и их уточнений 16
1.1 Каноническая информационная модель 16
1.2 Денотационная и аксиоматическая семантики как способ формального определения информационных моделей . 22
1.3 Методы формализации уточнения 27
1.4 Методы формализации языков спецификаций в AMN . 32
1.5 Выводы по главе 37
Формальное определение ядра канонической информационной модели 39
2.1 Абстрактный синтаксис ядра канонической модели 41
2.2 Экстенсиональная интерпретация абстрактных типов данных 43
2.3 Семантические домены и семантические функции построения пространства состояний 45
2.4 Семантические функции формирования ограничений па пространство состояний 52
2.4.1 Ограничение типизации экземпляров классов 52
2.4.2 Ограничения, налагаемые отношением тип-подтип . 54
2.4.3 Ограничения, налагаемые отношением класс-подкласс 55
2.4.4 Ограничения, налагаемые инвариантами 56
2.5 Семантические функции формирования предикатов, отвечающих функциям 57
2.6 Семантические функции преобразования правил канонической модели в формулы над пространством состояний 60
2.6.1 Семантика конъюнкции коллекций с условием , . 62
2.6.2 Семантика объединения коллекций 68
2.7 Семантические функции преобразования формул
канонической модели в формулы над пространством состояний 68
2.7.1 Атомарные предикаты 68
2.7,2 Условия 70
27.3 Составные формулы 74
2.7.4 Алгоритм SideEffectSemantics 74
2.8 Выводы по главе 76
Моделирование конструкций ядра канонической модели средствами языка AMN 78
3.1 Основные принципы моделирования 78
ЗЛЛ Экстенсиональная интерпретация АТД 78
ЗЛ.2 Двойственное представление методов АТД 80
3 1.3 Моделирование структуры спецификации типов канонической модели при помощи средств композиции абстрактных машин AMN 80
3-2 Контекстная машина 83
3.3 Структура абстрактной машины, соответствующей типу: моделирование атрибутов, методов, инвариантов - - - 85
3.4 Моделирование формул канонической модели предикатами AMN 90
3.4Л Атомарные предикаты 90
3.4.2 Условия 91
3.4.3 Составные формулы 93
3.5 Моделирование формул канонической модели обобщенными подстановками AMN 94
3.6 Моделирование правил канонической модели обобщенными подстановками AMN 99
3.7 Адаптация моделирования конструкций канонической модели в AMN для доказательства непротиворечивости спецификаций 104
3.8 Выводы по главе 107
Корректность отображения канонической модели в язык AMN 108
4Л Принципы доказательства корректности отображения канонической модели в AMN 108
4.2 Множество состояний информационной системы, задаваемой множеством абстрактных машин 111
4.3 Инъективное отображение пространства состояний ИС, задаваемой спецификацией модуля канонической модели, в пространство состояний ИС, задаваемой набором абстрактных машин 114
4.4 Корректность отображения ограничений на пространство состояний 117
4.5 Корректность отображения спецификаций методов 119
4.5.1 Корректность отображения формул 120
4.5.2 Корректность отображения правил 123
4.6 Выводы по главе 124
5 Автоматизация доказательства корректности решения задач над множественными неоднородными информационными источниками 125
5.1 Программа автоматического отображения спецификаций канонической модели в язык AMN 125
5.2 Автоматизация доказательства корректности задачи синтеза канонических моделей для посредников 129
5.3 Автоматизация доказательства корректности композиции ИС
из компонентов 137
5.4 Выводы по главе 145
Заключение 147
Литература
- Денотационная и аксиоматическая семантики как способ формального определения информационных моделей
- Семантические домены и семантические функции построения пространства состояний
- Моделирование структуры спецификации типов канонической модели при помощи средств композиции абстрактных машин AMN
- Инъективное отображение пространства состояний ИС, задаваемой спецификацией модуля канонической модели, в пространство состояний ИС, задаваемой набором абстрактных машин
Введение к работе
В настоящее время наблюдается устойчивая тенденция к нее большему вовлечению формальных методов в процесс разработки информационных систем1 (ИС), Это связано с увеличением количества задач, для решения которых необходимы доказательные рассуждения о свойствах систем. Именно для решения такого рода задач и предназначены опирающиеся на математическую логику и алгебру формальные методы, представляющие собой совокупность языков, технологий и инструментальных средств спецификации и верификации сложных ИС.
Спецификация ИС есть описание системы и ее желаемых свойств на некотором языке спецификаций. Для формальной спецификации исиоль-зуются языки с математически определенными синтаксисом и семантикой. Такие языки как AMN [1], Z/Object Z [2, 3], VDM [4] используют аппарат математической логики и теории множеств для описания последовательных систем. Другой класс языков, таких как АСР, CSP |5], CCS [6], предназначен для описания параллельных взаимодействующих (concurrent) систем. Существуют также подходы, направленные на комбинирование возможностей этих двух классов языков, такие как TCOZ [7j, csp2b [8]. Алгебраический подход к спецификации систем используется в языке ASM [9], комбинация алгебраического и логического подходов используется в языке RSL [11].
Верификация разрабатываемой системы есть ее формальная проверка на соответствие заданным требованиям. Существует два основных метода верификации сложных систем: верификация моделей (model checking) и доказательство теорем (theorem proving).
Верификация моделей основана на построении конечной модели системы и проверке выполнения заданных свойств в этой модели. В силу конечности модели, такая верификация всегда может быть выполнена ав-
Согласно определению OS! ISO, информационная система есть совокупность, состоящая из персонала, одного либо нескольких компьютером, соотіюггстіїующих qxyi.em программирования, физических процессов, средств телекоммуникаций и других объектов, образующих автономное целое, способное осуществлять обработку данных или пеїхдачу данных. Структура информационной системы состоит из четырех основных частей: операционной системы, обеспечивающей управление функционированием всей информационной системы; платформы, преобразующей интерфейсы операционной системы в нужную форму и предоставляющей необходимые виды информационных услуг; прикладных программ, выполняющих задачи, ради которых создана информационная система; области взаимодействия, предоставляются услуги связи прикладных программ, расположенных как в одной, так и в группе информационных систем. В подавляющем числе случаев при разработке ИС все части, кроме прикладных проірамм, полагают фиксированными. Поэтому и области разработки программного обеспечения под информационной системой понимается только одна ее часть, а именно - прикладные программы. Таким образом информационная система понимается и в данной работе.
тематически. Основная проблема верификаций моделей состоит в том, что для проверки свойств сложных систем далеко не всегда возможно построить конечную модель приемлемого размера,^ и даже просто конечную модель.
Доказательство теорелг представляет собой метод, в котором система описывается на языке некоторой формальної! логики, а требуемые свойства системы описываются как формулы логики. Доказательство теорем представляет собой процесс вывода заданных формул из аксиом логики с использованием правил вывода. Некоторые выводы могут быть получены автоматически, для получения более сложных выводов используются средства интерактивного доказательства,
В контексте методов верификации систем формализуется одно из наиболее важных понятий в области формальных методов - понятие уточнения [1, 12, 13, 14]. В настоящей работе уточнение понимается следующим образом: система В уточняет систему Л, если пользователь может использовать систему В вместо системы Л, не замечая факта замены А на В. Уточнение формализовано в различных языках спецификаций, и изначально предназначалось для разработки ИС 71сверху-вниз" методом пошагового уточнения (stepwise refinement). При этом система описывается на высоком уровне абстракции, затем уточняется серией конкретизации вплоть до кода на языке программирования. Каждая последующая конкретизация системы является более детальной, чем предыдущая. При этом каждый шаг уточнения формально доказывается, и полученная в результате система обладает всеми необходимыми свойствами.
Формальная спецификация и верификация с успехом применялись в большом количестве проектов по разработке ИС в различных областях; медицине, ядерной энергетике, телефонии, транспорте, космической технике, разработке микропроцессорной техники, верификации протоколов и пр.
Тем не менее, в области разработки ИС существует много задач, интенсивно использующих понятие уточнения. Для их решения уточнение должно быть формально доказано. Задачи требуют формализации и разработки средств для формальной верификации, В множестве таких задач можно выделить три больших класса:
задачи, связанные с удовлетворением специфических нефункциональных требований к ИС;
задачи интеграции множественных неоднородных источников данных п сервисов;
3. задачи композиции ИС из существующих программных и информационных компонентов в интероперабельных средах, таких как Web services, Grid и различные виды промежуточного слоя, расположенного между операционными системами и прикладными системами.
К первому классу относятся, например, задачи разработки систем, ошибки которых критичны для безопасности функционирования человека в таких системах (safety-critical)[15], или задачи разработки отказоустойчивых (fault-tolerant) систем, способных продолжать работу при наличии сбоев [1G].
Задачи интеграции неоднородных источников (сервисов) и задачи композиции ИС из компонентов становятся все более актуальными в настоящее время, когда развиваются и появляются новые технологии промежуточного слоя (CORBA, Java RMI, .NET, Web Services, Semantic Web, Grid и другие), В рамках этих технологий иакоплено большое количество программных и информационных технически интероперабельных компонентов. Технологии промежуточного слоя обеспечивают техническую возможность интеграции источников и конструирования распределенных, интероперабельных ИС из компонентов; позволяют накапливать репознторни компонентов для их дальнейшего использования при создании новых ИС. Ввиду широкой распространенности этих технологий, необходимы методы достижения семантической иптероперабелыюсти компонентов. Понятие семантической интероперабельности означает комбинацию способностей решения следующих вопросов; релевантности имеющихся компонентов разрабатываемому применению, соответствии их прикладных контекстов контексту применения, а также также непротиворечивости иитеропе-рабелыюй композиции ресурсов в контексте разрабатываемого применения*
Решение задач интеграции неоднородных источников может быть основано на идее предметных посредников^ предназначенных для преобразования несистематизированного набора информационных источников, предо-ставляемых различными провайдерами, в хорошо структурированную коллекцию, поддерживаемую интегрированными однородными спецификациями [17].
Посредник обеспечивает пользователей метаинформацией, однородно представляющей предметный контент охватываемых источников, а также поддерживает унифицированную (каноническую) информационную модель. Такая модель необходима для однородного представления разнообразных моделей представления информации, используемых в неодтюрод-
ных источниках. Каноническая модель является расширяемой - ядро модели фиксировано, и для каждой модели М информационного источника строится такое расширение ядра Е, что Е уточняется моделью М. В случае баз данных под моделью информационного источника подразумевается совокупность языка определения данных и языка манипулирования данными, которые использовались для спецификации источника. Модели информационных источников называются исходными, в отличие от канонической модели, называемой также целевой.
Объединение таких расширении ядра составляет синтез каноническое модели посредника для моделей источников. На основании одного и того же ядра возможен синтез множества канонических моделей для различных наборов информационных источников.
Посредник поддерживает процесс систематической регистрации и классификации источников, содержит унифицированные онтологическую и мета-информацию для обнаружения и композиции существующих источников. Регистрация неоднородных источников в посреднике, согласование онтологии посредника и информационных источников, а также поиск подходящих информационных источников существенным образом опираются на уточнение структурных, поведенческих и онтологических спецификаций посредника структурными, поведенческими и онтологическими спецификациями источников.
Для преобразования запросов в терминах посредника в запросы к конкретным коллекциям, а также для обратного преобразования результата, полученного от коллекций, служат адаптеры информационных источников. Генерация доказательно правильных адаптеров также базируется на уточнении спецификаций посредника спецификациями источников.
Таким образом, задачи, относящиеся ко второму классу, требуют решения ряда семантических проблем, включая:
синтез канонических моделей для посредников над разнородными источниками информации;
согласование онтологии посредника и информационных источников на основе полных онтологических спецификаций;
поиск информационных источников и сервисов, семантически и алгоритмически релевантных заданным требованиям;
регистрация неоднородных источников информации в предметных посредниках;
генерация доказательно правильных адаптеров информационных источников.
Основная идея композиционного проектирования состоит в том, чтобы построить корректную композицию спецификаций существующих компонентов (информационных, программных), уточняющую спецификацию требований к разрабатываемой ИС [18]- При этом спецификации требований и существующих компонентов представляются в канонической модели. Реальные компоненты реализуются в разнообразных языках программирования, моделях данных. Техническая интероперабелыюсть неоднородных компонентов достигается применением архитектур и компонентных моделей, подобных CORBA [19]. Тем самым технически обеспечивается возможность композиции компонентов. В целях проектирования спецификации компонентов приводятся к однородному представлению в канонической модели. Предполагается также, что спецификация требований также представляется в канонической модели (хотя для этого может потребоваться преобразование в такую модель из некоторого другого языка спецификаций, например из UML). В настоящей работе рассматриваются следующие виды композиции: соединение и пересечение абстрактных типов данных2. Неформально, соединение Т\ U Ті спецификаций типов 7\ и Т% включает всю информацию, содержащуюся в спецификациях Т\ и Т% пересечение Ті П І2 включает лишь обитую информацию из спецификаций Т\ и 7.
Методы решения вышеперечисленных задач разрабатывались в течении ряда лет в Лаборатории композиционных методов проектирования информационных систем Института проблем информатики РАН. Для однородного представления разнообразных информационных источников, описания моделей предметных областей, проектирования и программирования ИС в иптероперабельпых средах было разработано ядро канонической модели представления информации - язык СИНТЕЗ [20]. Для достижения всех указанных целей в языке СИНТЕЗ совместно используются парадигмы моделей представления знаний о предметных областях и спецификаций требований к ИС [21], моделей концептуального проектирования ИС [223 23), объектно-ориентированных моделей данных [24, 25], логического программирования в дедуктивных базах данных [26, 27, 28], систем управления неоднородными мультибазами данных [29, 30], предикативных спецификаций И С [23, 31].
2Попятие абстрактного типа данных подробно обсуждается в разделе 2.2. операции соединения н пересечения определяются в разделе 2.6Л.
Были также разработаны методы расширения канонической модели [30, 32, 33], методы и средства композиционного проектирования ИС ]18, 34, 35], методы и средства интеграции множественных неоднородных источников [17, 36]. Необходимо заметить, что использование языка СИНТЕЗ в качестве ядра канонической модели не предполагает отказа от распространенных методов и моделей, таких как ОМТ [37], UML [38]: с их помощью могут осуществляться анализ ИС и обратная инженерия. Для решения более сложных задач - интеграции информационных источников и композиционного проектирования ИС - требуется более точная информационная модель. Поэтому такие модели, как ОМТ и UML должны быть отображены в каноническую информационную модель.
Необходимым требованием к разработанным методам и средствам являлось обеспечение возможности автоматизированного доказательства факта уточнения спецификации требований композицией спецификаций существующих компонентов.
Цель и задачи работы
Целью диссертационной работы является исследование и разработка формальных оснований автоматизации доказательства уточнения полных спецификаций требований спецификациями компонентов и их композиций в процессе интеграции множественных неоднородных источников данных и сервисов и композиционного проектирования ИС.
Достижение цели предполагает решение следующих задач:
1, для проведения доказательных рассуждений о моделях информаци
онных ресурсов, например, рассуждений об их непротиворечивости,
об уточнении или отображении моделей, разработка метода формаль
ного определения канонических информационных моделей, определе
ние на его основе формальной семантики ядра канонической модели
(языка СИНТЕЗ);
2. для автоматизации формального доказательства уточнения полных
спецификаций требований спецификациями компонентов, а также до
казательства непротиворечивости спецификаций, разработка метода
моделирования канонических информационных моделей в теоретико-
модельном формальном языке спецификаций, разработка, на его ос
нове алгоритмов отображения ядра канонической модели в формаль
ный язык. В качестве такого языка в настоящей работе выбрана
Нотация Абстрактных Машин (Abstract Machine Notation, AMN)[1],
что позволит использовать существующую технологию доказательства уточнения (B-technology [39]) и инструментальные средства доказательства уточнения (В-Toolkit [40], Antelier В[41] ) для доказательства уточнения спецификаций канонической модели;
разработка метода доказательства корректности отображения информационных моделей с использованием их денотационно-аксиоматической семантики; применение метода для доказательства корректности разработанных алгоритмов отображения ядра канонической модели bAMN;
создание на основе этих алгоритмов инструментального средства автоматического отображения спецификаций канонической модели в AMN и разработка методики использования этого средства совместно с B-Toolkit при решении практических задач проектирования ИС.
Методы исследования
При решении поставленных в работе задач использовались методы денотационной и аксиоматической семантики, методы теории множеств и логики предикатов, методы теории уточнения спецификаций.
Научная новизна
В диссертационной работе получены следующие новые научные результаты:
разработан метод формального определения канонических информационных моделей и па его основе - формальная денотационно-аксиоматическая семантика языка СИНТЕЗ;
разработан метод моделирования канонических информационных моделей в языке AMN и на его основе - алгоритмы отображения языка СИНТЕЗ в AMN;
разработан метод доказательства корректности отображения информационных моделей с использованием их денотационно-аксиоматической семантики; с использованием метода было построено доказательство корректности алгоритмов отображения языка СИНТЕЗ в AMN;
разработана методика использования формального аппарата доказательства уточнения при интеграции множественных неоднородных источников и при композиционном проектировании ИС.
Практическая ценность
Разработанные методы и средства созданы как составная часть инструментария эксперта-конструктор а, осуществляющего композиционное проектирование ИС как в рамках локальных, так и в рамках распределенных библиотек компонентов. При этом процесс проектирования ИС становится формально верифицируемым, что позволяет корректно использовать существующие компоненты, уменьшает время отладки и тестирования систем, позволяет проектировать системы, надежность которых критична, и отка-зоустоичивые системы.
Разработанные методы и средства предназначеиытакже для встраивания'в качестве составной части средств интеграции неоднородных информационных источников и сервисов для решения таких задач, как: синтез канонических моделей для посредников над разнородными информационными источниками; согласование онтологии посредника и информационных источников; поиск информационных источников и сервисов, семантически релевантных заданным требованиям; регистрацию неоднородных информационных источников в предметных посредниках; генерацию доказательно правильных адаптеров информационных источников.
Реализация результатов работы
Результаты диссертационной работы использованы в проектах РФФИ 01-07090084, 03-01-00821, 05-07-90413-в; проекте № 1-Ю программы фундаментальных исследований ОИТВС РАН "Фундаментальные основы информационных технологий и систем", НИР Контекст "Контекстуализация неоднородных информационных источников в предметном информационном посреднике", НИР И НИ "Композиционные методы решения задач в инфраструктурах интеграции информации для научных исследований".
Разработанные инструментальные средства нашли применение в качестве составной части инструментария эксперта-конструктор а, реализующего композиционное проектирование ИС, и прототипа средств поддержки предметных посредников.
Апробация работы
Основные результаты диссертации докладывались на Международных конференциях ADBIS (Братислава 2002, Будапешт 2004), на XXIV Конференции молодых ученых механико-математического факультета МГУ им. М.В. Ломоносова (Москва, 2002), на Международном симпозиуме по базам данных конференции VLDB (Берлин 2003), на II научной сессии ИПИ
РАН (Москва, 2005), на научных семинарах лаборатории Композиционных методов проектирования информационных систем Института проблем информатики РАН.
На защиту выносятся следующие, полученные автором результаты:
метод формального определения канонических информационных моделей; формальная денотационно-аксиоматическая семантика языка СИНТЕЗ;
метод моделирования канонических информационных моделей в теоретико-модельном языке AMN; алгоритмы отображения языка СИНТЕЗ в AMN;
метод доказательства корректности отображения информационных моделей с использованием их денотационно-аксиоматической семантики; доказательство корректности алгоритмов отображения языка СИНТЕЗ в AMN;
разработанное на основе указанных алгоритмов инструментальное средство автоматического отображения спецификаций ядра канонической модели в AMN;
методика использования формального аппарата доказательства уточнения при интеграции множественных неоднородных источников данных и сервисов и при композиционном проектировании ИС.
Публикации по теме диссертации
По теме диссертации автором опубликовано 9 работ.
Структура работы
Текст диссертации включает введение, пять глав, заключение, список литературы и четыре приложения.
В первой главе изложены основные черты ядра канонической информационной модели (языка СИНТЕЗ) и мотивация формального определения канонической модели. Рассматривается обзор основных существующих методов формального определения информационных моделей, близких к ядру канонической модели.
Во второй главе рассматривается метод формального определения канонических информационных моделей. Метод демонстрируется на примере построения формальной семантики ядра канонической модели (языка СИНТЕЗ).
В третьей главе рассматривается метод моделирования канонических информационных моделей в языке AMN. Применение метода демонстрируется па примере определения отображения абстрактного синтаксиса ядра канонической модели в спецификации AMN.
В четвертой главе рассматривается метод доказательства корректности отображения информационных моделей с использованием их денотационно-аксиоматической семантики. Метод демонстрируется на примере доказательства корректности алгоритмов отображения G ядра канонической модели в AMN.
В пятой главе рассматриваются методика и примеры использования представленных в диссертационной работе методов моделирования спецификаций для автоматизации доказательства корректности решения задач над неоднородными источниками информации.
В заключении приводятся основные результаты, полученные в рамках данной работы.
В приложении А содержится конкретный синтаксис ядра канонической модели.
В приложении В приводится краткое описание языка AMN.
В приложении С рассматривается представление основных элементов UML и OCL в канонической модели.
В приложении D приводится полный текст спецификаций АМЫ, полученный в результате работы инструментального средства отображения спецификаций канонической модели в AMN на примерах, рассматриваемых в пятой главе.
Денотационная и аксиоматическая семантики как способ формального определения информационных моделей
Одними из самых широкоиспользуемых методов формального определения языков спецификаций (в том числе объектных моделей и языков запросов, обладающих сходными с канонической моделью чертами), являются методы денотационной и аксиоматической семантик [43, 44, 45, 46, 47].
Ниже приведен обзор основных существующих подходов формального определения информационных моделей, близких к ядру канонической модели, с использованием методов денотационной и аксиоматической семантик. Цель обзора состоит в выявлении общих закономерностей и особенностей формального определения информационных моделей, которые могут быть использованы при формальном определении ядра канонической модели.
С конца девяностых годов прошлого века ведутся активные исследования по формальному определению языка визуализации, спецификации, проектирования и документирования ИС, разработанного концерном OMG, - языка Unified Modeling Language (UML) [38], а также языка Object Constraint Language (OCL) [48], предназначенного для спецификации дополнительных требований, которые невозможно или сложно выразить графическими средствами языка UML. Во всех этих работах в той или иной степени применяются методы денотационной и аксиоматической семантик: индуктивно рассматривается представление конструкций языков UML/OCL в некотором формальном языке, основанном на математической логике, свойства конструкций представляются аксиомами языка. Часто для простоты опускается абстрактный синтаксис и семантические функции выражаются неявно или на примерах.
В работах France [49, 50] в качестве семантики языка UML рассматривается формальный язык Z [2]. Основное внимание уделено интерпретации в языке Z диаграмм классов UML. Понятие уникальной идентифицируемости объекта (object identity) в предложенном подходе формализуется при помощи предопределенных множеств объектных идентификаторов, заданных для каждого UML-класса. Разделяются понятия интепси-онала класса как набора свойств, общих для всех объектов класса и экс-тенсионала класса как множества объектов класса. Для экстенсионала и интенснонала вводятся различные схемы языка Z. Интенсиональная схема описьшает класс в терминах его атрибутов, типы атрибутов интерпретируются как предопределенные множества. Экстенсиональная схема со держит переменную, интерпретирующую множество экземпляров класса, а также функцию, ставящую в соответствие объектам их атрибуты. Отношение обобщения-специализации интерпретируется введением собственных интенсиональной и экстенсиональной схем для подкласса. Интенсиональной схема подкласса расширяющей интенсиональную схему суперкласса, а экстенсиональная схема подкласса содержит определение экстенслоиала подкласса и необходимые ограничения, задающие иерархию. При помощи отдельной схемы отражаются свойства пепересечепия экстеисиопалов классов. Ассоциации между классами определяются при помощи отдельных схем, включающих экстенсиональные схемы ассоциированных классов, кардинальность ассоциаций выражается специальными предикатами. Состояние системы в целом выражается схемой, включающей схему иерархии и схемы ассоциаций.
Работы Kim, Carrington [51, 52] посвящены определению семантики диаграмм классов UML в языке Object-Z [3] - объектно-ориентированном расширении Z. Язык Object-Z содержит понятия уникальной идентифицируемости объектов и наследования, что позволяет избавиться от экстенсиональных схем при интерпретации классов UML. В подходе каждый UML-класе интерпретируется схемой Object.-Z. Атрибуты типизируются предопределенными множествами, ассоциации интерпретируются атрибутами классов. Факт участия объекта класса в ассоциации в некоторой роли выражается при помощи предиката с квантором всеобщности. Отношение обобщения-специализации интерпретируется при помощи наследования схем Object-Z, а также специальными предикатами, указывающими на полиморфизм объектов суперклассов. Схема, выражающая состояние системы в целом, для каждого Object-Z-класса содержит множество, типизированное как множество экземпляров данного класса. Для класса, являющегося суперклассом, указывается полиморфизм объектов соответствующего множества. Схема системы включает также предикаты, утверждающие существование объектов, доступных по ассоциативной ссылке, и предикаты вхождения подкласса в суперкласс как подмножества.
Логическим продолжением данных работ является результат Roe, Broda, Russo [53] по представлению семантики подмножества OCL в Objcct-Z. Операции UML интерпретируются как отдельные операционные схемы, параметры операций интерпретируются как входные и выходные коммуникационные переменные схем. Инварианты OCL представляются либо как предикаты в схемах классов, либо как предикаты в схеме системы. Пред и постусловия операций UML представляются предикатами соответствз ющих операционных схем. В работе рассмотрено также инструментальное средство автоматического отображения диаграмм классов UML с наложенными OCL-ограничениями в Object-Z.
Работы Lano, Bicarregui (54, 55, 56] посвящены формальному определению языка UML в языке RAL (Realime Action Logic) [57). Спецификации RAL представляют собой структурированные теории, основанные на логике первого порядка и включающие средства описания временных свойств систем. Описана семантика конструкций UML, составляющих диаграммы классов, состояний, диаграммы последовательностей действий, активностей: классов, ассоциаций, атрибутов, операций, отношения обобщения, сообщений. Каждый UML-класс С представляется отдельной теорией Гс, содержащей одноименный предопределенный тип - множество всевозможных объектов класса. Множество существующих объектов класса представляется переменной С теории Го, типизированной как конечное подмножество элементов типа С. Множество переменных теории включает также переменную self, отражающую уникальную идентифицируемость объектов и переменные, соответствующие атрибутам UML-класса. Атрибутные переменные типизированы как функции из множества С в множество, представляющее тип атрибута. Ассоциации представляются переменным!], типизированными как элементы декартова произведения типов, представляющих ассоциированные классы. Факт существования объектов, входящих в ассоциации, интерпретируется соответствующими аксиомами. Специальными аксиомами представляются свойства ассоциаций, такие как кардинальность. Обобщение UML-классом Т UML-класса S интерпретируется аксиомами S ; Т A S С Т: тип S теории Гз является подтипом типа Т теории Ts, множество S является подмножеством Т. Операции UML представляются действиями (actions) соответствующих теорий RAL. В работе [55] определено также представление в RAL подмножества языка OCL. Показано, как полученная семантика может использоваться для верификации преобразования UML-диаграмм (усиления инвариантов, рационализации ассоциаций, элиминации ассоциации много-ко-мнопш, транзитивности агрегации, преобразования интерфейса).
Семантические домены и семантические функции построения пространства состояний
Описание семантических доменов начинается с элементарных доменов; В = {true, false} — логические значения; Z= { 1,0,1... } — множество целых чисел; STRING — множество последовательностей символов - строк; IDENTIFIER — множество идентификаторов, описываемое как совокупность последовательностей букв, цифр и знаков подчеркивания, в которых первым символом является буква; UJ С N — множество уникальных идентификаторов объектов.
Количество объектов в любой ИС всегда конечно, следовательно, в качестве множества уникальных идентификаторов можно взять любое бесконечное перечислимае множество» чем и вызвано требование включения U С N, где N - множество натуральных чисел. Следующая группа семантических доменов - производные домены, сконструированные из элементарных доменов операциями конструирования доменов: (IDENTIFIER.)- множество подмножеств идентификаторов IP(ILJ)- множество подмножеств уникальных идентификаторов объектов V = В + Z + STRING + IDENTIFIER + V{IDENTIFIER) + U + P(U) + AVAC + (AVAC) V = {B,Z, STRING, IDENTIFIER (IDENTIFIER) t V,f{V),AVAC (AVAC)} T = [U -» Л V-4] С = [7C - Р(ДУЛ)] SxC
Здесь V - семантический домен значений, которые может принимать какой-либо атрибут; V - домен, элементами которого являются семантические домены, значения из которых может принимать какой-либо атрибут; Т - параметризованное выражение, задающее семантический домен - множество функций, описывающих состояние объектов (функция из этого домена сопоставляет каждому объектному идентификатору из своей области определения некоторое абстрактное значение из AVAC)] С - параметризованное выражение, задающее семантический домен - множество функций, описывающих состав коллекций (функция из этого домена ставит в соответствие именам коллекций множества абстрактных значений); S - параметризованное выражение, задающее семантический домен - пространство состояний системы. Смысл параметра выражения IQ С IDENTIFIER состоит в том, что он является множеством имен коллекций модуля.
Пространство состояний конкретного модуля, задаваемого спецификацией из синтаксического домена Module, строится семантической функцией sMcdidc и является конкретизацией выражения S. Семантический домен абстрактных значений AVAC, участвующий в определении пространства состояний, строится семантической функцией sAVAC на основании спецификации секции типов модуля, принадлежащей синтаксическому домену TypeSection.
Семантические соотношения, задающие функцию построения пространства состояний sModule выглядят следующим образом; sModule\II MS] = sModuleSpeclMS] sModuleSpec{TS FS IRS] ± sTypeSection[TS] x sIRSection{IRSl
Сигнатура функции состоит из имени - sModule и области определения - синтаксического домена Module. Имена всех семантических функций имеют префикс 5, от слова semantic - семантический. Знак = используется в работе при определении семантических функций. Пространство состояний конкретного модуля определяется как декартово произведение результатов семантических функций sTypeSection и sIRSection, действующих па синтаксических доменах TypcSection и IRSection, соответствен тю. Семантические соотношения, определяющие действие функций STypeSection и sIRSection, описаны ниже: sTypeSection[TSL] [U -++ sAVA[TSL]] sAVAC\TSL\ ± g sTypeSpecOwnExt{i\TSL\}, і где гТЯ] — г-я спецификация типа из списка sTypeOwnExtlTD] sTypeDeclOwnExt[TD] sTypeDeclOwnExt\ADT] = sAbstmctDataTypeOwnExt{ADT\ sAbstmct.DataTypeOwnExt[TI STL ASLj = sAttributeListExt{sFullAttributeList[STLASL]) sTypeSection формирует домен частичных функций из U в AVAC. AVAC формируется функцией sAVAC как объединение непересекающихся собственных экстенсионален абстрактных типов. Собственный экстенеи-онал абстрактного типа формируется функцией sAbsiractDataTypcOwnExt на основании полного набора атрибутов типа, включающего атрибуты, унаследованные от супертипов. Формирование такого набора осуществляет функция sFullAttributeSet Преобразование результата работы функции sFullAttributeset в экстенсионал осуществляется функцией sAtimbuteListExt: sFullAttributeSet\STh ASL] = (U sTypeAttributes{sTypeIdlilSTLjj)lTSL]) hsAttrSpecListlASL}, зТуреЩЮ] ± sldentifierlWl где і[577/] - г-е имя супертипа из списка, операция перекрытия отношения т\ отношением Г2, т\ Э-г2 задается как Т\ 3-Г2 = dom (Т2 Г\) U Г операция антиограничения отношения г множеством s задается как $ г = {х, у\х - уЄгАх dom г — s} Функция sTypeAitribuies формирует множество атрибутов типа по идентификатору типа и списку спецификаций типов: sTypeAttributes{T : IDENTIFIER)[TSL] 4 Q sTypeSpecAitr{T){i\TSLll s7\jpeSpecAtir{T ; WENT1F1ER)\T1 STLASL] 4 if T = a% cJd[77] then sFullAttributeSetlSTL ASL] else 0, где г [ T JS LI - г-я спецификация типа из списка. Семантическая функция sTypeAitribuies имеет два вида параметров; параметры, принимающие значения из семантических доменов (Т из домена IDENTIFIER), список которых заключен в круглые скобки; и параметры, принимающие значения из синтаксических доменов (TSL из домена TypeSpecificationList) список которых заключен в квадратные скобки. Выражение ifhen Vielse 1 принимает значение V\ в случае, если Е истинно и значение Кг в противном случае.
Моделирование структуры спецификации типов канонической модели при помощи средств композиции абстрактных машин AMN
Методы АТД канонической модели могут иметь двойственное представление при отображении в AMN.
Во-первых, методы типа отображаются в операции абстрактной машины, соответствующей типу. Во-вторых, методы могут быть представлены как функции, типизированные в соответствии с: сигнатурами методов канонической модели. Для каждой из таких функций к инварианту абстрактной машины добавляется предикат, показывающий, каким образом связаны входные и выходные параметры функции. Предикат формируется на основе спецификации метода канонической модели.
Предполагается, что методы, имеющие представление функциями, не изменяют состояние объектов ИС.
Представление функцией метода т типа Т, представляемого в AMN абстрактной машиной Л/, используется для моделирования следующих случаев: ссылки на m в инварианте Т, либо в инвариантах какого-либо другого типа 7\; ссылки на тп в спецификации какого-либо другого метода mi типа Т, либо в спецификациях методов какого-либо другого тина Ті.
Спецификации типов канонической модели могут ссылаться друг на друга в спецификациях атрибутов, методов, инвариантов, образуя структуру спецификаций типов. Основным принципом отображения структуры спецификаций типов канонической модели в AMN является стремление отобразить каждый АТД отдельной абстрактной машиной. Проблема состоит в том, что средства композиции абстрактных машин являются гораздо менее гибкими, чем средства организации структуры спецификаций типов канонической модели. Данное противоречие разрешается при помощи процедуры преобразования ориентированного графа структуры модуля М, представляющего композиционную структуру спецификаций типов модуля, — DSG{M )b в ориентированный граф, представляющий композиционную структуру набора абстрактных машин, — DAMSG[M).
Определение 3.1. Ориентированный композиционный граф DSG(M) модуля М, есть пара (N, Е), где множеством вершин графа N является мнооїсєство Types(M) ЛТД, определенных в модуле М; множеством направленных ребер графа Е является мнооїсєство упорядоченных пар (Ті, 3J)J где Ті, Ту Types(M), и спецификации инвариантов и(или) методов Т\ содержат ссылки на атрибуты, методы, инварианты типа Ті, либо ссылки па коллекции с типоль экземпляров 7.
Определение 3.2. Множество Types(M) АТД, определенных в модуле Л/, есть мнооїсєство, состоящее из типов, описанных в секции type модуля и типов, соответствующих типовым выражениям, определенным в модуле; причем если 7\ U Ті Є Types{M), mo Т\ П 7 такоісе включается в Types(M). Типовое вырао/сепие есть идентификатор типа, либо выражение Т\ИТ (соединение типов), либо выражение 7\ П Т%, где Tj,T2 типовые выражения.
Определение 3.3. Ориентированный граф структуры абстрактных машин DAMSG(M) для модуля М, есть пара {N,E), где множеством вершин градэа N является множество подлтожеств Types(M) такое,что Vsi, S2 (si N Л s2 Є N = si П s2 = 0) Л Us= Types(M) s =N
Это означает, что множества спецификаций типов из N являются непересекающимися и объединение их образует множество всех спецификаций типов Types(M). Множеством направленных раскрашенных ребер графа Е является множество упорядоченных троек ($i S2,c)} где sus2eN, с {sees, uses, includes, extends}
Каждая из вершин s графа соответствует абстрактной машине, в которую отображаются весь набор типов из s. Ребро между вершинами графа означает отношение композиции абстрактных машин, цвет ребра означает вид композиции. DAMSG строится из DSG следующими последовательными преобразованиями: Раскраска. Ребра графа раскрашиваются по следующим правилам: — ребро {si, Sj) раскрашивается в цвет sees, если методы типов из 5/ ссылаются на атрибуты, методы типов из Sj, либо на коллекции : типами экземпляров из sy, — ребро (si,Sj) раскрашивается в цвет uses, если инварианты ти пов из Si ссылаются на атрибуты, методы типов из Sj, либо па КОЛЛекЦИИ С Типами ЭКЗемПЛЯрОВ ИЗ Sj\ — ребро (si, Sj) раскрашивается в цвет includes, если методы типов из si изменяют атрибуты типов из 5 ; — ребро ( , Sj) раскрашивается в цвет extends, если среди типов из Sj ЄСТЬ непосредственные СуперТИПЫ ТИПОВ НЗ S{.
Выявление косвенных ассоциаций между типами. Тип Ті имеет косвенную ассоциацию с типом Тг, если существуют такой атрибут а некоторого типа, метод / типа 1\, изменяющий значение атрибута а и метод g типа Тг3 ссылающийся на атрибут а и имеющий представление функциональной переменной. Отображение системы типов в AMN в этом случае требует отношения includes между машиной, инкапсулирующей тип Ті, и машиной, инкапсулирующей тип Т . Для отражения этого отношения в граф добавляется ребро {si,Sj} цвета includes, где Ті Є Si, Тч Є Sj. Таким образом косвенная ассоциация становится явной.
Элиминация циклов. В языке AMN не разрешаются циклы в гра фе композиционной иерархии абстрактных машин. Поэтому циклы в графе элиминируются при помощи следующей процедуры. Последовательно перебираются все циклы DCG, множество вершин цикла сливается в одну вершину. При слиянии двух ребер е\ и еі, результирующее ребро є красится в более яркий цвет из цветов ребер С\ и Є2- Шкала яркости цветов от менее яркого к более яркому выглядит так: sees, uses, includes, extends.
Элиминация дублирующих includes/extends путей. В языке AMN не разрешается одной машине быть дважды включенной в другую машину. Ввиду ИТОГО граф композиционной структуры абстрактных машин должен обладать следующим свойством: между любыми двумя вершинами не может быть более одного пути, ребра которого раскрашены в цвет includes либо в цвет extends. Процедура элиминации дублирующих includes -путей состоит в следующем.
Инъективное отображение пространства состояний ИС, задаваемой спецификацией модуля канонической модели, в пространство состояний ИС, задаваемой набором абстрактных машин
Целью данного раздела является определение ннъектнвного отображения 0 пространства состояний S системы, задаваемой спецификацией модуля М канонической модели, $ = sModu\e{M) в пространство состояний 8д системы, задаваемой множеством абстрактных машин Ми = 0(.М). Рассмотрим произвольное состояние S ь- С Є и построим состояние SB, которое будет являться образом S — С, SB = 9{S - С)
Рассмотрим произвольный уникальный объектный идентификатор и Є dom(5). Пусть Т - тот тип, что S(u) Є V . Без ограничения общности можно считать, что существует v Є exlp что self(v) — иу т.к. мы всегда сможем установить желаемую биекцию между множествами U и OID. Будем считать v образом S(u) при отображении в.
Если S[u) входит в состав некоторой коллекции С, то положим v є С (v принадлежит множеству, моделирующему коллекцию С при отображении 0). Если S(u) не входит в состав никакой коллекции, то положим v Є NCO.
Далее, рассмотрим множество W всех значений необъектных типов, на которые ссылается состояние 5ь С. Ссылки могут быть следующих видов: значение необъектного типа принадлежит некоторой необъектной коллекции; значение необъектного типа есть значение атрибута некоторого значения абстрактного типа, па которое ссылается состояние S — С.
Для каждого значения w типа Т из W выберем произвольное значение х є extp и будем считать х = в(гп). Если и входит в состав некоторой необъектной коллекции С, то положим w Є С (w принадлежит множеству, моделирующему коллекцию С при отображении 0).
Рассмотрим теперь последовательно все элементы ran (S) и W и определим значения атрибутных функций AMN на их образах при отображении в.
Пусть ш - значение типа Т из ran (5) U W. Для каждого атрибута а є AT положим следующее. Пусть а - атрибутная функция AMN, моделирующая атрибут а: если тип атрибута а не АТД-порожденный (раздел 2.3), положим a(e(w)) = yj(a) ввиду очевидной биекции между семантическими доменами примитивных типов и моделирующими их в AMN множествами; если тип атрибута а - АТД, положим а($(ю)) = 9{a(w)); если тип атрибута а - АТД-порожденный тип множества, положим a{6(w)) = {х 3 у (у є a(w) Ах = 9{у))}.
Таким образом, отображение в полностью определено. Утверждение 4.1. Построенное отобраоїсепие в инъективио. До казате л ьство. Пусть существуют два различных состояния S\ ь-» Сі 8 и 52 "- Съ Є S3 такие, что (?(5і Сі)-0{52 С2)-5л
Докажем, что S\ к- Сі = 52 — Сз и таким образом придем к противоречию. I. Рассмотрим произвольный уникальный объектный идентификатор и Є dom(5i). По построению в, и = self(6(u)), а значит, и Є dom( S2). Пусть Si(u) Є Vj, для некоторого Т, тогда selj l(u) Є extp, а значит t?2( ) Є К. Докажем теперь, что 5І(ЇІ) И 5г( ) совпадают на всех своих атрибутах, а следовательно} равны. Заметим, что 0(ЗД) = 0(S2(u)) = v поскольку идентификаторы из UID взаимооднозначно соответствуют значениям из Obj. Очевидно, что S\[u) и L 2( ) совпадают на атрибутах примитивных типов: по определению в o(0(Si(u))) = (Si(u))(a), a(e(S2(u))) = (Si(u))(a); а значит Пусть теперь тип атрибута а - объектный АТД. Тогда (5i(u))(a) = вс//(ад) = (52(u))(a)
Аналогично доказывается равенство всех соответствующих элементов множеств (5](ii))(a) и (S2{u))(a) если тип а- тип множества значений объектного АТД.
Далее, пусть тип а - необъектный АТД. Тогда необходимо показать, что значения (Si(u))(a) и ( S2(u))(a) совпадают на всех своих атрибутах, а следовательно, равны. Доказательство осуществляется аналогично доказательству равенства значений Si(u) и S2{u) по построению 9.