WWW.KONF.X-PDF.RU
БЕСПЛАТНАЯ ЭЛЕКТРОННАЯ БИБЛИОТЕКА - Авторефераты, диссертации, конференции
 

Pages:   || 2 | 3 | 4 | 5 |   ...   | 6 |

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

-- [ Страница 1 ] --

Российская Академия Наук

Институт Проблем Информатики

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

УДК 004.415.2+004.415.52+004.423.4

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

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

спецификаций

Диссертация

на соискание учной степени

е

кандидата технических наук

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

Научные руководители

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

Л. А. Калиниченко



доктор технических наук, профессор

В. А. Сухомлин

Москва 2006

Оглавление

Введение

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

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

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

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

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

1.5 Выводы по главе......................... 37 2 Формальное определение ядра канонической информационной модели

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

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

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

2.4 Cемантические функции формирования ограничений на пространство состояний..................... 52 2.4.1 Ограничение типизации экземпляров классов..... 52 2.4.2 Ограничения, налагаемые отношением тип-подтип.. 54 2.4.3 Ограничения, налагаемые отношением класс-подкласс 55 2.4.4 Ограничения, налагаемые инвариантами....... 56

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

2.6 Семантические функции преобразования правил канонической модели в формулы над пространством состояний 60 2.6.1 Семантика конъюнкции коллекций с условием.... 62 2.6.2 Семантика объединения коллекций........... 68

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

–  –  –

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

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

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

–  –  –

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

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

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

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

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

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





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

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

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

В контексте методов верификации систем формализуется одно из наиболее важных понятий в области формальных методов – понятие уточнения [1, 12, 13, 14]. В настоящей работе уточнение понимается следующим образом: система B уточняет систему A, если пользователь может использовать систему B вместо системы A, не замечая факта замены A на B.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Основная идея композиционного проектирования состоит в том, чтобы построить корректную композицию спецификаций существующих компонентов (информационных, программных), уточняющую спецификацию требований к разрабатываемой ИС [18]. При этом спецификации требований и существующих компонентов представляются в канонической модели.

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

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

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

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

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

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

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

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

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

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

Abstract

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

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

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

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

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

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

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

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

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

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

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

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

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

Загрузка...

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

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

М.В. Ломоносова (Москва, 2002), на Международном симпозиуме по базам данных конференции VLDB (Берлин 2003), на II научной сессии ИПИ РАН (Москва, 2005), на научных семинарах лаборатории Композиционных методов проектирования информационных систем Института проблем информатики РАН.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

В приложении A содержится конкретный синтаксис ядра канонической модели.

В приложении B приводится краткое описание языка AMN.

В приложении C рассматривается представление основных элементов UML и OCL в канонической модели.

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

16

–  –  –

1.1. Каноническая информационная модель В настоящий период развития информационных технологий (ИТ) активно создаются разнообразные модели представления информации. Это развитие происходит как в рамках конкретных распределенных инфраструктур (таких как архитектуры OMG, в частности, архитектуры, движимые моделями представления информации (MDA)), архитектуры семантического Веб и Веб-сервисов, архитектуры электронных библиотек как коллективных хранилищ информации в различных предметных областях, архитектуры информационных грид), так и в стандартах языков и моделей данных (таких как, например, ODMG, SQL, UML, стеки XML и RDF моделей данных), процессных моделей и моделей потоков работ, семантических моделей (включая онтологические модели и модели метаданных), моделей цифровых репозиториев данных и знаний в конкретных областях науки (например, виртуальные обсерватории в астрономии).

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

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

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

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

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

Каноническая модель содержит унифицированную систему типов, включающую универсальный конструктор типов (Абстрактный Тип Данных, АТД), а также представительный набор встроенных типов. Описание абстрактного типа данных инкапсулирует спецификации атрибутов, методов и инвариантов типа. Методы и инварианты типов описываются встроенным типом функции. По умолчанию АТД считается объектным – экземпляры такого типа (объекты) имеют встроенный атрибут self, значением которого является уникальный идентификатор, остающийся неизменным в течении всего времени жизни объекта. При модификации объекты сохраняют идентифицируемость. АТД также может быть объявлен необъектным:

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

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

