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

• Ступников, Сергей Александрович
• кандидат технических наук
• 2006

Оглавление диссертации кандидат технических наук Ступников, Сергей Александрович

Введение

1 Методы формализации информационных моделей и их уточнений

1.1 Каноническая информационная модель.

1.2 Денотационная и аксиоматическая семантики как способ формального определения информационных моделей

1.3 Методы формализации уточнения.

1.4 Методы формализации языков спецификаций в AMN

1.5 Выводы по главе.

2 Формальное определение ядра канонической информационной модели

2.1 Абстрактный синтаксис ядра канонической модели

2.2 Экстенсиональная интерпретация абстрактных типов данных

2.3 Семантические домены и семантические функции построения пространства состояний.

2.4 Семантические функции формирования ограничений на пространство состояний.

2.4.1 Ограничение типизации экземпляров классов.

2.4.2 Ограничения, налагаемые отношением тип-подтип

2.4.3 Ограничения, налагаемые отношением класс-подкласс

2.4.4 Ограничения, налагаемые инвариантами

2.5 Семантические функции формирования предикатов, отвечающих функциям

2.6 Семантические функции преобразования правил канонической модели в формулы над пространством состояний

2.6.1 Семантика конъюнкции коллекций с условием

2.6.2 Семантика объединения коллекций.

2.7 Семантические функции преобразования формул канонической модели в формулы над пространством состояний 68 2.7.1 Атомарные предикаты.

2.7.2 Условия.

2.7.3 Составные формулы.

2.7.4 Алгоритм SideEffectSemantics.

2.8 Выводы по главе.

3 Моделирование конструкций ядра канонической модели средствами языка AMN

3.1 Основные принципы моделирования.

3.1.1 Экстенсиональная интерпретация АТД

3.1.2 Двойственное представление методов АТД.

3.1.3 Моделирование структуры спецификации типов канонической модели при помощи средств композиции абстрактных машин AMN.

3.2 Контекстная машина.

3.3 Структура абстрактной машины, соответствующей типу: моделирование атрибутов, методов, инвариантов

3.4 Моделирование формул канонической модели предикатами AMN.

3.4.1 Атомарные предикаты.

3.4.2 Условия.

3.4.3 Составные формулы.

3.5 Моделирование формул канонической модели обобщенными подстановками AMN.

3.6 Моделирование правил канонической модели обобщенными подстановками AMN.

3.7 Адаптация моделирования конструкций канонической модели в AMN для доказательства непротиворечивости спецификаций.

3.8 Выводы по главе.

4 Корректность отображения канонической модели в язык AMN

4.1 Принципы доказательства корректности отображения канонической модели в AMN.

4.2 Множество состояний информационной системы, задаваемой множеством абстрактных машин.

4.3 Инъективпое отображение пространства состояний ИС, задаваемой спецификацией модуля канонической модели, в пространство состояний ИС, задаваемой набором абстрактных машин.

4.4 Корректность отображения ограничений на пространство состояний.

4.5 Корректность отображения спецификаций методов.

4.5.1 Корректность отображения формул.

4.5.2 Корректность отображения правил.

4.6 Выводы по главе.

5 Автоматизация доказательства корректности решения задач над множественными неоднородными информационными источниками

5.1 Программа автоматического отображения спецификаций канонической модели в язык AMN.

5.2 Автоматизация доказательства корректности задачи синтеза канонических моделей для посредников.

5.3 Автоматизация доказательства корректности композиции И С из компонентов.

5.4 Выводы ио главе.

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

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

Спецификация ИС есть описание системы и ее желаемых свойств на некотором языке спецификаций. Для формальной спецификации используются языки с математически определенными синтаксисом и семантикой. Такие языки как AMN [1], Z/Object Z [2, 3], VDM [4] используют аппарат математической логики и теории множеств для описания последовательных систем. Другой класс языков, таких как АСР, CSP [5], CCS [6], предназначен для описания параллельных взаимодействующих (concurrent) систем. Существуют также подходы, направленные на комбинирование возможностей этих двух классов языков, такие как TCOZ [7], csp2b [8]. Алгебраический подход к спецификации систем используется в языке ASM [9], комбинация алгебраического и логического подходов используется в языке RSL [11].

Верификация разрабатываемой системы есть ее формальная проверка на соответствие заданным требованиям. Существует два основных метода верификации сложных систем: верификация моделей (model checking) и доказательство теорем (theorem proving).

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

