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

Российская Академия Наук Институт Проблем Информатики

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

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

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

05.13.17 — Теоретические основы информатики

Автореферат диссертации на соискание ученой степени кандидата технических наук

Москва 2005

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

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

профессор Л. А. Калиниченко

доктор технических наук, профессор В. А. Сухомлин

Официальные оппоненты — доктор физико-математических наук

А. К. Петренко

кандидат физико-математических наук Р. Э. Яворский

Ведущая организация — Институт Проблем Управления РАН

Защита диссертации состоится „ '( " 200&Г. в ч.ОО мин.

на заседании диссертационного совета Д.002.073.01 при Институте проблем информатики РАН по адресу: 119333 г. Москва, ул. Вавилова, 44, корп. 2.

С диссертацией можно ознакомиться в библиотеке Института проблем информатики РАН.

Отзывы в одном экземпляре, с заверенной подписью, просим направлять по адресу: 119333, Москва, ул. Вавилова, 44, корп. 2, в диссертационный совет.

Автореферат разослан „19 й е^е^с^Л 20(Рг\

Ученый секретарь

диссертационного совета Д.002.073.01 доктор технических наук,

С. Н.Гринченко

CU>OGA

57

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

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

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

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

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

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

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

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

РОС НАЦИОНАЛЬНАЯ 3 БИБЛИОТЕКА

f ПлайКтГ

системах (safety-critical), или задачи разработки отказоустойчивых (fault-tolerant) систем, способных продолжать работу при наличии сбоев.

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

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

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

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

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

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

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

Основная идея композиционного проектирования состоит в том, чтобы построить корректную композицию спецификаций существующих компонентов (информационных, программных), уточняющую спецификацию требований к разрабатываемой ИС. При этом спецификации требований и существующих компонентов представляются в канонической модели. Реальные компоненты реализуются в разнообразных языках программирования, моделях данных. Техническая интероперабелыюсть неоднородных компонентов достигается применением архитектур и компонентных моделей, подобных СОШЗА. Тем самым технически обеспечивается возможность композиции компонентов. В целях проектирования спецификации компонентов приводятся к однородному представлению в канонической модели. Предполагается также, что и спецификация требований представляется в канонической модели (хотя для этого может потребоваться преобразование в такую модель из некоторого другого языка спецификаций, например из 1)МЬ). В настоящей работе рассматриваются следующие виды композиции: соединение и пересечение абстрактных типов данных1. Неформально, соединение Т\ и Т-2 спецификаций типов 7\ и Т-г включает всю информацию, содержащуюся в спецификациях Т\ и Т2; пересечение Т\ П 7г включает лишь общую информацию из спецификаций Т\ и Т2.

Методы решения вышеперечисленных задач разрабатывались в течении ряда лет в Лаборатории композиционных методов проектирования инфор-

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

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

Были также разработаны методы расширения канонической модели, методы и средства композиционного проектирования ИС, методы и средства интеграции множественных неоднородных источников. Необходимо заметить, что использование языка СИНТЕЗ в качестве ядра канонической модели не предполагает отказа от распространенных методов и моделей, таких как ОМТ, иМЬ: с их помощью могут осуществляться анализ ИС и обратная инженерия. Для решения более сложных задач - интеграции информационных источников и композиционного проектирования ИС - требуется более точная информационная модель. Поэтому такие модели, как ОМТ и иМЬ должны быть отображены в каноническую информационную модель [8].

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Структура и объем работы. Диссертация состоит из введения, пяти глав, заключения, списка литературы и четырех приложений. Основное содержание работы изложено на 157 страницах текста, включая 7 рисунков и 3 таблицы. Список литературы содержит 104 наименования.

Содержание работы

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

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

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

В течении последних лет в лаборатории композиционных методов проектирования ИС ИПИ РАН проводились интенсивные исследования по разработке методов решения задач над неоднородными информационными источниками, таких как композиционное проектирование ИС, регистрация источ-