Для решения задач композиционного проектирования было разработано исчисление спецификаций типов [34]. На основе частично упорядоченного отношением тип-подтип множества спецификаций типов определена решетка типов. Операциями решетки типов являются соединение (join) и пересечение (meet) типов. Неформально, соединение T1 T2 спецификаций типов T1 и T2 включает всю информацию, содержащуюся в спецификациях T1 и T2 ; пересечение T1 T2 включает лишь общую информацию из спецификаций T1 и T2.

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

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

В течении последних лет в лаборатории композиционных методов проектирования ИС ИПИ РАН проводились интенсивные исследования по разработке методов решения задач над неоднородными информационными источниками, таких как композиционное проектирование ИС [18, 34, 35], регистрация источников в предметных посредниках [17, 36], интеграция моделей источников [30, 32, 33], переписывание запросов в среде посредников [42]. В процессе этих исследований постоянно проявлялась необходимость формального определения канонической объектной информационной модели (при использовании языка СИНТЕЗ в качестве ее ядра) при манипулировании разнообразными информационными моделями – задания ее (канонической модели) формальной семантики.

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

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

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

Именно на такую унификацию направлены разработанные в данной работе формализованные информационные модели. UML и его отображения ориентированы главным образом на проектирование ИС "сверху-вниз". Вместе с тем, ввиду широкого распространения UML, он полезно использовался при композиционном проектировании ИС на этапах планирования и анализа [18, 36, 35], а также при интеграции информационных источников [17] следующим образом (см. рис. 1.1).

Рис. 1.1. Схема композиционного подхода к проектированию ИС Подход включает в себя прямую и обратную фазы. При прямой фазе (левая часть рисунка) происходит описание спецификаций требований к проектируемой ИС (или разработка схемы предметного посредника). ИС (предметный посредник) разрабатываются в рамках определенной прикладной области, которая задает прикладную семантику для спецификации требований. Этапы планирования требований и анализа реализуются с помощью произвольного метода объектного анализа и проектирования (ОАП), использующего язык UML [38]. Выбранный метод ОАП расширяется онтологическими спецификациями, и другими понятиями канонической модели. При обратной фазе (правая часть рисунка) происходит описание спецификаций компонентов (информационных источников).

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

Общность канонической модели демонстрируется в приложении C на примере поглощения ядром канонической модели представительных подмножеств языков UML и OCL.

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

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

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

1.2. Денотационная и аксиоматическая семантики как способ формального определения информационных моделей Одними из самых широкоиспользуемых методов формального определения языков спецификаций (в том числе объектных моделей и языков запросов, обладающих сходными с канонической моделью чертами), являются методы денотационной и аксиоматической семантик [43, 44, 45, 46, 47].

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

С конца девяностых годов прошлого века ведутся активные исследования по формальному определению языка визуализации, спецификации, проектирования и документирования ИС, разработанного концерном OMG, – языка Unied Modeling Language (UML) [38], а также языка Object Constraint Language (OCL) [48], предназначенного для спецификации дополнительных требований, которые невозможно или сложно выразить графическими средствами языка UML. Во всех этих работах в той или иной степени применяются методы денотационной и аксиоматической семантик:

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