1 Согласно определению OSI ISO, информационная cucme.ua есть совокупность, состоящая из персонала, одного либо нескольких компьютером, соответствующих средств программирования, физических процессов, средств телекоммуникаций и других объектов, образующих автономное целое, способное осуществлять обработку данных или передачу данных. Структура информационной системы состоит из четырех основных частей: операционной системы, обеспечивающей управление функционированием всей информационной системы; платформы, преобразующей интерфейсы операционной системы в нужную форму и предоставляющей необходимые виды информационных услуг; прикладных программ, выполняющих задачи, ради которых создала информационная система; области взаимодействия, предоставляющей услуги связи прикладных программ, расположенных как в одной, так и в группе информационных систем. В подавляющем числе случаев при разработке ИС все части, кроме прикладных программ, полагают фиксированными. Поэтому и области разработки программного обеспечения под информационной системой понимается только одна ее часть, а именно - прикладные программы. Таким образом информационная система понимается и в данной работе. томатически. Основная проблема верификации моделей состоит в том, что для проверки свойств сложных систем далеко не всегда возможно построить конечную модель приемлемого размера, и даже просто конечную модель.

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

В контексте методов верификации систем формализуется одно из наиболее важных понятий в области формальных методов - понятие уточнения [1, 12, 13, 14]. В настоящей работе уточнение понимается следующим образом: система В уточняет систему А, если пользователь может использовать систему В вместо системы А, не замечая факта замены А на В. Уточнение формализовано в различных языках спецификаций, и изначально предназначалось для разработки ИС „сверху-вниз" методом пошагового уточнения (stepwise refinement). При этом система описывается на высоком уровне абстракции, затем уточняется серией конкретизации вплоть до кода на языке программирования. Каждая последующая конкретизация системы является более детальной, чем предыдущая. При этом каждый шаг уточнения формально доказывается, и полученная в результате система обладает всеми необходимыми свойствами.

Формальная спецификация и верификация с успехом применялись в большом количестве проектов по разработке ИС в различных областях: медицине, ядерной энергетике, телефонии, транспорте, космической технике, разработке микропроцессорной техники, верификации протоколов и пр.

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

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

2. задачи интеграции множественных неоднородных источников данных и сервисов;

3. задачи композиции ИС из существующих программных и информационных компонентов в интероперабельных средах, таких как Web services, Grid и различные виды промежуточного слоя, расположенного между операционными системами и прикладными системами.

К первому классу относятся, например, задачи разработки систем, ошибки которых критичны для безопасности функционирования человека в таких системах (safety-critical) [15], или задачи разработки отказоустойчивых (fault-tolerant) систем, способных продолжать работу при наличии сбоев [16].

Задачи интеграции неоднородных источников (сервисов) и задачи композиции ИС из компонентов становятся все более актуальными в настоящее время, когда развиваются и появляются новые технологии промежуточного слоя (CORBA, Java RMI, .NET, Web Services, Semantic Web, Grid и другие). В рамках этих технологий накоплено большое количество программных и информационных технически интероперабельных компонентов. Технологии промежуточного слоя обеспечивают техническую возможность интеграции источников и конструирования распределенных, интероперабельных ИС из компонентов; позволяют накапливать репознтории компонентов для их дальнейшего использования при создании новых ИС. Ввиду широкой распространенности этих технологий, необходимы методы достижения семантической интероперабелъности компонентов. Понятие семантической интероиерабельности означает комбинацию способностей решения следующих вопросов: релевантности имеющихся компонентов разрабатываемому применению, соответствии их прикладных контекстов контексту применения, а также также непротиворечивости иптероне-рабельной композиции ресурсов в контексте разрабатываемого применения.

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

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

Объединение таких расширений ядра составляет синтез канонической модели посредника для моделей источников. На основании одного и того же ядра возможен синтез множества канонических моделей для различных наборов информационных источников.

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

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

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

• синтез канонических моделей для посредников над разнородными источниками информации;

• согласование оитологий посредника и информационных источников на основе полных онтологических спецификаций;

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

• регистрация неоднородных источников информации в предметных посредниках;

• генерация доказательно правильных адаптеров информационных источников.