ников в предметных посредниках, интеграция моделей источников, переписывание запросов в среде посредников [3]. В процессе этих исследований постоянно проявлялась необходимость формального определения канонической объектной информационной модели (при использовании языка СИНТЕЗ в качестве ее ядра) при манипулировании разнообразными информационными моделями - задания ее (канонической модели) формальной семантики. Формальная семантика необходима для проведения доказательных рассуждений о моделях информационных ресурсов. Имея формальную семантику, можно строго формулировать утверждения о непротиворечивости и уточнении спецификаций, выраженных в модели. Появляется возможность доказательства корректности отображений одних моделей информационных ресурсов в другие модели. В частности, синтез канонической модели строится как расширение ее ядра для каждой конкретной модели информационного ресурса так. что ядро вместе с таким расширением должно уточняться этой конкретной моделью. Для таких манипуляций информационными моделями и выраженными в них спецификациями требуется выражение их семантики в некотором формальном языке, позволяющем осуществлять доказательство непротиворечивости и уточнения спецификаций. В настоящей работе в качестве такого языка выбрана Нотация Абстрактных Машин (АЛДО), которая позволяет осуществлять необходимые рассуждения относительно спецификаций. Для AMN разработаны специальные инструментальные средства, составляющие в совокупности так называемую В-технологию. Для того, чтобы можно было манипулировать спецификациями информационных моделей в рамках В-технологии (в частности, доказывать корректность отношения уточнения между спецификациями, выраженными в различных моделях), необходимо корректно отобразить такие модели в язык АМК с сохранением семантики. В настоящей работе создан метод такого отображения и показано, как его следует применять на примере ядра канонической информационной модели (языка СИНТЕЗ).

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

могут быть использованы инструментальные средства доказательства уточнения (например, В-технология). Их использование будет доказательно правильным, если доказана корректность отображения ядра в соответствующую модель (например, АМ1Ч).

Таким образом, одной из важнейших проблем моделирования композиционных уточняющих спецификаций является формализация соответствующих им языковых конструкций. В разделе 1.2 приведен обзор основных существующих методов формального определения информационных моделей, близких к ядру канонической модели. Цель обзора состояла в выявлении общих закономерностей и особенностей формального определения информационных моделей, которые могут быть использованы при формальном определении ядра канонической модели. Рассмотрены также специфические черты канонической модели, не представленные или слабо представленные в существующих информационных моделях, потребовавшие разработки адекватных методов формального определения. Среди таких особенностей: определенные в канонической модели операции композиции типов и решетка типов; четкое разделение понятий типа данных, как описания структуры и поведения значений типа, и коллекции, как множества значений некоторого типа; иерархия обобщения-специализации на множестве типов и на множестве коллекций; предикативные спецификации функций - формулы, задающие смешанные пред и постусловия функции и содержащие предикаты-коллекции, вызовы функций (в том числе с побочными эффектами), кванторы существования и всеобщности; язык правил (использующихся, в частности, как запросы к коллекциям), содержащий операции соединения, пересечения, объединения, селекции и проекции объектных и необъектных коллекций.

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

В разделе 1.4 рассмотрены существующие подходы к моделированию в АЛШ информационных моделей, близких к ядру канонической модели. Указано, что ни один из известных подходов не ориентирован на доказательство уточнения с использованием В-технологии. Выделены основные черхы, отличающие представленный в настоящей работе метод моделировании спецификаций в AMN от других существующих методов: однородность (ЛМ1Ч-спецификация, полученная в результате отображения канонической спецификации, может быть использована и как уточняющая спецификация, и как уточняемая); использование усовершенствованного экстенсионального принципа моделирования АТД; представление в АМДО специфических черт канонической модели.

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

Формальное определение ядра заключается в сообщении канонической модели комбинированной денотационно-аксиоматической семантики. Методология денотационной семантики в обобщенном смысле предполагает отображение синтаксических конструкций модели в математические объекты: целые числа, логические значения, функции и т.д. В настоящей работе методы денотационной семантики используются для отображения синтаксиса модели в объекты теории множеств и логики предикатов первого порядка.

Методы денотационной семантики удобны для определения пространства состояний системы, задаваемой спецификацией модели. Множество допустимых состояний системы задается при помощи наложения ограничений К на пространство состояний S. Множество ограничений К представляет собой теорию (множество формул) первого порядка, формулы которой определены на S. Кроме К, в аксиоматическую часть семантики модели входит множество предикатов F, отвечающих спецификациям методов АТД и спецификациям функций, не являющихся методами АТД. Таким образом, семантикой спецификации модели является совокупность пространства состояний S, теории R, а также множества предикатов F.

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