В работах France [49, 50] в качестве семантики языка UML рассматривается формальный язык Z [2]. Основное внимание уделено интерпретации в языке Z диаграмм классов UML. Понятие уникальной идентифицируемости объекта (object identity) в предложенном подходе формализуется при помощи предопределенных множеств объектных идентификаторов, заданных для каждого UML-класса. Разделяются понятия интенсионала класса как набора свойств, общих для всех объектов класса и экстенсионала класса как множества объектов класса. Для экстенсионала и интенсионала вводятся различные схемы языка Z. Интенсиональная схема описывает класс в терминах его атрибутов, типы атрибутов интерпретируются как предопределенные множества. Экстенсиональная схема содержит переменную, интерпретирующую множество экземпляров класса, а также функцию, ставящую в соответствие объектам их атрибуты. Отношение обобщения-специализации интерпретируется введением собственных интенсиональной и экстенсиональной схем для подкласса. Интенсиональной схема подкласса расширяющей интенсиональную схему суперкласса, а экстенсиональная схема подкласса содержит определение экстенсионала подкласса и необходимые ограничения, задающие иерархию. При помощи отдельной схемы отражаются свойства непересечения экстенсионалов классов. Ассоциации между классами определяются при помощи отдельных схем, включающих экстенсиональные схемы ассоциированных классов, кардинальность ассоциаций выражается специальными предикатами.

Состояние системы в целом выражается схемой, включающей схему иерархии и схемы ассоциаций.

Работы Kim, Carrington [51, 52] посвящены определению семантики диаграмм классов UML в языке Object-Z [3] – объектно-ориентированном расширении Z. Язык Object-Z содержит понятия уникальной идентифицируемости объектов и наследования, что позволяет избавиться от экстенсиональных схем при интерпретации классов UML.

В подходе каждый UML-класс интерпретируется схемой Object-Z. Атрибуты типизируются предопределенными множествами, ассоциации интерпретируются атрибутами классов. Факт участия объекта класса в ассоциации в некоторой роли выражается при помощи предиката с квантором всеобщности. Отношение обобщения-специализации интерпретируется при помощи наследования схем Object-Z, а также специальными предикатами, указывающими на полиморфизм объектов суперклассов. Схема, выражающая состояние системы в целом, для каждого Object-Z-класса содержит множество, типизированное как множество экземпляров данного класса. Для класса, являющегося суперклассом, указывается полиморфизм объектов соответствующего множества. Схема системы включает также предикаты, утверждающие существование объектов, доступных по ассоциативной ссылке, и предикаты вхождения подкласса в суперкласс как подмножества.

Логическим продолжением данных работ является результат Roe, Broda, Russo [53] по представлению семантики подмножества OCL в ObjectZ. Операции UML интерпретируются как отдельные операционные схемы, параметры операций интерпретируются как входные и выходные коммуникационные переменные схем. Инварианты OCL представляются либо как предикаты в схемах классов, либо как предикаты в схеме системы. Пред и постусловия операций UML представляются предикатами соответствующих операционных схем. В работе рассмотрено также инструментальное средство автоматического отображения диаграмм классов UML с наложенными OCL-ограничениями в Object-Z.

Работы Lano, Bicarregui [54, 55, 56] посвящены формальному определению языка UML в языке RAL (Real-time Action Logic) [57]. Спецификации RAL представляют собой структурированные теории, основанные на логике первого порядка и включающие средства описания временных свойств систем. Описана семантика конструкций UML, составляющих диаграммы классов, состояний, диаграммы последовательностей действий, активностей: классов, ассоциаций, атрибутов, операций, отношения обобщения, сообщений. Каждый UML-класс C представляется отдельной теорией C, содержащей одноименный предопределенный тип – множество всевозможных объектов класса. Множество существующих объектов класса представляется переменной C теории C, типизированной как конечное подмножество элементов типа C. Множество переменных теории включает также переменную self, отражающую уникальную идентифицируемость объектов и переменные, соответствующие атрибутам UML-класса. Атрибутные переменные типизированы как функции из множества C в множество, представляющее тип атрибута. Ассоциации представляются переменными, типизированными как элементы декартова произведения типов, представляющих ассоциированные классы. Факт существования объектов, входящих в ассоциации, интерпретируется соответствующими аксиомами.

Специальными аксиомами представляются свойства ассоциаций, такие как кардинальность. Обобщение UML-классом T UML-класса S интерпретируется аксиомами S T S T : тип S теории S является подтипом типа T теории S, множество S является подмножеством T. Операции UML представляются действиями (actions) соответствующих теорий RAL. В работе [55] определено также представление в RAL подмножества языка OCL.

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