Основная идея композиционного проектирования состоит в том, чтобы построить корректную композицию спецификаций существующих компонентов (информационных, программных), уточняющую спецификацию требований к разрабатываемой ИС [18]. При этом спецификации требований и существующих компонентов представляются в канонической модели. Реальные компоненты реализуются в разнообразных языках программирования, моделях данных. Техническая интероперабельность неоднородных компонентов достигается применением архитектур и компонентных моделей, подобных CORBA [19]. Тем самым технически обеспечивается возможность композиции компонентов. В целях проектирования спецификации компонентов приводятся к однородному представлению в канонической модели. Предполагается также, что спецификация требовании также представляется в канонической модели (хотя для этого может потребоваться преобразование в такую модель из некоторого другого языка спецификаций, например из UML). В настоящей работе рассматриваются следующие виды композиции: соединение и пересечение абстрактных типов данных2. Неформально, соединение Т\ U спецификаций типов Т\ и Т2 включает всю информацию, содержащуюся в спецификациях Т\ и Т2; пересечение Т\ П Т2 включает лишь общую информацию из спецификаций Т\ и Т2.

Методы решения вышеперечисленных задач разрабатывались в течении ряда лет в Лаборатории композиционных методов проектирования информационных систем Института проблем информатики РАН. Для однородного представления разнообразных информационных источников, описания моделей предметных областей, проектирования и программирования ИС в интероперабельных средах было разработано ядро канонической модели представления информации - язык СИНТЕЗ [20]. Для достижения всех указанных целей в языке СИНТЕЗ совместно используются парадигмы моделей представления знаний о предметных областях и спецификаций требований к ИС [21], моделей концептуального проектирования ИС [22, 23], объектно-ориентированных моделей данных [24, 25], логического программирования в дедуктивных базах данных [26, 27, 28], систем управления неоднородными мультибазами данных [29, 30], предикативных спецификаций ИС [23, 31].

2Понятие абстрактного типа данных подробно обсуждается в разделе 2.2. операции соединения и пересечения определяются в разделе 2.6.1.

Были также разработаны методы расширения канонической модели [30, 32, 33], методы и средства композиционного проектирования И С [18, 34, 35], методы и средства интеграции множественных неоднородных источников [17, 36]. Необходимо заметить, что использование языка СИНТЕЗ в качестве ядра канонической модели не предполагает отказа от распространенных методов и моделей, таких как ОМТ [37], UML [38]: с их помощью могут осуществляться анализ ИС и обратная инженерия. Для решения более сложных задач - интеграции информационных источников и композиционного проектирования ИС - требуется более точная информационная модель. Поэтому такие модели, как ОМТ и UML должны быть отображены в каноническую информационную модель.

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

Цель и задачи работы

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

Достижение цели предполагает решение следующих задач:

1. для проведения доказательных рассуждений о моделях информационных ресурсов, например, рассуждений об их непротиворечивости, об уточнении или отображении моделей, разработка метода формального определения канонических информационных моделей, определение на его основе формальной семантики ядра канонической модели (языка СИНТЕЗ);

2. для автоматизации формального доказательства уточнения полных спецификаций требований спецификациями компонентов, а также доказательства непротиворечивости спецификаций, разработка метода моделирования канонических информационных моделей в теоретико-модельном формальном языке спецификаций, разработка на его основе алгоритмов отображения ядра канонической модели в формальный язык. В качестве такого языка в настоящей работе выбрана Нотация Абстрактных Машин (Abstract Machine Notation, AMN)[1], что позволит использовать существующую технологию доказательства уточнения (B-technology [39]) и инструментальные средства доказательства уточнения (B-Toolkit [40], Antelier В[41] ) для доказательства уточнения спецификаций канонической модели;

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

4. создание на основе этих алгоритмов инструментального средства автоматического отображения спецификаций канонической модели в AMN и разработка методики использования этого средства совместно с B-Toolkit при решении практических задач проектирования ИС.

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

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

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

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

• разработан метод формального определения канонических информационных моделей и на его основе - формальная денотационно-аксиоматическая семантика языка СИНТЕЗ;

• разработан метод моделирования канонических информационных моделей в языке AMN и на его основе - алгоритмы отображения языка СИНТЕЗ в AMN;

• разработан метод доказательства корректности отображения информационных моделей с использованием их денотационно-аксиоматнчес-кой семантики; с использованием метода было построено доказательство корректности алгоритмов отображения языка СИНТЕЗ в AMN;

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