С синтаксическими доменами ассоциированы метапеременпые, которые используются вместо элементов соответствующих доменов при описании семантических функций. Например, синтаксическому домену ModulcSpec (спецификация модуля - основной единицы определения канонической модели) соответствует переменная MS:

MS : ModuleSpec = TypeSection x Functionsection x IRSection

Спецификация модуля состоит из секции типов TypeSection, секции функций Functionsection и секции описания информационных источников IRSection.

В разделе 2.2 излагается основная идея, на которой базируются принципы построения пространства состояний - идея экстенсиональной интерпретации абстрактных типов данных.

Определение. Абстрактный тип данных Т есть тройка {Vt, От, 1т), где Vt - экстенсионал типа, От множество операций типа, 1т инвариант типа.

Спецификацию типа в канонической модели составляют От и 1т, экстенсионал Vt используется для придания формальной семантики спецификации типа и является предопределенным множеством (семантическим доменом). Различается собственный и полный экстенсионалы типа. Собственным экс-тенсионалом V?r типа Т называется множество значений типа Т, не являющихся значениями никакого подтипа типа Т. Полным экстенсионалом V? типа Т называется объединение и полных экстенсионалов всех подтипов типа Т. Объединение экстенсионалов всех типов есть множество AVAC (Ahstract VALues).

Множество операций От представляет собой объединение множеств атрибутов и методов AtöFt- Семантически, атрибут представляется константной функцией а : Vt —► Е(а). При этом Е(а) множество значений, которое может принимать атрибут. Например, если тип а - целочисленный, то Е(а) = Z (множество целых чисел), если тип а - необъектный абстрактный тип Т, то Е(о) = Vt, если тип а объектный абстрактный тип, то Е(а) — U, где U -предопределенное множество (семантический домен) объектных идентификаторов.