Семантика подмножества языка OCL в логике первого порядка рассмотрена в работах Beckert, Schmitt [58, 59]. Ограничения в терминах OCL, налагаемые на диаграмму классов UML D, представляются как теории логики первого порядка ThD над специальной сигнатурой D. Описаны правила построения сигнатуры D по элементам диаграммы: используемым встроенным типам, классам, ассоциациям, атрибутам, операциям. Определены общие принципы построения формул теории ThD по диаграмме D. Наибольшее внимание уделено представлению в виде логических термов операций над коллекциями. Предложен также альтернативный способ представления типов коллекций в виде предикатов, сокращающий количество используемых в логической теории функциональных символов и аксиом.

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

Результаты Riedel, Scholl [60, 61] посвящены определению денотационной семантики языка CROQUE, основанного на ODMG-стандарте языка OQL. Разработана система типов и правила типизации выражений языка запросов. Семантика конструкций языка выражена в виде правил – предикатов, определяющих, содержится ли некоторое значение в результирующем множестве запроса.

В работах Cherniak [62, 63] по определению семантики языка OQL семантические соотношения представляют собой выражения в языке комбинаторов KOLA [63]. В подходе используется понятие окружения – нумерованного списка переменных, используемых в теле запроса и их текущих значений.

Дальнейшим продвижением в области формального определения языков SQL и OQL является работа Brown [64]. Для языков определены синтаксические и семантические домены, правила типизации выражений. Определены также семантические функции, задающие правила формирования результирующего множества запроса. Семантические функции, помимо параметров из синтаксических доменов, могут иметь параметр окружение (список используемых переменных и их значений) и параметр состояние базы данных. Объектная база данных в данном подходе состоит из коллекций, являющихся множествами объектов. Объект представляет собой уникально идентифицируемую сущность (entity), сущность – функцию из множества сообщений в множество сложных значений.

Цель определения формальной семантики информационных моделей авторы упомянутых подходов определяют как создание базы для дальнейшего формального анализа проектируемых систем. В подходе Lano, Bicarregui [54, 55, 56] в частности, описывается методика применения формальной семантики UML для доказательства корректности использования образцов проектирования (design patterns) при проектировании ИС. Авторы подходов также указывают, что разработанная семантика является формализацией той семантики, которая неформально описана в стандартах информационных моделей. Формальная семантика может служить также для выявления противоречий в стандартах информационных моделей.

Подход к формальному определению ядра канонической модели, рассматриваемый в главе 2 настоящей работы, заключается в сообщении канонической модели комбинированной денотационно-аксиоматической семантики. В качестве языка определения формальной семантики используется теория множеств и логика предикатов первого порядка. Такой подход к семантике является более общим, чем выражение семантики в какой-либо конкретной модели, такой, например, как Z, Object-Z, RAL или VDM [4].

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

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

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

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

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

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

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



Pages:   || 2 | 3 | 4 | 5 |   ...   | 6 |
Похожие работы:

«АКСЕНОВ Алексей Юрьевич МОДЕЛИ И МЕТОДЫ ОБРАБОТКИ И ПРЕДСТАВЛЕНИЯ СЛОЖНЫХ ПРОСТРАНСТВЕННЫХ ОБЪЕКТОВ Специальность 05.13.01 – Системный анализ, управление и обработка информации (технические системы) Диссертация на соискание ученой степени кандидата технических наук Научный руководитель: доктор технических наук, Кулешов С.В....»

«Рафикова Юлия Юрьевна ГЕОИНФОРМАЦИОННОЕ КАРТОГРАФИРОВАНИЕ РЕСУРСОВ ВОЗОБНОВЛЯЕМЫХ ИСТОЧНИКОВ ЭНЕРГИИ (на примере Юга России) Диссертация на соискание ученой степени кандидата географических наук Специальность 25.00.33 «Картография» Научный руководитель Доктор географических наук, профессор Б.А. Новаковский Москва 201 Содержание Введение.. Глава 1....»