Практическая ценность

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

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

Реализация результатов работы

Результаты диссертационной работы использованы в проектах РФФИ 0107090084, 03-01-00821, 05-07-90413-в; проекте № 1-10 программы фундаментальных исследований ОИТВС РАН "Фундаментальные основы информационных технологий и систем", НИР Контекст "Контекстуализация неоднородных информационных источников в предметном информационном посреднике", НИР И3НИ "Композиционные методы решения задач в инфраструктурах интеграции информации для научных исследований".

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

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

Основные результаты диссертации докладывались на Международных конференциях ADBIS (Братислава 2002, Будапешт 2004), на XXIV Конференции молодых ученых механико-математического факультета МГУ им. М.В. Ломоносова (Москва, 2002), на Международном симпозиуме по базам данных конференции VLDB (Берлин 2003), на II научной сессии ИПИ

РАН (Москва, 2005), на научных семинарах лаборатории Композиционных методов проектирования информационных систем Института проблем информатики РАН.

На защиту выносятся следующие, полученные автором результаты:

• метод формального определения канонических информационных моделей; формальная денотационно-аксиоматическая семантика языка СИНТЕЗ;

• метод моделирования канонических информационных моделей в теоретико-модельном языке AMN; алгоритмы отображения языка СИНТЕЗ в AMN;

• метод доказательства корректности отображения информационных моделей с использованием их денотационно-аксиоматической семантики; доказательство корректности алгоритмов отображения языка СИНТЕЗ в AMN;

• разработанное на основе указанных алгоритмов инструментальное средство автоматического отображения спецификаций ядра канонической модели в AMN;

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

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

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

Структура работы

Текст диссертации включает введение, пять глав, заключение, список литературы и четыре приложения.

Заключение диссертации по теме «Теоретические основы информатики», Ступников, Сергей Александрович

5.4. Выводы по главе

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

Представлено инструментальное средство автоматического отображения спецификаций канонической модели в AMN, реализующее алгоритмы, определенные в главе 3. Инструментальное средство встроено в прототипы средств композиционного проектирования и интеграции информационных источников, разработанные в лаборатории композиционных методов проектирования ИС ИПИ РАН.

Методика использования инструментального средства для автоматизации доказательства корректности решения задачи синтеза канонических моделей продемонстрирована на примере расширения канонической информационной модели (языка СИНТЕЗ) на основе типа связи языка ODL стандарта ODMG.

Методика использования инструментального средства для автоматизации доказательства корректности решения задачи композиции ИС из компонентов продемонстрирована на примере системы назначения экспертов Исследовательского фонда.

Заключение

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

• разработан метод формального определения канонических информационных моделей и па его основе - комбинированная денотационно-аксиоматическая семантика ядра канонической объектной информационной модели (языка СИНТЕЗ), позволяющая проводить доказательные рассуждения о моделях информационных ресурсов;

• разработан метод моделирования канонических информационных моделей в теоретико-модельном языке спецификаций, основанном на логике предикатов первого порядка и теории множеств - Нотации Абстрактных Машин (AMN) и на его основе - алгоритмы отображения ядра канонической информационной модели в AMN, позволяющие использовать инструментальные средства доказательства уточнения для автоматизированного доказательства уточнения спецификаций канонической модели;

• разработан метод доказательства корректности отображения информационных моделей с использованием их денотационно-аксиоматической семантики; с использованием метода было построено доказательство корректности алгоритмов отображения ядра канонической модели в AMN;

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

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

Список литературы диссертационного исследования кандидат технических наук Ступников, Сергей Александрович, 2006 год

1. Abrial J.-R. The B-Book: Assigning Programs to Meanings. - Cambridge: Cambridge University Press, 1996.

2. Spivey J. The Z Notation: A Reference Manual. L. Prentice Hall, 1992.

3. R. Duke and G. Rose. Formal Object Oriented Specification Using Object-Z. Macmillan, 2000.

4. Fitzgerald J., Larsen P.G., Mukhcrjee P., Plat N., Vcrhocf M. Validated Designs for Object-oriented Systems. Springer-Verlag, 2005.

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

6. Milner R. Communication and Concurrency. L.: Prentice Hall, 1989.

7. Mahony В., Dong J.S. Timed Communicating Object Z // IEEE Transactions on Software Engineering. 2000. - V. 26, №2. - P. 150-177.