Состояние системы, задаваемой спецификацией модуля канонической модели, характеризуется составом источников, определенных в спецификации, а также состоянием объектов. Состав источника с экземплярами типа Т есть некоторое подмножество экстенсионала Vj. Состав всех источников в совокупности задается функцией С € [Ic —> №(AVAC)], где 1с - множество имен коллекций, определенных в спецификации. Состояние объектов задается функцией <S С [U AVAC\. Пространство состояний системы, которому принадлежит упорядоченная пара функций S С, обозначается § = [U -+» AVAC] х [Ic Р{AVAC)] (декартово произведение множества частичных функций из U в AVAC и множества тотальных функций из 1с в множество подмножеств множества AVAL).

Следующий элемент денотационной семантики семантические домены -определяют абстрактные математические объекты, которые мы хотим счи-

тать семантикой спецификации. На основе элементарных доменов, например, множества логических значений В = {true, false}, при помощи операторов конструирования домепов строятся производные семантические домены. В число операторов входят декартово произведение х, сумма +, конструктор множества подмножеств Р(-), конструктор упорядоченной пары кон-

структор функционального домена [•—>•]•

Семантические функции отображают абстрактные синтаксические структуры в соответствующие семантические объекты. Семантические функции, формирующие пространство состояний, являются, по существу, сложными конструкторами семантических доменов, и само пространство состояний представляет собой сложный семантический домен. Семантические функции задаются при помощи сигнатур и семантических соотношений. Сигнатура определяет имя и область определения функции. Семантические соотношения определяют, каким образом функция действует на том или ином синтаксическом домене. Аргументы семантических функций - синтаксические объекты - заключаются в специальные скобки [•], для того, чтобы отделить их от семантических объектов. Семантические домены и семантические функции построения пространства состояний описаны в разделе 2.3. Например, семантическая функция sModuleSpec, формирующая пространство состояний по спецификации модуля, определяется следующим образом:

sModuleSpec[TS FS IRS} = sTypeSeciion{TS\ х sIRSecUon[IRS] Сигнатура функции состоит из имени - sModuleSpec и области определения - синтаксического домена ModuleSpec. Метапеременные TS, FS, IRS принимают значения из синтаксических доменов TypeSection, FunctionSection и IRSection, соответственно. Имена всех семантических функций имеют префикс s, от слова semantic - семантический. Знак = используется в работе при определении семантических функций. Пространство состояний конкретного модуля определяется как декартово произведение результатов семантических функций STypeSection и sIRSection.

Итак, в разделе 2.3 показано, каким образом семантические функции формируют пространство состояний на основании некоторой спецификации канонической модели. Пусть семантический домен S есть пространство состояний, полученное на основании некоторой спецификации М.

Заметим, что система, задаваемая спецификацией М, может находиться не во всех состояниях из S. Множество §° состояний, в которых система действительно может находиться, - множество допустимых состояний -является собственным подмножеством S, элементы которого удовлетворяют:

• ограничениям типизации экземпляров классов;

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

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

• ограничениям инвариантов.

Ограничения, выраженные в виде формул логики предикатов первого порядка, составляют множество R = {ф\,..., фп}, т.е.

§° = {5 >->■ С е § | фх Л ... Л фп}

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

В разделе 2.5 определены семантические функции формирования предикатов, отвечающих функциям канонической модели. Рассмотрим в качестве примера спецификацию метода типа Student, увеличивающего стипендию студента на величину rise в случае, если рейтинг студента выше, чем limit:

raiseScholarship: -С in: function; params: { +limit/integer, +rise/mteger }; { predicative:

{ this.rating >= limit -> this.scholarship^ this.scholarship+rise >

>;

>

Действие метода задается предикативной спецификацией, описывающей смешанные предусловия и постусловия метода. Для выражения условий, связанных с изменением состояния ИС, ссылки на значения переменных при завершении метода изображаются идентификаторами переменных, выделенными следующими после них апострофами. Переменные без апострофа ссылаются на исходное состояние ИС. Таким образом, предикативные спецификации методов это формулы не просто над S, но над S х §, где первый компонеш отвечает за исходное состояние ИС, второй - за конечное. Кроме тою, у метода есть параметры, не связанные с состоянием ИС (limit, rise), а потому для того, чтобы полностью определить пространство, над которым действует предикативная спецификация метода, нужно добавить к S х S семантические домены типов параметров (множества Z целых чисел). Семантикой данного метода является Student. raiseScholarship - предикат, определенный на пространстве § х Z х Z х § следующим образом:

Student. raiseScholarsh.ip (v. limit, rise) ^ v G Vstudent A limit G Z Л rise G Z Л 3 w • ((rating(v) > limit w = scholarship(v) + rise) Л 5' = S <J~{self(v) м- (»; <3-{scholarship w})})

где операция перекрытия отношения г\ отношением г2, г\ <3определяется как г\ <Ьг2 = dom(f2 < т\) U Гг, операция антиограничения отношения г множеством s - я ^ г = {z, dorn г — s}.

Вообще, предикативная спецификация метода может быть формулой либо правилом. Правило отличается от формулы тем, что (1) не может содержать конструкции, изменяющие состояние системы, и (2) может содержать такие операции композиции коллекций, типичные для языков запросов, как соединение и объединение коллекций. Семантика правил канонической модели рассмотрена в разделе 2.6, семантика формул - в разделе 2.7.

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

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

Отображение задается при помощи семантических функций, определенных на синтаксических доменах абстрактного синтаксиса канонической модели, а также при помощи алгоритмов. Модуль, как основная единица определения канонической модели, является единицей отображения канонической модели в AMN. Модуль представляется в AMN набором конструкций (абстрактных машин), состоящим из контекстной машины и машин, соответствующих АТД модуля. Контекстная машина содержит информацию, характеризующую модуль как целое, машины типов содержат информацию, характерную для отдельных типов. Таким образом, для модуля М канонической модели, &(М) = {Mctxt} U Мtype», где Mctxt контекстная машина, Mtypes - множество машин, соответствующих АТД.

В разделе 3.1 изложены основные принципы моделирования канонических спецификаций в AMN. Моделирование АТД в AMN, также, как и формальная семантика АТД, базируется на экстенсиональном принципе: тип моделируется множеством своих экземпляров. Такое множество экземпляров называется экстепсионалом типа. В отличие от понятия экстенсионала в формальной семантике канонической модели, экстенсионал типа в AMN представляет собой

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

Такой подход, в отличие от прямого моделирования в AMN семантики АТД, позволяет избежать бесконечности экстенсионалов и значительно упро-* щает моделирование функций в AMN операциями абстрактных машин. При этом упрощается процесс автоматического/интерактивного доказательства уточнения. Правомерность подобного подхода обоснована сохранением семантики канонической модели при отображении в AMN (доказательство этого факта приводится в главе 4 настоящей работы).

Для моделирования потенциальных экземпляров всех абстрактных типов вводится множество AVAL, и для каждого типа Т с экстенсионалом Е? выполнено включение Еу С AVAL. Заметим, что поскольку AVAL представляет собой множество потенциальных экземпляров типов, то оно значительно отличается от множества AVAC, используемого для моделирования экземпляров типов при определении семантики канонической модели.

Экстенсионалы типов соотносятся в соответствии с отношением тип-подтип: для каждой пары типов 7\, 7г, где Тг является подтипом Ti, выполнено отношение включения на экстенсионалах Ef2 С Ej¡. Таким образом моделируется иерархия типов.

Спецификации типов канонической модели могут ссылаться друг на друга в спецификациях атрибутов, методов, инвариантов, образуя структуру спецификаций типов. Основным принципом отображения структуры спецификаций типов канонической модели в AMN является стремление отобразить каждый АТД отдельной абстрактной машиной. Проблема состоит в том, что средства композиции абстрактных машин в AMN являются гораздо менее гибкими, чем средства организации структуры спецификаций типов канонической модели. Данное противоречие разрешается при иомощи процедуры преобразования ориентированного графа структуры модуля М, представляющего композиционную структуру спецификаций типов модуля, — DSG(M), в ориентированный граф, представляющий композиционную структуру набора абстрактных машин, — DAMSG(M). Алгоритм преобразования изложен в разделе 3.1.3.

В разделе 3.2 рассмотрены правила формирования контекстной машины Mclxt по спецификации модуля М канонической модели. Основное содержание

контекстной машины составляют экстенсионалы типов и отношения между экстенсионалами.

Правила формирования машин из множества Mtypes рассмотрены в разделе 3.3. Рассмотрены методы моделирования атрибутов, методов, инвариантов абстрактных типов конструкциями AMN. Так, например, атрибут а типа Т моделируется функциональной переменной с именем а и областью определения Ет- Метод meth типа Т с входными параметрами р'к, выходными параметрами pf, предикативной спецификацией /: meth :{in:function; params: {+Pi/ 7i,..., +pn/Tn, -pn+i/T„+1,..., -pm/Tm}; {predicative: {/}};

}

представляется в AMN операцией с именем meth-op. Операцию формирует семантическая функция mMethodSubst (все семантические функции отображения канонической модели в AMN имеют префикс т). На вышеприведенной спецификации метода meth функция действует следующим образом: Рп+ь ■■■,Рт<- meth-op(o, рь ..., рп) = PRE о 6 extJF A pi € Е(Т\) А ... А рп Е Е(Тп) THEN

mSubstitution\fJ END

Первым входным параметром операции meth^op является объект, для которого вызывается метод meth. Предусловием операции является корректная типизация входных параметров. Вспомогательная семантическая функция Е сопоставляет типу моделирующее его в AMN множество. Семантическая функция mSubstitution формирует представление предикативных спецификаций канонической модели обобщенными подстановками (преобразователями предикатов, служащих для моделирования поведения) AMN. В разделе 3.5 рассмотрено действие функции mSubstitution на формулах канонической модели, в разделе 3.6 - на правилах.

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

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

аксиоматической семантики. Метод демонстрируется на примере доказательства корректности алгоритмов отображения 0 ядра канонической модели в АМГ4.

В разделе 4.1 описаны общие принципы доказательства. Корректность © заключается в следующем. Спецификация модуля канонической модели, как и набор абстрактных машин АММ, задает некоторую систему, представляющую собой множество значений АТД, объединенных в коллекции. Система характеризуется состоянием и поведением. Состояние системы задается значениями атрибутов состояния объектов, входящими в данный момент в систему, а также составом коллекций. Поведение системы задается методами значений, входящих в систему. Методы могут изменять состояние системы. Спецификация модуля канонической модели, как и набор абстрактных машин АМК, задает множество допустимых состояний системы, а также способы изменения состояния системы (методы значений). © корректно, если для любой М - спецификации модуля канонической модели - существует инъективное отображение в задаваемого ею множества состояний системы, в множество состояний системы, задаваемого Мд = в(М) - набором абстрактных машин АМЫ, и все методы сохраняют свое действие при отображении 0: если метод т переводит систему, задаваемую М, из состояния «1 в «2, то метод ©(т) переводит систему, задаваемую Мв, из состояния б^) в 0(зг)-Это означает, что системы, задаваемые М и Мв, будут вести себя одинаково.

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

Доказательство корректности © состоит из следующих этапов.

• построение инъективного отображения в из пространства § состояний системы, задаваемой спецификацией модуля канонической модели М, в пространство §в состояний системы, задаваемой набором абстрактных машин Мв = ©(М);

• проверка корректности отображения ограничений на пространство состояний;

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

Заметим, что отображение 9 можно естественным образом распространить на формулы. Обозначим #/(•) отображение, определенное на формулах над пространством 8. Терм 9{{ф) получается из формулы ф применением

отображения в ко всем термам, входящим в ф. Таким образом, формула фактически переносится из пространства состояний 8 в пространство Бд.

Корректность отображения ограничений на пространство состояний заключается в следующем. Пусть К = {Фи---,Фп} теория, задающая выделение множества состояний спецификации модуля канонической модели М. Пусть Кд = {ф\,..., фт} теория, задающая выделение множества состояний набора абстрактных машин Мд. Отображение ограничения корректно, если конъюнкции ф\ Л ... Л фт и 9{(ф\) Л ... Л 9/{фп) эквивалентны.

Корректность отображения спецификаций методов поясняется следующей коммутативной диаграммой:

оеМ Л м2э©(о)

яо % 9]($о) 50(о)

Предикативная спецификация метода т модуля М канонической модели отображается в обобщенную подстановку операции ©(т) некоторой абстрактной машины из набора Мв отображением в, семантическая функция канонической модели отображает т в предикат вт € F над пространством состояний В. По предикату зт строится предикат в/(зтп) над пространством состояний Семантическая функция АКШ отображает 0(тп) в вв(т) € Корректность отображения тп заключается в эквивалентности формул, задающих предикаты 0/(бтл) и зв(т).

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

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

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

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

В разделе 5.1 представлено инструментальное средство автоматического отображения спецификаций канонической модели в AMN, реализующее алгоритмы, определенные в третьей главе диссертационной работы, Описан графический интерфейс инструментального средства и сценарий работы эксперта-конструктора ИС с инструментальным средством. Сценарий применим для доказательства уточнения при решении задач над неоднородными источниками информации. Инструментальное средство реализовано на языке Java 2 в среде Windows [9] и встроено в прототипы средств композиционного проектирования и интеграции информационных источников, разработанные в лаборатории композиционных методов проектирования ИС ИПИ РАН.

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

• построить отображение М, в Е,\

• отобразить Е, в AMN;

• построить AMN-семантику для М,;

• применить В-технологию для доказательства того, что Мх уточняет Е,.

В качестве примера рассмотрено расширение канонической модели на основе типа связи (relationship) языка ODL стандарта ODMG.

Тип связи при этом представляет собой единственный элемент исходной модели. Для типа связи построено его отображение в каноническую модель, AMN-семантика. Образ типа связи в канонической модели при помощи инструментального средства автоматически отображен в AMN. Полученные AMN-спецификации (их полный текст приведен в приложении) были введены в инструментальное средство автоматизации доказательства уточнения AMN (B-Toolkit 5.1.4).

Далее при помощи B-Toolkit автоматически были сформулированы тео ремы, в совокупности утверждающие факт уточнения типом связи своего образа в канонической модели. Часть теорем была доказана с использованием

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

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

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

• разрешение конфликтов между спецификациями требований и компонентов;

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

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

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

В качестве примера приведены результаты первых четырех этапов композиционного проектирования части системы Исследовательский фонд, и подробно описан последний этап проектирования. Рассмотрены спецификации системы Исследовательский фонд в канонической модели (спецификации требований), а также спецификации компонентов, онтологически релевантные спецификациям требований. Данные спецификации при помощи инструментального средства были отображены в А\ДО (полный текст полученных АМЫ-спецификаций приведен в приложении) и введены в инструментальное средство автоматизации доказательства уточнения АМ№ Далее автоматически были сформулированы и затем автоматически или интерактивно доказаны теоремы уточнения.

Заключение

Основные результаты работы сводятся к следующему:

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

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

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

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

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

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

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

2. Briukhov D.O., Kalinichenko L.A., Stupnikov S.A. Compositional approach for heterogeneous sources registration at a subject mediator // Emerging Database Research in Eastern Europe: Proceedings of the Pre-Conference Workshop of VLDB 2003. Cottbus: Brandenburg University of Technology, 2003. - P. 5-12. C.A. Ступникову в статье принадлежит формальное обоснование регистрации неоднородных источников в предметном посреднике.

3. Kalinichenko L.A., Martynov D.O., Stupnikov S.A. Query rewriting using views in a typed mediator environment // Advances in Databases and Information Systems: Proc. of the East European Conférence. - Springer-Verlag, 2004. P. 3753. Ступникову С. A. в статье принадлежит формальная семантика правил языка СИНТЕЗ.

4. Ступников С.А., Калиниченко JT.A. Формальная семантика канонической информационной модели в композиционной инфраструктуре распределенных информационных систем. Проблемы и методы информатики. II Научная сессия ИПИ РАН: Тезисы докладов / Под ред. И.А. Соколова. - М.: ИПИ РАН, 2005. - С. 151-153. С.А. Ступниковым разработана формальная семантика канонической информационной модели.

5. Ступников С.А. Формальная семантика ядра канонической объектной информационной модели // Системы и средства информатики: Спец. вып. Формальные методы и модели в композиционных инфраструктурах распределенных информационных систем / Под ред. И. А. Соколова. — М.: ИПИ РАН, 2005. - С. 40-68.

6. Ступников С.А. Отображение спецификаций, выраженных средствами ядра канонической модели, в язык AMN // Системы и средства информатики: Спец. вып. Формальные методы и модели в композиционных инфраструктурах распределенных информационных систем / Под ред. И. А. Соколова. —

7. Ступников С.А. Автоматизация верификации уточнения при композиционном проектировании информационных систем и посредников // Системы и средства информатики: Спец. вып. Формальные методы и модели в композиционных инфраструктурах распределенных информационных систем / Под ред. И. А. Соколова. - М.: ИПИ РАН, 2005. - С. 96-119.

8. Ступников С.А., Брюхов Д.О. Представление иМЬ и ОСЬ в канонической информационной модели // Системы и средства информатики: Спец. вып. Формальные методы и модели в композиционных инфраструктурах распределенных информационных систем / Под ред. И. А. Соколова. — М.: ИПИ РАН, 2005. - С. 120-129. С.А. Ступниковым разработано представление языка ОСЬ в канонической модели.

9. Программа автоматического отображения спецификаций канонической информационной модели в Нотацию Абстрактных Машин: Свидетельство об официальной регистрации программы для ЭВМ N 2005611080 / С.А. Ступников. Зарегистрировано в Реестре программ для ЭВМ 05.05.2005.

М.: ИПИ РАН, 2005. - С. 69-95.

Принято к исполнению 14/12/2005 Исполнено 15/12/2005

Заказ № 1379 Тираж. 100 экз.

ООО «11-й ФОРМАТ» ИНН 7726330900 Москва, Варшавское ш , 36 (095) 975-78-56 (095) 747-64-70 www.autoreferat.ru

CIOOS А

Ц7 .57.

Введение

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, нашедшие применение в качестве составной части инструментария эксперта-конструктора, реализующего композиционное проектирование ИС, и прототипа средств поддержки предметных посредников;

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

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.