«ВОЙТКО ДМИТРИЙ АЛЕКСЕЕВИЧ КОМПЛЕКСНЫЙ ПОДХОД К СОВЕРШЕНСТВОВАНИЮ ОРГАНИЗАЦИИ ЛЕЧЕБНО-ДИАГНОСТИЧЕСКОЙ ПОМОЩИ ПРИ РАКЕ ПРЕДСТАТЕЛЬНОЙ ЖЕЛЕЗЫ 14.02.03 Общественное здоровье и здравоохранение Диссертация на соискание ученой степени кандидата медицинских наук НАУЧНЫЕ РУКОВОДИТЕЛИ: доктор...»

«ФИРСОВА Екатерина Валериевна ОБУЧЕНИЕ ДИСКРЕТНОЙ МАТЕМАТИКЕ СТУДЕНТОВ ВУЗА С ИСПОЛЬЗОВАНИЕМ ДИСТАНЦИОННЫХ ОБРАЗОВАТЕЛЬНЫХ ТЕХНОЛОГИЙ (на примере специальности/профиля «прикладная информатика (в экономике)») 13.00.02 – теория и методика обучения и воспитания (математика) ДИССЕРТАЦИЯ на соискание ученой степени...»

«ЕРУСАЛИМСКИЙ ЯКОВ МИХАЙЛОВИЧ РАЗРАБОТКА И ИССЛЕДОВАНИЕ МЕТОДОВ РЕШЕНИЯ ЭКСТРЕМАЛЬНЫХ ЗАДАЧ НА ОРИЕНТИРОВАННЫХ ГРАФАХ И СЕТЯХ С ОГРАНИЧЕНИЯМИ НА ДОСТИЖИМОСТЬ Специальность: 05.13.17 – теоретические основы информатики диссертация на соискание ученой степени доктора технических наук Ростов-на-Дону, 2015 ОГЛАВЛЕНИЕ ВВЕДЕНИЕ....»

«ЛЯШ Ася Анатольевна МЕТОДИКА ОБУЧЕНИЯ БУДУЩИХ УЧИТЕЛЕЙ ИНФОРМАТИКИ ИСПОЛЬЗОВАНИЮ ИНФОРМАЦИОННО-ОБРАЗОВАТЕЛЬНЫХ СИСТЕМ В ПРОФЕССИОНАЛЬНОЙ ДЕЯТЕЛЬНОСТИ Специальность 13.00.02 – теория и методика обучения и воспитания (информатика) Диссертация на соискание ученой степени кандидата педагогических наук Научный руководитель: доктор педагогических...»

«Орлов Юрий Львович ПОЛНОГЕНОМНЫЙ КОМПЬЮТЕРНЫЙ АНАЛИЗ РАСПРЕДЕЛЕНИЯ САЙТОВ СВЯЗЫВАНИЯ ТРАНСКРИПЦИОННЫХ ФАКТОРОВ ЭУКАРИОТ ПО ДАННЫМ ИММУНОПРЕЦИПИТАЦИИ ХРОМАТИНА И ВЫСОКОПРОИЗВОДИТЕЛЬНОГО СЕКВЕНИРОВАНИЯ 03.01.09 – математическая биология, биоинформатика Диссертация на соискание ученой степени доктора биологических наук Научный консультант: академик...»

«Зайцев Владислав Вячеславович РАЗРАБОТКА И ИССЛЕДОВАНИЕ МЕТОДИКИ ПРОЕКТИРОВАНИЯ БАЗЫ МЕТАДАННЫХ ХРАНИЛИЩА ГЕОДАННЫХ Специальность 25.00.35 – «Геоинформатика» ДИССЕРТАЦИЯ на соискание ученой степени кандидата технических наук Научный руководитель д-р техн. наук, проф. А.А. Майоров Москва 2015   ОГЛАВЛЕНИЕ...»