8. Butler M. J. csp2B: A Practical Approach To Combining CSP and В // Formal Aspects of Computing. 2000. - N. 12. - P. 182-198.

9. Borger E., Stark R. Abstract State Machines: A Method for High-Level System Design and Analysis. Springer Verlag, 2003.

10. Del Castillo G. The ASM Workbench: PhD thesis. Paderborn: Department of Mathematics and Computer Science of Paderborn University, 2000.

11. RAISE Language Group. The RAISE Specification Language. L.: Prentice Hall, 1992.

12. Back J.R., Von Right J. Refinement Calculus. N.Y.: Springer-Verlag, 1998.

13. Hehner E. C. R. A Practical Theory of Programming. N.Y.: Springer-Verlag, 1993.

14. Morgan C. Programming from Specifications. Hempstead: Prentice Hall,1990.

15. Storey N. Safety-Critical Computer Systems. Boston: Addison-Wesley, 1996.

16. Johnson B. Design and Analysis of Fault-Tolerant Digital Systems. -Boston: Addison Wesley, 1989.

17. The Common Object Request Broker: Architecture and Specification / OMG, document number 91.12.1. 1991.

18. Калипичепко Л.А. СИНТЕЗ: язык определения, проектирования и программирования интероперабельных сред неоднородных информационных ресурсов. Москва: ИПИ РАН, 1993.

19. Koubarakis М., Mylopoulos J., Stanley М., Borgida A. Telos: features and formalization: Technical Report / University of Toronto. KRR-TR-89-4.- 1989.

20. Borgida A. et al. Support for data-intensive applications: conceptual design and software development: Technical Note / University of Toronto. CSRI-51. - 1989.

21. Jarke M. et al. Information system development as knowledge engineering: a review of the DAIDA project. // Programmirovanic. 1991. - N 1.

22. Atkinson M. et al. The object-oriented database system manifesto // Proc. DOOD'89. 1989. - P. 40-57.

23. Soley R. Object Management Architecture Guide / OMG document 90.9.1.- Framingham, 1990.

24. Abiteboul S. Towards a deductive object-oriented database language // Proc. DOOD'89. 1989. - P. 419-438.

25. Ceri S., Gottlob В., Tanca L. Logic programming and databases. -Spronger-Verlag, 1990.

26. Naqvi S., Tsur S. A logical language for data and knowledge bases. -Freeman Publ., 1989.

27. Калиниченко JI.A. Методы и средства интеграции неоднородных баз данных. Москва: Наука, 1983. - 423 с.

28. Kalinichenko L.A. Methods and tools for equivalent data model mapping construction // Proc. EDBT'90 Conference. Springer-Verlag, 1990. - 92119.

29. Borgida A., Mertikas M., Schmidt J.W., Wetzel I. specification and refinement of database applications: Report / Universitaet Hamburg. -ESPRIT 892. Hamburg, 1990.

30. Kalinichenko L.A. Method for Data Models Integration in the Common Paradigm // Advances in Databases and Information Systems: Proc. of the First East-European Conference. St. Petersburg: Nevsky Dialekt, 1997. -P. 275-284.

31. Kalinichenko L.A. Compositional Specification Calculus for Information Systems Development // Advances in Databases and Information Systems: Proc. of the 3rd East European Conference. Berlin-Heidelberg: Springer-Verlag, 1999. - P. 317-331.

32. Брюхов Д.О. Конструирование информационных систем на основе интероперабельных сред информационных ресурсов: Дис. каид. техн. наук: 05.13.11 М.: ИПИ РАН, 2003. - 158 с.

33. Rumbaugh J. et al. Object Oriented Modeling and Design. L.: Prentice Hall, 1991.

34. OMG Unified Modeling Language Specification Version 1.5 / http://www.omg.org 2003.

35. Abrial J.-R. B-Technology: Technical overview. B-Core (UK) Ltd., 1993.40. http://www.b-corc.com/ONLINEDOC/BToolkit.html41. http://www.atelierb.societe.com/indexuk.html

36. Tennent R.D. The denotational semantics of programming languages // CACM. 1976. - V. 19, №8. - P.437-453.

37. Allison L. A Practical Introduction to Denotational Semantics. -Cambridge: Cambridge University Press, 1986.

38. Schmidt D. Denotational Semantics: A Methodology for Language Development. Dubuque: William C. Brown Pub., 1988.

39. Stoy J.E. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. Cambridge: MIT Press, 1977.

40. Winskel G. The Formal Semantics of Programming Languages. -Cambridge: MIT Press, 1993.

41. Response to the UML 2.0 OCL Rfp (ad 2000-09-03). Revised Submission, version 1.6 / http://www.omg.org 2003.

42. Bruel J.M., France R.B. Transforming UML models to formal specifications // UML'98: Beyond the Notation: Proc. of 1st International Workshop. -Springer-Verlag, 1999.

43. France R.B., Grant E., Bruel J.M. UMLtranZ: An UML-based rigorous requirements modeling technique: Technical report/ Fort Collins: Colorado State University, 2000.

44. Kim S., Carrington D. A Formal Mapping between UML Models and Object-Z Specifications // ZB2000 Formal Specification and Development in Z and B: Proc. First International Conference of В and Z users. -Springer-Verlag, 2000. P. 2-21.

45. Kim S., Carrington D. A formal denotational semantics of UML in Object-Z // L'OBJET. 2001. - V. 7, N. 1.

46. Roe D., Broda K., Russo A. Mapping UML Models incorporating OCL Constraints into Object-Z: Technical Report / Imperial College. N 2003/9.- L., 2003.

47. Lano K., Bicarregui J. Formalising the UML in Structured Temporal Theories / Technical Report TUM-I9813: Proceedings of the ECOOP 98 Workshop on Behavioural Semantics. Munchen: Technische Universitat Munchen, 1998.

48. Lano K., Bicarregui J. UML Refinement and Abstraction Transformations // Proc. ROOM 2 Workshop. Bradford: Bradford University, 1998.

49. K. Lano, J. Bicarregui, A. Evans. Structured Axiomatic Semantics for UML Models // Rigorous Object-Oriented Methods: Proc. of the Conference. -http://ewic.bcs.org/conferences/2000/objectmethods/papers/ paper5.htm- 2000.

50. Lano K. Logical Specification of Reactive and Real-Time Systems // Journal of Logic and Computation. 1998. - V. 8, N. 5. - P. 679-711.

51. Baar Т., Beckert В., Schmitt P.H. An Extension of Dynamic Logic for modeling OCL's @pre operator // Perspectives of System Informatics: Proc. Fourth Andrei Ershov International Conference. Springer-Verlag, 2001.

52. Beckert В., Keller U., Schmitt P. Translating the Object Constraint Language into First-order Predicate Logic // Proc. VERIFY: Workshop at Federated Logic Conferences. Copenhagen, 2002.

53. Riedel H., Scholl M.H. The CROQUE-model: Formalization of the data model and query language: Technical Report,/ Dept. of Mathematics and Computer Science. N. 23/96. - Konstanz: University of Konstanz, 1996.

54. Riedel H., M.H. Scholl. M.H. A formalization of ODMG queries // Proc. 7th Intnl. Conf. on Data Semantics. L.: Chapman and Hall, 1997. - P. 219-247.

55. Cherniack M. Translating queries into combinators: Technical report / Brown University. RI 02912. - Providence, 1996.

56. Cherniack M., Zdonik S.B. Rule languages and internal algebras for rule-based optimizers // ACM SIGMOD record. 1996. - V. 25, N. 2. - P. 401-412.

57. Brown S. A. The Semantics of Database Query Languages: Ph.D. Thesis.- Sheffield: Sheffield University, 1999. 203 p.

58. Von Wright J. Program Refinement by Theorem Prover // Proc. 6th Refinement Workshop. Springer Verlag, 1994.

59. Gordon M.J.C., Melham T.F. Introduction to HOL. NY: Cambridge University Press, 1993.67. http://www.ora.on.ca/z-eves/index.html68. http://www.vdmbook.com/tools.php

60. Bicarregui J.C., Ritchie B. Reasoning About VDM Developments Using The VDM Support Tool in Mural // VDM 91: Formal Software Development Methods. Springer-Verlag, 1991. - P. 371-388.

61. RAISE Method Group. The RAISE Development Method. L.: Prentice Hall, 1995.

62. George C. RAISE Tools User Guide: Technical Report / UNU/IIST. 227.- Macau, 2001.

63. Dasso A., George C. Transforming RSL into PVS: Technical Report / UNU/IIST. 256. - Macau, 2002.