«ЭРКЕНОВА ЛАУРА ЗАГИДИЕВНА ОРГАНИЗАЦИОННО-ЭКОНОМИЧЕСКИЕ АСПЕКТЫ УПРАВЛЕНИЕ УСТОЙЧИВЫМ РАЗВИТИЕМ РЕГИОНА (на примере Кабардино-Балкарской Республики) Специальность 08.00.05 – Экономика и управление народным хозяйством (региональная экономика) Диссертация на соискание ученой степени кандидата экономических наук Научный руководитель: доктор экономических наук...»

«ВАЙСМАН ДАВИД ШУНЕВИЧ СОВЕРШЕНСТВОВАНИЕ СИСТЕМЫ ИНФОРМАЦИОННОГО ОБЕСПЕЧЕНИЯ ОЦЕНКИ И АНАЛИЗА СМЕРТНОСТИ НАСЕЛЕНИЯ НА УРОВНЕ СУБЪЕКТА РОССИЙСКОЙ ФЕДЕРАЦИИ 14.02.03 – Общественное здоровье и здравоохранение Диссертация на соискание ученой степени доктора медицинских наук Научный консультант: доктор медицинских наук, профессор И.М....»

«РОЩИН ДЕНИС ОЛЕГОВИЧ ПОТЕРИ ОТ САХАРНОГО ДИАБЕТА И ПУТИ РЕШЕНИЯ ПРОБЛЕМЫ ИХ ОЦЕНКИ 14.02.03 – общественное здоровье и здравоохранение Диссертация на соискание ученой степени кандидата медицинских наук Научный руководитель: доктор медицинских наук, профессор Т.П. Сабгайда Москва – 2015...»

«МИНИСТЕРСТВО ЗДРАВООХРАНЕНИЯ РОССИЙСКОЙ ФЕДЕРАЦИИ ФГБУ «ЦЕНТРАЛЬНЫЙ НАУЧНО-ИССЛЕДОВАТЕЛЬСКИЙ ИНСТИТУТ ОРГАНИЗАЦИИ И ИНФОРМАТИЗАЦИИ ЗДРАВООХРАНЕНИЯ» _ СТЕРЛИКОВ СЕРГЕЙ АЛЕКСАНДРОВИЧ ОПТИМИЗАЦИЯ СИСТЕМЫ ОКАЗАНИЯ ПРОТИВОТУБЕРКУЛЕЗНОЙ ПОМОЩИ НАСЕЛЕНИЮ РОССИЙСКОЙ ФЕДЕРАЦИИ 14.02.03 – Общественное здоровье и здравоохранение Диссертация на соискание ученой степени доктора медицинских наук Научный консультант: доктор медицинских наук, профессор Нечаева Ольга Брониславовна Москва,...»

«АФАНАСОВА Елена Пантелеевна ПРОГНОЗИРОВАНИЕ РАЗВИТИЯ И ИСХОДОВ, РАЗРАБОТКА СЕТЕВЫХ И МАТЕМАТИЧЕСКИХ МОДЕЛЕЙ ДЛЯ СОВЕРШЕНСТВОВАНИЯ ДИАГНОСТИКИ И АНАЛИЗА ТЕРАПИИ ОСТРОГО ЭНДОМЕТРИТА 03.01.09 – Математическая биология, биоинформатика (медицинские науки) Диссертация на соискание ученой степени доктора медицинских наук Научный консультант: доктор медицинских наук, профессор Агарков Николай Михайлович Курск – 2014 ОГЛАВЛЕНИЕ Стр....»

«Егоров Алексей Юрьевич ФОРМИРОВАНИЕ И РАЗВИТИЕ РЫНКА ОРГАНИЧЕСКОЙ АГРОПРОДОВОЛЬСТВЕННОЙ ПРОДУКЦИИ (НА ПРИМЕРЕ ЦФО) Специальность 08.00.05 Экономика и управление народным хозяйством (экономика, организация и управление предприятиями, отраслями, комплексами – АПК и сельское хозяйство) ДИССЕРТАЦИЯ на соискание ученой степени кандидата экономических наук...»