64. Owre S., Rushby J.M., Shankar N. PVS: A Prototype Verification System // Proc. 11th International Conference on Automated Deduction. -Springer-Verlag, 1992. P. 748-752.

65. Dijkstra E. W. A Discipline of Programming. L.: Prentice Hall, 1976.

66. Behm P., Benoit P., Faivre A., Meynaider J. M. METEOR: A Successful Application of В in a Large Project // World Congress on Formal Methods: Proc. of FM'99. 1999. - P. 369-387.76. http://www.matisse.qinetiq.com/

67. Abrial J. R., Cansell D., Mery D. A Mechanically Proved and Incremental Development of IEEE 1394 Tree Identity Protocol // Formal Aspects of Computing. 2003. - V. 14, N 3. - P. 215-227.

68. Facon, P., Laleau, R., Nguyen, H. Mapping Object Diagrams into В Specifications // In Proc. Methods Integration Workshop. -http: //ewic.bcs.org/conferences/1996/ methodsintegration / papers / paper6.pdf 1996.

69. Meyer E., Souquieres Л. A Systematic Approach to Trabsform OMT Diagrams to а В Specification // Proc. FM'99. Springer-Verlag, 1999. - P. 875-895.

70. Lano K. The В Language and Method: A Guide to Practical Formal Development. Springer-Verlag, 1996.

71. Snook C., Butler M. Tool-Supported Use of UML for Constructing В Specifications: Technical Report / Southampton University. DSSE-TR-2002-3. - Highfield, 2002.

72. Ledang H., Souquieres J. Modeling class operations in B: application to UML behavioral diagrams // Proc. of ASE 2001. Washington: IEEE Computer Society, 2001. - P. 289-296.

73. Ledang H., Souquieres J. Integration of UML and В Specification Techniques: Systematic Transformation from OCL Expressions into В // Proc. of APSEC 2002. Washington: IEEE Computer Society, 2002. - P. 495-506.

74. Ledang H., Souquieres J. Contributions for Modeling UML State-Charts in В // Integrated Formal Methods: Proceedings of the Third International Conference. Springer-Verlag, 2002. - P. 109-127.

75. Ledang H., Souquieres J., Charles S. ArgoUML+B : Un outil de transformation systematique de specifications UML vers B// Proc. of AFADL'2003. Rennes: IRISA, 2003. - P. 3-18.87. http://argouml.tigris.org/

76. Ledang H., Souquicres J. Formalizing UML Behavioral Diagrams with В // Proceedings of Tenth OOPSLA Workshop on Behavioral Semantics: Back to Basics. Northeastern University Press, 2001. - P. 162-171.

77. Kalinichenko L.A. Data model transformation method based on axiomatic data model extension // 4th International Conference on Very Large Data Bases (VLDB): Proceedings. 1978.

78. Калиниченко JI.A., Ступников C.A., Земцов H.A. Синтез канонических моделей для интеграции неоднородных источников информации. ИПИ РАН, 2005. - 87 с.

79. The Object Database Standard: ODMG-93 / Ed. R.G.G. Cattell. San Mateo: Morgan Kaufmann Publ., 1994. - 169 p.

80. Ступников C.A. Отображение канонической модели спецификаций в формальную нотацию для моделирования уточняющих спецификаций // Труды XXIV Конференции молодых ученых. М.: МГУ им. М.В. Ломоносова, 2002. - С. 169-171.

81. Стуиников С.А. Формальная семантика ядра канонической объектной информационной модели // там же. С. 40-68.

82. Ступников С.А. Отображение спецификаций, выраженных средствами ядра канонической модели, в язык AMN // там же. С. 69-95.

83. Ступников С.А. Автоматизация верификации уточнения при композиционном проектировании информационных систем и посредников // там же. С. 96-119.

84. Ступников С.А., Брюхов Д.О. Представление UML и OCL в канонической информационной модели // там же. С. 120-129.

85. Калиниченко Л.А., Ступников С.А., Земцов Н.А. Каноническая модель процессов и ее формальная интерпретация // там же. С. 130-151.

86. В. Нотация абстрактных машин

87. В.1. Спецификация состояний системы в AMN

88. В таблице В.1 собраны основные теоретико-множественные обозначения AMN. Здесь 5, Т, U, s,t обозначают множества, причем 5 С S и t С Т; г, п, Г2, q отношения из 5 в Т, g - отношение из Т в U.