«Биричевский Алексей Романович Аппаратно-программные методы защиты информации в мобильных устройствах телекоммуникационных и информационных систем Специальность 05.13.19 – Методы и системы защиты информации, информационная безопасность Диссертация на соискание ученой степени Кандидата технических наук Научный руководитель д.т.н,...»

«Родионова Татьяна Васильевна Исследование динамики термокарстовых озер в различных районах криолитозоны России по космическим снимкам Диссертация на соискание ученой степени кандидата географических наук по специальности 25.00.33 картография Научный руководитель: в. н. с., д. г. н. Кравцова В. И. Москва 2013 Оглавление Введение...3 1. Термокарстовые озера...»

«УДК 316.32 АБДУЛЛАЕВ Ильхом Заирович «ИНФОРМАТИЗАЦИЯ ОБЩЕСТВЕННО-ПОЛИТИЧЕСКОЙ ЖИЗНИ В УСЛОВИЯХ ГЛОБАЛИЗАЦИИ РАЗВИТИЯ» Специальность – 23.00.04 – Политические проблемы мировых систем и глобального развития Диссертация на соискание ученой степени доктора политических наук Ташкент – 2007 ОГЛАВЛЕНИЕ с. 3 – 15 ВВЕДЕНИЕ Глава 1. Понятийно-категориальные основы теории информационного...»

«Шаталов Павел Сергеевич СИСТЕМА ПОДДЕРЖКИ ПРИНЯТИЯ РЕШЕНИЙ ПО УПРАВЛЕНИЮ ПРИРОДНЫМИ ПОЖАРАМИ С ИСПОЛЬЗОВАНИЕМ ВЫСОКОПРОИЗВОДИТЕЛЬНЫХ ВЫЧИСЛИТЕЛЬНЫХ СИСТЕМ И ДАННЫХ КОСМИЧЕСКОГО МОНИТОРИНГА 05.13.01 Системный анализ, управление и обработка информации (информатика, вычислительная техника, управление) Диссертация на соискание ученой степени...»

«Андреева Надежда Михайловна МЕТОДИКА ИСПОЛЬЗОВАНИЯ ДОРОЖНЫХ КАРТ ПРИ ЭЛЕКТРОННОМ ОБУЧЕНИИ СТУДЕНТОВ ИНФОРМАТИКЕ (на примере экономических и биологических направлений подготовки) 13.00.02 – Теория и методика обучения и воспитания (информатика, уровень профессионального образования) ДИССЕРТАЦИЯ на соискание учёной степени кандидата...»

«ЗУДОВ АНТОН БОРИСОВИЧ МОДЕЛЬНЫЕ ПРЕДСТАВЛЕНИЯ И АЛГОРИТМЫ ПРОВЕРКИ ПРАВИЛ В АКТИВНЫХ БАЗАХ ДАННЫХ Специальность: 05.13.17 – Теоретические основы информатики Диссертация на соискание ученой степени кандидата технических наук Научный руководитель: доктор технических наук профессор Макарычев П.П. ПЕНЗА 2015 СОДЕРЖАНИЕ Введение 1 АНАЛИЗ МОДЕЛЕЙ, МЕТОДОВ И СРЕДСТВ ПОСТРОЕНИЯ АКТИВНЫХ БАЗ ДАННЫХ 1.1 Анализ современных технологий обработки...»









 
2016 www.konf.x-pdf.ru - «Бесплатная электронная библиотека - Авторефераты, диссертации, конференции»

Материалы этого сайта размещены для ознакомления, все права принадлежат их авторам.
Если Вы не согласны с тем, что Ваш материал размещён на этом сайте, пожалуйста, напишите нам, мы в течении 1-2 рабочих дней удалим его.