авторефераты диссертаций БЕСПЛАТНАЯ БИБЛИОТЕКА РОССИИ

КОНФЕРЕНЦИИ, КНИГИ, ПОСОБИЯ, НАУЧНЫЕ ИЗДАНИЯ

<< ГЛАВНАЯ
АГРОИНЖЕНЕРИЯ
АСТРОНОМИЯ
БЕЗОПАСНОСТЬ
БИОЛОГИЯ
ЗЕМЛЯ
ИНФОРМАТИКА
ИСКУССТВОВЕДЕНИЕ
ИСТОРИЯ
КУЛЬТУРОЛОГИЯ
МАШИНОСТРОЕНИЕ
МЕДИЦИНА
МЕТАЛЛУРГИЯ
МЕХАНИКА
ПЕДАГОГИКА
ПОЛИТИКА
ПРИБОРОСТРОЕНИЕ
ПРОДОВОЛЬСТВИЕ
ПСИХОЛОГИЯ
РАДИОТЕХНИКА
СЕЛЬСКОЕ ХОЗЯЙСТВО
СОЦИОЛОГИЯ
СТРОИТЕЛЬСТВО
ТЕХНИЧЕСКИЕ НАУКИ
ТРАНСПОРТ
ФАРМАЦЕВТИКА
ФИЗИКА
ФИЗИОЛОГИЯ
ФИЛОЛОГИЯ
ФИЛОСОФИЯ
ХИМИЯ
ЭКОНОМИКА
ЭЛЕКТРОТЕХНИКА
ЭНЕРГЕТИКА
ЮРИСПРУДЕНЦИЯ
ЯЗЫКОЗНАНИЕ
РАЗНОЕ
КОНТАКТЫ


Pages:     | 1 |   ...   | 7 | 8 || 10 | 11 |   ...   | 26 |

«Электронные библиотеки: Перспективные Методы и Технологии, Электронные коллекции English Труды RCDL 2010 ...»

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

ражается в OWL при помощи комбинации конст- Условия для свойств объектов. Когда класс (em рукций SubPropertyOf и ObjectPropertyChain. ployee) связывается со своим типом экземпляров СИНТЕЗ OWL (Employee), на область определения, область значе all c/City, r/Region, s/Region SubPropertyOf( ния и кардинальность свойств, составляющих тип, ( is_in(city, c) & ObjectPropertyChain( накладываются соответствующие ограничения. В is_in(region, r) & locatedIn partOf ) случае, когда метакласс ассоциаций свойства явля is_in(region, s) & locatedIn ) ется подклассом некоторого специального мета is_in(c.locatedIn, r) & класса (например, метакласс Same Salary свойства is_in(r.partOf, s) - sameSalary является подклассом метакласса is_in(c.locatedIn, s ) reflexive), свойство должно удовлетворять всем ин Отображение ключей. Ключи представляются в вариантам суперкласса (свойство sameSalary долж языке СИНТЕЗ при помощи встроенных утвержде- но быть рефлексивным).

ний уникальности атрибутов (unique). В OWL клю- Конструкция СИНТЕЗ Условие чи представляются при помощи конструкции e, s ( { employee;

in: class;

HasKey. (e, s) (salary)DP instance_section:

СИНТЕЗ OWL Employee;

e (employee)C { Employee;

in: type;

HasKey( employee …} s (integer)DT) empCode: integer;

empCode ) { Employee;

in: type;

e, s1, s2 ( keys: worksOn: {set;

(e, s1) (salary)DP { unique;

{ empCode } };

type_of_element: Project;

};

(e, s2) (salary)DP } metaslot in: WorksOn;

end s1 = s2 ) salary: integer;

4 Интерпретации и модели онтологий } e, p ( { WorksOn;

языка СИНТЕЗ (e, p) (worksOn)OP in: association, metaclass;

e (employee)C В качестве семантических структур, интерпре- instance_section: { s (project)C ) тирующих онтологии языка СИНТЕЗ, будут рас- domain: employee;

смотрены те же структуры, что используются в [7] range: project;

для интерпретации онтологий OWL. Это позволит };

упростить доказательство корректности отображе- } ния языка СИНТЕЗ и OWL. e( { SameSalary;

Так, интерпретация I = I, D, •C, •OP, •DP, •I, •DT, e (employee)C in: association, metaclass;

•LT представляет собой кортеж из следующих ком- superclass: reflexive;

(e, e) (sameSalary)OP) понентов: instance_section: { • I – объектный домен;

domain: employee;

• D – домен типов данных;

range: employee;

• •C – функция интерпретации классов;

для ка- };

} ждого класса Cl выполнено (Cl)C I;

{ Employee;

in: type;

• •OP – функция интерпретации свойств объек sameSalary: {set;

тов, область значения которых – коллекция type_of_element:

объектов;

для каждого свойства op выполнено Employee;

};

(op)OP I I;

metaslot in: SameSalary end • •DP – функция интерпретации свойств объек } тов, область значения которых – множество Условия для фактов. полученную из O добавлением класса A и утвер ждения, что объект с именем ida входит в A:

Конструкция Условие СИНТЕЗ { A;

in: class;

(JohnJohnson)I (employee)C { JohnJohnson;

superclass: C1;

((JohnJohnson)I, (3200)LT) in: employee;

instance_section: { salary: 3200;

(salary)DP inv: { in: invariant;

boss: JackJackson;

((JohnJohnson)I, (JackJackson)I) { A = differ(thing, C2) } } (boss)OP };

} Условия для подклассов.

Конструкция СИНТЕЗ Условие { ida;

in: A;

} (manager)C (employee)C { manager;

in: class;

superclass: employee;

Тогда очевидно, что интерпретация I, расширен …} ная утверждением (ida)I = a, является моделью O1, т.е. из отрицания поглощения C1 C2 следует суще Условия для утверждений уникальности.

ствование модели для O1. Следовательно, из отсут СИНТЕЗ OWL ствия модели для O1 следует поглощение C1 C2.

x, y, k ( { Employee;

in: type;

Таким образом, задача поглощения сведена к задаче (x, k) (empCode)DP empCode: integer;

отсутствия модели.

keys: (y, k) (empCode)DP Аналогичным образом для канонической модели { unique;

{ empCode } };

x = y ) адаптируются и другие сводимости.

} 5 Корректность взаимного отображения Условия для инвариантов.

канонической модели и языка OWL Конструкция СИНТЕЗ Условие (manager)C (areaMan manager = Обозначим чрез : SSYNSOWL взаимное отобра ager)C (topManager)C union(areaManager, жение (являющееся формально отношением) мно topManager) жества SSYN схем, выраженных в канонической мо m ( (m)I all m/TopManager ( дели и SOWL – множества онтологий, выраженных в (topManager)C is_in(topManager, m) - языке OWL 2 (примером такого отображения явля is_in(m.boss, m) ) ((m) I, (m) I) (boss)OP ) ется отображение, определенное в разделе 3). Он #{m | (e, m) (boss)OP cardinal({m/Manager | тологии s SSYN и o SOWL отображаются друг в m (topManager)C } is_in(e.boss, m) & друга iff s, o.

is_in(topManager, m)}) Назовем отображение корректным, если для = любых двух онтологий s SSYN и o SOWL таких, h, f ( e.hireDate e.fireDate что s, o следующие условия эквивалентны:

(e, h) (hireDate)DP • существует модель MS для онтологии s;

(e, f) (fireDate)DP • существует модель MO для онтологии o.

hf) Заметим, что корректность отображения озна чает эквивалентность задач вывода в канонической Для доказательства корректности отображения модели и в дескриптивной логике SROIQ [11], отве канонической модели и OWL 2 необходимо также чающей языку OWL 2 DL.

убедиться, что основные задачи вывода (непротиво- Действительно, основные задачи вывода в речивость онтологии, поглощение понятий и т. д.), SROIQ сводимы к задаче существования модели в сводимые друг к другу в дескриптивных логиках, SROIQ [11], существование модели в SROIQ экви сводимы друг к другу и в канонической модели. валентно существованию модели в языке СИНТЕЗ, Действительно, доказательства сводимости для де- а задачи вывода в языке СИНТЕЗ сводимы к задаче скриптивных логик легко преобразуются в доказа- существования модели в языке СИНТЕЗ.

тельства сводимости для канонической модели. В В разделе 4 показано, как онтологии языка качестве примера рассмотрим доказательство сво- СИНТЕЗ интерпретируются при помощи семанти димости задачи поглощения к задаче отсутствия ческих структур, используемых при интерпретации модели (unsatisfiability). языка OWL 2. Таким образом, если рассмотреть для Рассмотрим онтологию O и задачу поглощения онтологий s SSYN и o SOWL, связанных отобра для классов C1 C2 из O. По определению погло- жением, одну и ту же интерпретацию I, то для щения, C1 C2 iff для любой модели I = I, D, •C, доказательства корректности отображения остает •OP, •DP, •I, •DT, •LT онтологии O выполнено (C1)С ся показать лишь, что I удовлетворяет s iff I удовле (C2)С. Рассмотрим задачу отрицания поглощения: творяет o. Для этого нужно показать, что условия пусть существует такая модель I и такой объект a, удовлетворения интерпретации онтологии канони что a (C1)С и a (C2)С. Рассмотрим онтологию O1, ческой модели, рассмотренные в разделе 4, эквива лентны условиям удовлетворения интерпретации Условия для рефлексивных свойств.

онтологии OWL [7]. В общем случае доказательство Условия для СИНТЕЗ Условия для OWL осуществляется индукцией по построению онтоло- e (e (employee)C x ( x I гии (по классам, свойствам, фактам, инвариантам и (e, e) (sameSalary)OP) (x, x) (sameSalary)OP) т. д.). В данном разделе эквивалентность условий продемонстрирована на примерах из раздела 3, ил- Условия для непересекающихся свойств.

люстрирующих основные закономерности доказа- Условия для СИНТЕЗ Условия для OWL тельства. В левой части таблиц приводятся условия e (e (employee) (hireDate)DP (fire C для конструкций СИНТЕЗ, рассмотренных в разде h, f ( Date)DP = ле 3. В правой части таблиц приводятся условия для (e, h) (hireDate) DP соответствующих конструкций OWL, также рас (e, f) (fireDate)DP смотренных в разделе 3. В условиях для OWL со h f )) хранены обозначения, используемые в [7].

Условия для иерархии композиций свойств.

Условия для свойств объектов.

Условия для СИНТЕЗ Условия для OWL Условия для СИНТЕЗ Условия для OWL c, r, s ( с (city)C y0, y1, y2 ( e, s ( x, y ( r (region)C (y0, y1) (locatedIn)OP (e, s) (salary)DP (x, y) (salary)DP s (region) (y1, y2) (partOf)OP C e (employee) x (employee)C ) C (c, r) (locatedIn) (y0, y2) (locatedIn)OP ) OP s (integer) ) x, y ( DT (r, s) (partOf) OP e, s1, s2 ( (x, y) (salary)DP (c, s) (locatedIn)OP ) (e, s1) (salary) y (xsd:integer)DT) DP (e, s2) (salary) (employee)C { x | #{ y | DP Условия для утверждений уникальности.

(x, y) (salary)DP } = 1 } s1 = s2 ) Условия для СИНТЕЗ Условия для OWL x, y, k ( x, у, w ( e, p ( x, y ( (x, k) (empCode)DP x (employee)C (e, p) (worksOn)OP (x, y) (worksOn)OP (y, k) (empCode) y (employee)C DP e (employee)C e (employee)C) (x, k) (empCode)DP x=y) s (project)C ) x, y ( (y, k) (empCode)DP (x, y) (worksOn)OP x = y) s (project)C ) Нетрудно видеть, что конъюнкции условий для Условия для отношений между классами.

СИНТЕЗ и условий для OWL эквивалентны. В про Условия для СИНТЕЗ Условия для OWL стейших случаях условия просто совпадают (на (manager)C (employee)C (manager)C (employee)C пример, отношения между классами) или совпадают с точностью до переменных.

(manager)C (areaMan (manager)C (areaMan- Таким образом, построенное отображение ager)C (topManager)С ager)C (topManager)С корректно и позволяет использовать для решения задач вывода в онтологиях канонической модели Условия для фактов. автоматические системы вывода для дескриптивных Условия для СИНТЕЗ Условия для OWL логик [5].

(JohnJohnson)I (em- (JohnJohnson)I (em- Трансформация, отвечающая отображению под ployee)C ployee)C множества канонической информационной модели ((JohnJohnson)I, (3200)LT) ((JohnJohnson)I, (3200)LT) в язык OWL 2, реализована на языке трансформа (salary)DP (salary)DP ций моделей ATL (ATLAS Transformation Language) ((JohnJohnson)I, (JackJack ((JohnJohnson)I, (Jack- [10]. Трансформация позволяет автоматически по son)I) (boss)OP Jackson)I) (boss)OP рождать онтологию на языке OWL 2 из онтологии, выраженной в канонической информационной мо дели.

Условия для самоограничений.

Условия для СИНТЕЗ Условия для OWL 6 Заключение m ((m)I (topManager)C (topManager)C { x | (x, x) (boss)OP} Важной задачей при создании предметных по ((m), (m) ) (boss) ) I I OP средников для интеграции неоднородных информа Условия для ограничений на размер области и ционных ресурсов является верификация онтологи класс значений свойств. ческого моделирования и интеграции онтологий.

Условия для СИНТЕЗ Условия для OWL Онтологии представляются в предметных посред e ( e (employee)C (employee)C { x | никах в канонической информационной модели, #{m | (e, m) (boss)OP #{ y | (x, y) (boss)OP m (topManager) } 1) у (topManager)C } 1 } C служащей общим языком, унифицирующим разно- soning. – Menlo Park, California: AAAI Press, образные модели ресурсов. 2006. – P. 57-67.

В данной работе представлено взаимное отобра- [12] Брюхов Д.О., Вовченко А. Е., Захаров В.Н., Же жение канонической модели (языка СИНТЕЗ) и он- ленкова О.П., Калиниченко Л.А., Марты тологической модели, служащей входным языком нов Д.О., Скворцов Н.А., Ступников С.А. Архи для автоматических систем вывода в дескриптив- тектура промежуточного слоя предметных по ных логиках – языка OWL 2. Построенное отобра- средников для решения задач над множеством жение позволяет использовать системы вывода для интегрируемых неоднородных распределенных решения задач вывода в онтологиях канонической информационных ресурсов в гибридной грид модели. Тем самым достигается верификация кон- инфраструктуре виртуальных обсерваторий // цептуального моделирования и интеграции онтоло- Информатика и ее применения. – М., 2008. – гий. Т. 2, Вып. 1. – С. 2-34.

[13] Kalinichenko L.A., Stupnikov S.A., Vovchen ko A.E. Mediation based semantic grid // Distrib Литература uted computing and grid technologies in science [1] Kalinichenko L.A., Briukhov D.O., Mar- and education: Proc. of the Int. Conf. – Dubna:

tynov D.O., Skvortsov N.A., Stupnikov S.A. Me- JINR, 2010.

diation framework for enterprise information sys- [14] Wiederhold G. Mediators in the architecture of tem infrastructures // The 9th Int. Conf. on Enter- future information systems // IEEE Computer. – prise Information Systems (ICEIS). – 2007. – P. 1992. – V. 25, No 3. – P. 38-49.

246-251.

[2] Kalinichenko L.A., Stupnikov S.A., Martynov D.O.

A mutual mapping of the canonical SYNTHESIS: a language for canonical information information model and OWL modeling and mediator definition for problem solv ing in heterogeneous information resource envi- S.A. Stupnikov, N.A. Skvortsov ronments. – M.: IPI RAS, 2007. – 171 p.

[3] Briukhov D.O., Kalinichenko L.A., Skvortsov N.A. Main points of a mutual mapping of the canonical in Information sources registration at a subject media- formation model and distinguishing features of OWL tor as compositional development// Advances in language are presented. The mapping allows to use de Databases and Information Systems: Proc. of the scription logic automatic reasoners for inference prob 5th East European Conf. LNCS 2151. – Berlin- lems solving in ontologies of the canonical model. Thus Heidelberg: Springer-Verlag, 2001. – P. 70-83. a verification of subject mediators conceptual modeling [4] Horrocks I., Sattler U., Tobies S. Practical reason- and heterogeneous information resources integration in ing for very expressive description logics // Logic J. mediators are achieved.

of the IGPL. – 2000. – V. 8, No 3. – P. 239-264.

[5] Pellet: OWL 2 reasoner for Java. – http:// clarkpar- Работа выполнена при финансовой поддержке РФФИ sia. com/pellet/. (проекты 08-07-00157, 10-07-00342, 10-07-00640) и Про [6] Patel-Schneider P.F. OWL 2 Web ontology lan- граммы фундаментальных исследований Президиума РАН № 3 «Фундаментальные проблемы системного про guage new features and rationale. – 2009. – http:// граммирования», раздел 4 «Системы управления базами www.w3.org/TR/owl2-new-features/.

данных», проект «Исследование методов и средств про [7] Horrocks I., Parsia B., Sattler U. OWL 2 Web on межуточного слоя предметных посредников, обеспечи tology language direct semantics. – 2009. – вающего решение задач над множеством неоднородных http://www.w3.org/TR/owl2-direct-semantics/. распределенных информационных ресурсов»

[8] Калиниченко Л.А., Скворцов Н.А.. Реверсивное онтологическое моделирование при унифици рованном представлении различных онтологи ческих моделей источников информации в предметном посреднике // Системы и средства информатики: Спец. вып. Формальные методы и модели в композиционных инфраструктурах распределенных информационных систем / Под ред. И.А. Соколова. – М.: ИПИ РАН, 2005. – С. 184-212.

[9] Bock С. et al. OWL 2 Web Ontology Language Structural Specification and Functional-Style Syn tax. – 2009. – http://www.w3.org/TR/2009/REC owl2-syntax-20091027/.

[10] ATL Project. – http://www.eclipse.org/m2m/atl/.

[11] Horrocks I., Kutz O., Sattler U. The even more irresistible SROIQ // Proc. of the Tenth Int. Conf.

Principles of Knowledge Representation and Rea Cемантическая трансформация канонической информационной модели в формальный язык спецификаций для верификации уточнения © С.А. Ступников Институт проблем информатики РАН, г. Москва ssa@ipi.ac.ru • интеграция информационных моделей ресур Аннотация сов;

Cтатья посвящена разработке методов и • регистрация ресурсов в предметных посред средств достижения семантической интеро- никах.

перабельности неоднородных информаци- Модели информационных ресурсов предметной онных ресурсов при создании интегриро- области, для которой создается предметный по ванных информационных систем. В качест- средник, могут быть совершенно различными. Це ве основного факта, подлежащего формаль- лью интеграции моделей является создание канони ной проверке, рассматривается уточнение ческой информационной модели, унифицирующей спецификации системы спецификациями (т. е. представляющей однородным образом) модели ресурсов. Предложена трансформация язы- ресурсов [3]. Унификация модели ресурсов R есть ка СИНТЕЗ, нацеленного на разработку приведение ее к канонической информационной предметных посредников для решения за- модели C, т. е. создание такого расширения E кано дач над неоднородными ресурсами в фор- нической модели и такого отображения M исходной мальный язык спецификаций AMN, под- модели в расширенную каноническую, что исходная держивающий уточнение. Тем самым дос- модель уточняет расширенную каноническую мо тигается возможность доказательства уточ- дель. Уточнение моделей означает, что для любой нения спецификаций языка СИНТЕЗ при допустимой спецификации r модели R ее образ M(r) помощи существующих автоматических и при отображении M уточняется спецификацией r.

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

1 Введение Интеграция моделей ресурсов является предвари тельным этапом для регистрации конкретных ре Для обеспечения семантической интеропера сурсов в предметном посреднике [1].

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

мально, спецификация B уточняет спецификацию Еще одним важным этапом регистрации являют A, если пользователь может использовать B вместо ся поиск спецификаций типов ресурсов, релевант A, не замечая факта замены A на B. Перспективной ных типам концептуальной схемы посредника, и технологией, использующей уточнение для верифи доказательство уточнения типами ресурсов типов кации интеграции неоднородных информационных посредника. Тем самым обеспечивается возмож ресурсов, является технология предметных посред ность реализации виртуальной схемы посредника ников [1].

посредством схем ресурсов.

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

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

«Электронные библиотеки: перспективные методы и технологии, электронные коллекции» – RCDL’2010, Казань, Россия, В данной статье в качестве канонической модели щих инвариантов – инвариантов, соотносящих со рассматривается язык СИНТЕЗ [5], нацеленный на стояния уточняемой и уточняющей спецификаций.

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

СИНТЕЗ в формальный язык спецификаций, под 3 Язык трансформации моделей ATL держивающий понятие уточнения. В качестве тако го языка выбрана Нотация абстрактных машин Базовыми составляющими MDA являются моде (AMN) [2], для которой существуют специализиро- ли. Они рассматриваются как первичные сущности, ванные инструментальные средства доказательства и наиболее важными операциями манипулирования уточнения [6]. Трансформация реализует отображе- моделями становятся трансформации моделей из ние языка СИНТЕЗ в AMN [11] и представляет со- одной в другую. Модель определяется в соответст бой программу, получающую на вход произвольную вии с семантикой некоторой метамодели, при этом допустимую спецификацию на языке СИНТЕЗ и говорят, что модель конформна (conforms to) мета автоматически порождающую соответствующую модели. Стандартом MOF определена четырехуров спецификацию на языке AMN. При этом можно невая архитектура моделей: модели уровня М0 опи говорить, что языку СИНТЕЗ сообщается формаль- сывают объекты реального мира, модели уровня М ная семантика в языке AMN, а потому данная называются обычно схемами, модели уровня М трансформация называется семантической. Статья представляют собой собственно информационные сосредоточена на трансформации основных объект- модели, модели уровня М3 – метаметамодели, пред ных черт языка СИНТЕЗ. назначенные для описания моделей уровня М2.

В качестве языка для определения трансформа- ATL представляет собой декларативно-импера ции выбран ATL (ATLAS Transformation Language) тивный язык, позволяющий описывать способ по [10]. ATL является одним из языков трансформации рождения моделей (называемых целевыми) на осно моделей, разрабатываемых в контексте Движимой вании моделей, называемых исходными. Система моделями архитектуры (MDA), поддерживаемой типов и операций над типами языка ATL очень стандартом MOF [8] консорциума OMG. близка (но не тождественна) системе типов языка Статья организована следующим образом. В OCL. Для языка ATL на базе платформы Eclipse разделах 2 и 3 описаны основные черты языков реализована интегрированная среда разработки, AMN и ATL соответственно. В разделе 4 рассмот- называемая ATL Development Tools (ADT). В каче рена и продемонстрирована на примере трансфор- стве модели уровня М3 языком ATL поддерживает мация канонической информационной модели в ся модель Ecore [9].

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

• какой элемент исходной модели должен быть ными типами и конструкторами типов (сортов).

Язык предикатов AMN включает обычный набор взят;

логических связок (конъюнкцию, дизъюнкцию, им- • количество и тип порождаемых элементов пликацию, отрицание), кванторы существования, целевой модели;

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

ми машинами. AMN позволяет интегрированно рас- Целью данной статьи является описание транс сматривать спецификацию пространства состояний формации, преобразующей язык СИНТЕЗ в язык и поведения машины (определенного операциями AMN. При этом абстрактный синтаксис языков на состояниях). Спецификация состояния вводится СИНТЕЗ и AMN представляется в виде моделей переменными состояния вместе с инвариантами – уровня M2 (называемых Synthesis и Amn соответст ограничениями, которые должны всегда удовлетво- венно), конформных метамодели Ecore. Трансфор ряться. Операции абстрактных машин основаны на мация автоматически порождает схему (модель обобщенных подстановках (generalized substitu- уровня M1), удовлетворяющую модели Amn, на ос tions), описывающих переходы между состояниями новании схемы, удовлетворяющей модели Synthesis.

системы.

Уточнение формализуется в AMN путем форму лировки ряда теорем специального вида, так назы ваемых proof obligations. Такие теоремы формули руются автоматически при помощи инструменталь ных средств поддержки [6] на основании склеиваю включает атрибуты classSize (максимальный размер 4 Трансформация канонической инфор класса тестируемых студентов), enrolled (множество мационной модели в язык AMN студентов, находящихся в классе в данный момент) и tested (множество тех студентов, находящихся в 4.1 Спецификация на языке СИНТЕЗ классе, которые прошли тестирование). Метод en Рассмотрим пример части спецификации пред- roll вызывается при входе нового студента в класс, метного посредника University в предметной облас- метод test – при окончании студентом тестирования, ти высшего образования. Синтаксически элементы метод leave – при выходе студента из класса. Спе языка СИНТЕЗ представляются фреймами, заклю- цификации методов представляют собой формулы чаемыми в фигурные скобки. Фреймы состоят из многосортного объектного исчисления – типизиро слотов, разделяемых точкой с запятой. Слот состо- ванного варианта логики предикатов первого по ит из имени и списка значений. Имя слота отделяет- рядка. Формулы задают смешанные пред- и посту ся от списка значений двоеточием, значения одного словия методов.

слота разделяются запятыми. В формулах ключевое слово this указывает на текущий экземпляр типа;

функция cardinal обозна { University;

in: module;

чает мощность множества;

предикат is_in – принад type: лежность элемента множеству;

функции union и { Person;

in: type;

code: integer;

}, differ – объединение и разность множеств;

предикат { Student;

in: type;

supertype: Person;

= – отношение подмножества на множествах и grade: integer;

}, отношение «меньше либо равно» на числах;

логиче { ClassManager;

in: type;

ские связки &, ^, - – конъюнкцию, отрицание и enrolled: {set;

type_of_element: Student;

};

импликацию;

all – квантор существования;

/ – типи tested: {set;

type_of_element: Student;

};

зацию переменной некоторым типом;

термы, отме classSize: integer;

ченные апострофом, ссылаются на состояние экзем subset: { in: invariant;

пляра типа после выполнения метода, т. е. обозна { all cm/ClassManager (cm.tested = cm.enrolled & чают побочные эффекты метода.

cardinal(cm.enrolled) = cm.classSize) } Так, предусловиями метода enroll является про };

верка того, что текущее количество студентов в enroll: { in: function;

params: {+st/Student};

классе меньше максимально допустимого (cardi {{ cardinal(this.enrolled) this.classSize & nal(this.enrolled) this.classSize) и что студент, же ^is_in(this.enrolled, st) & лающий войти в класс, еще не входил в класс this.enrolled’ = union(this.enrolled, {st}) }} (^is_in(this.enrolled, st)). Если предусловие выполня };

ется, студент считается вошедшим в класс, т. е. по test: { in: function;

params: {+st/Student};

мещается в множество enrolled (this.enrolled’= {{ is_in(this.enrolled, st) & union(this.enrolled, {st})).

^is_in(this.tested, st) & В определения типов могут быть включены ин this.tested’ = union(this.tested, {st}) }} варианты типов – ограничения, выраженные в виде };

замкнутой логической формулы. Например, инвари leave: { in: function;

params: {+st/Student};

ант subset утверждает, что каждый тестируемый {{ is_in(this.enrolled, st) & студент является вошедшим в класс (tested = en this.enrolled’ = differ(this.enrolled, {st}) & rolled) и что количество вошедших не может быть (is_in(this.tested, {st}) - больше максимального (cardinal(enrolled) = class this.tested’ = differ(this.tested, {st}) & Size).

(is_in(this.tested, {st}) this.tested’ = this.tested) 4.2 Формализация абстрактного синтаксиса язы }} ка СИНТЕЗ };

Рассмотрим теперь, каким образом абстрактный };

} синтаксис языка СИНТЕЗ представляется в виде Основной единицей определения канонической модели Synthesis уровня M2, конформной метамо модели является модуль [5] (University), включаю дели Ecore [9]. Элементами модели, конформной щий определения абстрактных типов данных (АТД).

Ecore, могут быть классы (EClass), атрибуты (EAt Пример включает три типа: Person, Student и Class tribute), ссылки (EReference). Например, синтаксис Manager. Тип Student является подтипом типа Per АТД формализуется следующим классом ADTDef son (значение подтипа может использоваться всюду, метамодели Ecore:

где ожидается значение супертипа;

подтип наследу ет элементы спецификации супертипа, например, eClassifiers xsi:type="ecore:EClass" name="ADTDef" атрибут code). eSuperTypes="#//TypeDef" АТД описывают состояние и поведение своих eStructuralFeatures xsi:type="ecore:EReference" экземпляров в терминах атрибутов и методов ти- name="attributes" upperBound="-1" па. Так, тип ClassManager (описывающий препода- eType="#//AttributeDef" вателя, управляющего тестированием студентов), eOpposite="#//AttributeDef/attributeOf"/ eStructuralFeatures xsi:type="ecore:EReference" Для того чтобы продемонстрировать, каким об name="invariants" upperBound="-1" разом конкретные спецификации на языке СИНТЕЗ eType="#//InvariantDef"/ представляются в модели Synthesis, рассмотрим eStructuralFeatures xsi:type="ecore:EReference" фрагмент спецификации University:

name="subtypes" lowerBound="1" upperBound="-1" eType="#//ADTDef" eOpposite="#//ADTDef/supertypes"/ 1 xmi:XMI xmi:version="2.0" eStructuralFeatures xsi:type="ecore:EReference" syn:ModuleDef name="University" name="supertypes" upperBound="-1" eType="#//ADTDef" 2 containedTypes="/2 /3 /4"/ eOpposite="#//ADTDef/subtypes"/ syn:ADTDef name="Person" typeInModule="/0" /eClassifiers 3 attributes="/6 "/ syn:ADTDef name="Student" Из описания можно видеть, что класс ADTDef typeInModule="/0" attributes="/7" наследуется от класса TypeDef и обладает атрибута 4 supertypes="/1"/ ми (attributes), инвариантами (invariants), подтипа syn:ADTDef name="ClassManager" ми (subtypes) и супертипами (supertypes). Без «син 5 typeInModule="/0" attributes="/8" / таксического сахара» XML это описание может 6 syn:IntegerDef/ быть представлено в следующем виде:

syn:AttributeDef name="code" attributeOf="/1" ADTDef(attributes: AttributeDef*, invariants: InvariantDef*, 7 type="/5"/ subtypes: ADTDef*, supertypes: ADTDef*): TypeDef syn:AttributeDef name="grade" attributeOf="/2" 8 type="/5"/ Знак * здесь означает кардинальность свойства:

syn:FunctionDef name="enroll" parameters="/9" например, АТД может обладать несколькими атри 9 predicativeSpec="/10" бутами или инвариантами. Целиком фрагмент мо syn:ParameterDef name="st" дели Synthesis, необходимый для представления parameterKind="input" parameterOf="/8" спецификации University (раздел 4.1), выглядит сле 10 type="3"/ дующим образом:

11 syn-form:Conjunction formula="/11 /12 /13" / ValueDef(typeOfValue: TypeDef) syn-form:ArithmeticPredicate symbol="le" ElementDef(name: String): ValueDef 14 terms="/14 /15" / FrameDef(parameters: ParameterDef*): ElementDef syn-form:BuiltInFunction name="cardinal" ParameterDef(parameterKind: String, 16 terms="/16" / parameterOf: FrameDef, type: TypeDef): ElementDef syn-form:GetFunction name="enrolled" TypeDef(typeInModule: ModuleDef): FrameDef 17 terms="/17" / ModuleDef(containedTypes: TypeDef*): FrameDef syn-form:Variable name="this"/ ADTDef(attributes: AttributeDef*, invariants: InvariantDef*, /xmi:XMI subtypes: ADTDef*, supertypes: ADTDef*): TypeDef AttributeDef(attributeOf: ADTDef, type: TypeDef): Элементы спецификации по умолчанию нуме ElementDef руются последовательными числами для удобства InvariantDef(predicativeSpec: Formula): TypeDef организации ссылок на них. Например, модулю FunctionDef(functionInModule: ModuleDef, University присвоен номер 1, и ссылка на него в дру predicativeSpec: Formula): TypeDef гих элементах спецификации осуществляется сле IntegerDef(unsigned: Boolean): TypeDef дующим образом: /1. Для удобства номера элемен SetDef(ofType: TypeDef): TypeDef тов спецификаций приведены слева (но они не яв SetValueDef(values: ValueDef):ValueDef ляются частью спецификации).

Formula() 4.3 Отображение спецификаций в язык AMN Variable(): ValueDef QuantifiedFormula(variables: Variable*, Рассмотрим теперь, каким образом модуль Uni formula: Formula): Formula versity представляется в AMN.

ExsistentiallyQuantifiedFormula(): QuantifiedFormula MACHINE University_Context UniversallyQuantifiedFormula(): QuantifiedFormula SETS Obj;

OID Conjunction(formula: Formula*):Formula ABSTRACT_CONSTANTS self, Negation(formula: Formula): Formula Implication(antecedent: Formula, consequent: Formula): ext_Person, ext_Student, ext_ ClassManager Formula PROPERTIES self: Obj - OID & CollectionComprehension(vars: Variable*, ext_Person: POW(Obj) & ext_Student: POW(Obj) & formula: Formula): ValueDef ext_ClassManager: POW(Obj) & Atom(symbol: String, terms: ValueDef): Formula ext_Student : ext_Person BuiltInPredicate(): Atom END ArithmeticPredicate(): Atom SetPredicate(): Atom REFINEMENT Person FunctionCall(terms: ValueDef): ElementDef SEES University_Context BuiltInFunction(): FunctionCall AccessFunction(): FunctionCall ABSTRACT_VARIABLES code SetFunction(): AccessFunction INVARIANT code: ext_Person -- INTEGER GetFunction(): AccessFunction END Представление типа множеством своих потенци REFINEMENT Student альных экземпляров позволяет естественным обра SEES University_Context зом моделировать атрибуты типа функциями AMN:

EXTENDS Person атрибут enrolled моделируется функцией enrolled:

ABSTRACT_VARIABLES grade ext_ClassManager -- POW(ext_Student) в разделе INVARIANT grade: ext_Student -- INTEGER переменных машины ClassManager.

END Инварианты типа (например, subset) представ ляются конъюнктивными частями раздела REFINEMENT ClassManager INVARIANT соответствующей машины (знак ! в SEES University_Context AMN обозначает квантор всеобщности, : – отно ABSTRACT_VARIABLES classSize, enrolled, tested шение подмножества).

INVARIANT classSize: INTEGER & Методы типа (например, enroll) представляются enrolled: ext_ClassManager -- POW(ext_Student) & операциями абстрактной машины (операции, соот tested: ext_ClassManager -- POW(ext_Student) & ветствующие остальным методам, опущены). Пер !cm.( cm: ext_ClassManager = вым входным параметром av операции является tested(cm) : enrolled(cm) & объект, для которого вызывается метод. В преду card(enrolled(cm) = classSize(cm)) ) словиях PRE операции осуществляется типизация OPERATIONS входных параметров.

enroll(av, st) = Одной из основных особенностей представления PRE av: ext_ClassManager & st: ext_Student предикативных спецификаций методов языка THEN СИНТЕЗ в AMN является выделение помеченных ANY v WHERE card(enrolled(av)) classSize(av) & апострофом термов, которые ссылаются на состоя not(st: enrolled(av)) & v = enrolled(av) \/ {st} ние экземпляра типа после выполнения метода (на THEN пример, this.enrolled’). Для каждого из таких термов enrolled(av) := v заводится новая переменная (v), вхождение терма в END спецификацию метода заменяется на вхождение END переменной. Сама спецификация метода представ END ляется в AMN подстановкой неограниченного вы Модуль представляется в AMN набором абст- бора ANY. Подстановка ANY v WHERE P(v) THEN S рактных машин, состоящим из контекстной машины END устанавливает переменной v произвольное (University_Context) и машин, соответствующих значение, удовлетворяющее предикату P(v), после АТД модуля. Контекстная машина содержит ин- чего выполняется вложенная подстановка S. Вло формацию, характеризующую модуль как целое, женной подстановкой представляются побочные машины типов содержат информацию, характерную эффекты метода.

для отдельных типов.

4.4 Формализация абстрактного синтаксиса язы Представление АТД в AMN основано на экстен ка AMN сиональном принципе: тип представляется кон стантным множеством потенциальных экземпляров Рассмотрим, каким образом абстрактный син этого типа. Такое множество называется экстенсио- таксис языка AMN представляется в виде модели налом типа (например, ext_ClassManager). Множе- AMN уровня M2, конформной метамодели Ecore.

ство потенциальных экземпляров всех абстрактных Как и модель Synthesis (раздел 4.2), модель AMN типов моделируются константным множеством рассматривается в данном разделе в виде, лишенном AVAL, так что для каждого типа T с экстенсионалом «синтаксического сахара» XML. Целиком фрагмент ext_T выполнено ext_T: POW(AVAL). Здесь знак «:» модели AMN, необходимый для представления спе означает принадлежность множеству, POW – мно- цификации University (раздел 4.3), выглядит сле жество подмножеств. Для каждой пары тип – дующим образом:

подтип (например, Person и Student) выполнено отношение включения на экстенсионалах Machine(sees: AbstractMachine*, (ext_Student : ext_Person). Таким образом моде- extends: AbstractMachine*, sets: Set*, лируется иерархия типов. Для обеспечения уни- properties: Predicate, invariant: Predicate, operations: Operations*): Element кальной идентификации объектов вводится множе Refinement(abstractConstants: Element*, ство объектных идентификаторов OID. Биекция self:

abstractVariables: Element*):Machine Obj - OID моделирует неявный атрибут self Operation(inputParams: Variable*, outputParams: Variable*, каждого типа. Упомянутые константы и их свойства Substitution: Substitution): Element определяются в контекстной машине. Структура Element(name: String) спецификаций типов канонической модели также Set(): Element моделируется при помощи средств композиции аб- Deferred(): Set страктных машин. Так, машина, соответствующая типу Student, расширяет (EXTENDS) машину, соот- Predicate(stringRepr: String) QuantifiedPredicate(variables: Variable*, ветствующую супертипу Person.

predicate: Predicate): Predicate UniversallyQuantified(): QuantifiedPredicate   ),  ExistentiallyQuantified(): QuantifiedPredicate   selfProp: AMN!AtomicPredicate(  AtomicPredicate(sign: String, expression: Expression*):    sign  ':', expression  selfConst,  Predicate    expression  selfType),  Conjunction(predicate: Predicate*): Predicate   selfType: AMN!BinaryOperator (  Negation(predicate: Predicate): Predicate    sign  '', expression  objConst,  Disjunction(predicate: Predicate*): Predicate    expression  oidSet  Implication(antecedent: Predicate, consequent: Predicate):   )  Predicate }  Equivalence(predicate: Predicate*): Predicate   Контекстной машине присваивается имя, добав Expression() ляются константные множества Obj и OID и преди SetComprehension(variable: Variable*, кат propertiesPredicate, описывающий их свойства predicate: Predicate): Expression (см. раздел 4.3). В секции from правила описывается OperationalExpression(sign: String): Expression имя (m) и тип (Synthesis!ModuleDef) входного эле UnaryOperator(expression: Expression):

мента, в секции to – имена (am, objSet, oidSet, self OperationalExpression Const, selfProp, selfType) и типы выходных элемен BiaryOperator(expression: Expression*):

тов. Для каждого выходного элемента устанавлива OperationalExpression FunctionalExpression(expression: Expression*): ются его свойства. Так, например, контекстной ма OperationalExpression шине присваивается имя: name - m.name + Variable(name: String): Expression '_Context'.

NamedConstant (name: String): Expression При помощи отдельного правила в контекстную IntegerValue(value: Integer): Expression машину добавляются константы и предикаты, отра IntegerValue(values: Expression): Expression жающие экстенсиональный принцип представления АТД в AMN:

Substitution() BecomesEqual(leftExpression: Expression*, rightExpression: Expression*): Substitution rule ADT2ContextMachineProperties{  Precondition(pre: Predicate,  from adt : Synthesis!ADTDef  thenPart: Substitution): Substitution  to   Any(any: Variable*, where: Predicate,   ext: AMN!NamedConstant(  thenPart: Substitution):Substitution    name  'ext_' + adt.name    ),  4.5 Правила трансформации языка СИНТЕЗ в   pred: AMN!AtomicPredicate (  AMN    sign  ':', expression  ext,     expression  extType  Трансформация, преобразующая спецификации   ),  языка СИНТЕЗ в спецификации языка AMN, пред-   extType: AMN!FunctionalExpression(  ставляет собой модуль языка ATL, получающий на    sign  'POW',   вход модель уровня M1, конформную модели Syn-    expression  thisModule.resolveTemp(  thesis и порождающую модель уровня M1, кон-     adt.typeInModule,'objConst')  формную модели AMN. Заголовок модуля выглядит   ),  следующим образом:  do {    thisModule.resolveTemp(adt.typeInModule,       'am').abstractConstants  ext;

  module Synthesis2AMN;

    thisModule.resolveTemp(adt.typeInModule,   create OUT:AMN from IN:Synthesis;

     'propertiesPredicate').predicate  pred;

  }}  Правило, порождающее контекстную машину am на основании модуля m языка СИНТЕЗ, выгля При помощи этого правила, например, в машину дит следующим образом:

University_Context добавляются константа   ext_Person и предикат ее типизации ext_Person:

rule SynthesisModule2AMNAbstractMachine {  POW(Obj). Можно заметить, что в правиле исполь  from m: Synthesis!ModuleDef  зуется секция императивного кода do (выполняю  to   щегося после создания элементов, указанных в сек   am: AMN!AbstractMachine (  ции to). Специальная функция resolveTemp приме    name  m.name + '_Context',     sets  Sequence{objSet, oidSet},  няется для того, чтобы получить доступ к элемен    abstractConstants   там, созданным другими правилами. Так, выраже     Sequence{objConst, selfConst},  ние thisModule.resolveTemp(adt.typeInModule, 'am')    properties  propertiesPredicate  возвращает контекстную машину, созданную на   ),      основе модуля adt.typeInModule языка СИНТЕЗ (ко   objSet: AMN!Deferred(name  'Obj'),  торому принадлежит АТД adt) правилом   oidSet: AMN!Deferred(name  'OID'),  SynthesisModule2AMNAbstractMachine.

  selfConst: AMN!NamedConstant(name'self'),  Правило, порождающее отдельную машину для   propertiesPredicate : AMN!Conjunction (  каждого АТД, выглядит следующим образом:

   predicate  Sequence{selfProp}        Synthesis!IntegerDef))     thisModule.AttributeTypeStringExp(at,   rule ADT2Machine {     'NAT');

   from adt : Synthesis!ADTDef    if(at.type.oclIsTypeOf(Synthesis!SetDef))   to      thisModule.AttributeTypeSetDef(at);

    am: AMN!AbstractMachine (    thisModule.resolveTemp(at.attributeOf,     name  adt.name,     'am').abstractVariables  attrVar;

     invariant  predicate,    thisModule.resolveTemp(at.attributeOf,      sees  thisModule.resolveTemp(      'predicate').predicate  attrPred;

      adt.typeInModule, 'am')  }}     ),  Правило создает переменную машины, соответ   predicate: AMN!Conjunction(),  ствующую атрибуту (например, enrolled) и предикат  do {  типизации этой переменной (например, enrolled:

  if(adt.subtypesnotEmpty()){     for(e in adt.subtypes)  ext_ClassManager -- POW(ext_Student)). При этом     thisModule.genStrictInclusion(adt,e);

  для отображения типа атрибута используются спе   }  циальные правила AttributeTypeStringExp (для про   if(adt.supertypesnotEmpty()){  стых типов, например, integer) и AttributeTypeSetDef    for(e in adt.supertypes)  для типов множества:

    am.extendsClause         thisModule.resolveTemp(e, 'am');

  rule AttributeTypeStringExp(    }    attr: Synthesis!AttributeDef,  }    stringVal: String){  Правило добавляет контекстную машину в сек-  to  цию SEES машины типа;

добавляет машины, соот-   funcExp: AMN!StringValue(  ветствующие супертипам в секцию EXTENDS, а    value  stringVal  также для каждого подтипа вызывает правило Gen-   )   do {  StrictInclusion, добавляющее в контекстную машину   thisModule.resolveTemp(attr,   предикаты, моделирующие иерархию типов (на   'totalFunction').expression  funcExp;

  пример, ext_Student : ext_Person):

}}  rule GenStrictInclusion(  rule attributeTypeSetDef(    adt : Synthesis!ADTDef,    attr: Synthesis!AttributeDef){    subType: Synthesis!ADTDef){   to   to    funcExp : AMN!FunctionalExpression(    inclusion: AMN!AtomicPredicate(     sign  'POW',     sign  ':',      expression  thisModule.resolveTemp(     expression  Sequence{      attr.type.ofType, 'ext')      thisModule.resolveTemp(subType,'ext'),    )      thisModule.resolveTemp(adt, 'ext')   do{     }    thisModule.resolveTemp(attr,  'totalFunc   )  tion').expression  funcExp;

   do{  }}    thisModule.resolveTemp(  Заметим, что правило Attribute2MachineSections    adt.typeInModule,'propertiesPredicate').  применяется только для атрибутов, тип которых не     predicate  inclusion;

  есть тип функции. Данное предусловие проверяется }}  при помощи вспомогательного правила Правило, порождающее на основании специфи- IsNotFunctional:

кации атрибута АТД соответствующие конструкции helper context Synthesis!AttributeDef def:  в машине типа, выглядит следующим образом:

  IsNotFunctional(): Boolean =    rule Attribute2MachineSections {   if self.oclIsTypeOf(Synthesis!AttributeDef)  from at: Synthesis!AttributeDef(   then             at.isNotFunctional())    if not self.type.oclIsTypeOf(  to            Synthesis!FunctionDef)   attrPred : AMN!AtomicPredicate (    then true    sign  ':', expression  attrVar,    else false    expression  totalFunction    endif   ),   else false   totalFunction : AMN!BinaryOperator (   endif;

    sign  '',  Функциональные атрибуты отображаются в опе   expression  thisModule.resolveTemp(  рации машин при помощи следующего правила:

                 at.attributeOf, 'ext')   ),  rule Function2Operation{     attrVar: AMN!Variable(name  at.name),   from at: Synthesis!AttributeDef(   do{            at.isFunctional())    if(at.type.oclIsTypeOf(  вила для преобразования встроенных предикатов  to  (например, is_in):

  operation: AMN!Operation(     name  at.name,  rule BuiltInPredicate2AtomicPredicate{     inputParams  objParam,   from builtIn : Synthesis!BuiltInPredicate     substitution  subst   to    ),    atomPred: AMN!AtomicPredicate(    objParam: AMN!Variable(name  'av'),     expression  builtIn.terms    subst: AMN!Precondition(    )     pre  precondPredicate,   do{     thenPart  thenSubstAny     if(builtIn.symbol = 'is_in')    ),     atomPred.sign  ':';

    precondPredicate: AMN!Conjunction(   }     predicate  objPred      ),  переменных:

  objPred: AMN!AtomicPredicate (     sign  ':',  rule Variable{     expression  thisModule.resolveTemp(   from synthVar: Synthesis!Variable                    at.attributeOf, 'ext'),   to    expression  objParam    amnVar: AMN!Variable(namesynthVar.name)    ),  }    thenSubstAny: AMN!Any(     where  whereConj,  логических связок (например, конъюнкции):

   thenPart  sequenceSubstitution    ),  rule Сonjunction{    whereConj : AMN!Conjunction (   from conjSynth: Synthesis!Conjunction     predicate  at.type.predicativeSpec   to    ),    conjAMN: AMN!Conjunction(    sequenceSubstitution : AMN!SequenceSubst()     predicate  conjSynth.formula   do{    )    for(e in at.type.parameters)  }     if(e.type.oclIsTypeOf(Synthesis!ADTDef))      thisModule.generateParameters(e, at);

  арифметических предикатов:

  thisModule.resolveTemp(at.attributeOf,     'am').operations  operation;

  rule ArithmeticPredicate2BinaryOperator{  }}   from     arithmPred: Synthesis!ArithmeticPredicate  Правило создает операцию машины, соответст  to   вующую функциональному атрибуту (например,   atomPred: AMN!BinaryOperator(  enroll), присваивает ей имя, создает первый пара    sign  arithmPred.symbol,  метр av операции его предикат типизации (напри    expression  arithmPred.terms  мер, av: ext_ClassManager), создает подстановки,   )  составляющие тело операции. Дополнительное пра- }  вило GenerateParameters создает остальные пара метры операции и их предикаты типизации (напри- встроенных функций (например, union):

мер, st: ext_Student):

rule BuiltInFunction2FunctionalExpression{  rule GenerateParameters(   from builtIn: Synthesis!BuiltInFunction    param: Synthesis!ParameterDef,   do{    attr: Synthesis!AttributeDef){    if(builtIn.name = 'union')   to      thisModule.genUnion(builtIn);

    var: AMN!Variable(name  param.name),  }    varPred: AMN!AtomicPredicate(  rule genUnion(     sign  ':', expression  var,     builtIn: Synthesis!BuiltInFunction){     expression  thisModule.resolveTemp(   to                    param.type, 'ext')    funcExp: AMN!BinaryOperator(    )     sign  '\\/', expression  builtIn.terms    do{    )     if(param.parameterKind = 'input')  }      thisModule.resolveTemp(attr,       'operation').inputParams  var;

  значений (например, целочисленных):

   thisModule.resolveTemp(attr,  rule Term2AMNIntegerValue{      'precondPredicate').predicate  varPred;

   from term: Synthesis!IntegerValueDef  }}   to  Каждая из конструкций, составляющих формулы   integerVal: AMN!IntegerValue (  языка СИНТЕЗ, преобразуется в формулы AMN при    value  term.value )  помощи отдельного правила. Так, существуют пра- }  и других видов выражений. ing in heterogeneous information resource envi Ввиду ограничения размера статьи, набор пра- ronments.– M.: IPI RAS, 2007. – 171 p.

вил, приведенный в данном разделе, не образует [6] Atelier B. The industrial tool to efficiently deploy полную трансформацию (в большинстве случаев the B method. – http://www.atelierb.eu/index даже описание самих правил не является полным). en.php.

Однако приведенные правила позволяет продемон- [7] ATL Project. – http://www.eclipse.org/m2m/atl/.

стрировать основные принципы построения транс- [8] Meta Object Facility (MOF) 2.0 Core Specifica формации. tion. – http://www.omg.org/cgi-bin/doc?formal/06 01-01.pdf, 2006.

[9] Budinsky F., Steinberg D., Ellersick R., Grose T.

5 Заключение Eclipse modeling framework, chapter 5 ”Ecore Одним из способов обеспечения семантической modeling concepts”. – Addison Wesley Profes интероперабельности неоднородных информацион- sional, 2004.

ных ресурсов при создании интегрированных ин- [10] Candela L., Castelli D., Ferro N., Ioannidis Y. et al.

формационных систем является использование ме- The DELOS digital library reference model – foun тодов и средств формализации уточнения. Исполь- dations for digital libraries. Version 0.98. – зование ресурса для реализации части интегриро- http://www.delos.info/files/pdf/ReferenceModel/D ванной системы является правомочным, если спе- ELOS_DLReferenceModel_0.98.pdf, 2008.


цификация ресурса уточняет часть спецификации [11] Ступников С.А. Отображение спецификаций, системы. выраженных средствами ядра канонической мо Перспективной технологией, использующей дели, в язык AMN // Системы и средства ин уточнение для верификации интеграции неоднород- форматики: Спец. вып. Формальные методы и ных информационных ресурсов, является техноло- модели в композиционных инфраструктурах гия предметных посредников. В статье рассматри- распределенных информационных систем / Под вается трансформация канонической информацион- ред. И.А. Соколова. – М.: ИПИ РАН, 2005. – ной модели посредников (языка СИНТЕЗ) в фор- C. 69-95.

мальный язык спецификаций AMN, поддерживаю щий уточнение. Таким образом, канонической мо A semantic transformation of the canonical дели сообщается формальная семантика, и достига information model into a formal ется возможность доказательства уточнения специ specification langage for the refinement фикаций канонической модели при помощи суще verification ствующих автоматических и интерактивных систем доказательства.

S.A. Stupnikov Литература The paper is devoted to the development of methods and tools achieving the semantic interoperability of [1] Kalinichenko L.A., Briukhov D.O., Mar heterogeneous information resources during the devel tynov D.O., Skvortsov N.A., Stupnikov S.A. Me opment of integrated information systems. A refinement diation framework for enterprise information sys of a system specification by the resources specifications tem infrastructures // The 9th Int. Conf. on Enter is considered as a basic fact requiring a formal proof. A prise Information Systems (ICEIS). – 2007. – P.

transformation of the SYNTHESIS language aimed at 246-251.

development of subject mediators for tasks solving over [2] Abrial J.-R. The B-book: assigning programs to heterogeneous resources into AMN formal specification meanings. – Cambridge: Cambridge University language supporting the refinement. Thus a possibility Press, 1996.

of refinement proving in the SYNTHESIS language [3] Захаров В.Н., Калиниченко Л.А. Ступни with the help of the existing automatic/interactive ков С.А. Конструирование канонических ин proves is achieved.

формационных моделей для интегрированных информационных систем // Информатика и её Работа выполнена при финансовой поддержке РФФИ применения. – 2007. – Т. 1, Вып. 2. – С. 15-38.

(проекты 08-07-00157, 10-07-00342, 10-07-00640) и Про [4] Скворцов Н.А. Применение уточнения понятий граммы фундаментальных исследований Президиума в решении задач манипулирования онтологиями РАН № 3 – Фундаментальные проблемы системного про // Труды Девятой Всерос. науч. конф. «Элек- граммирования, раздел 4 – Системы управления базами тронные библиотеки: перспективные методы и данных, проект – Исследование методов и средств про технологии, электронные коллекции», RCDL' межуточного слоя предметных посредников, обеспечи 2007. – Университет города Переславля: Пере- вающего решение задач над множеством неоднородных славль-Залесский, 2007. – C. 225-229. распределенных информационных ресурсов [5] Kalinichenko L.A., Stupnikov S.A., Martynov D.O.

SYNTHESIS: a language for canonical information modeling and mediator definition for problem solv От спецификаций требований к концептуальной схеме © А.Е. Вовченко1, В.Н. Захаров1, Л.А. Калиниченко1, Д.Ю. Ковалёв2, О.В. Рябухин1, Н.А. Скворцов1, С.А. Ступников Институт проблем информатики РАН, г. Москва Московский государственный университет им. М. В. Ломоносова leonidk@synth.ipi.ac.ru, dm.kovalev@gmail.com, nskv@ipi.ac.ru Однако вопросы обоснованного формирования Аннотация самих спецификаций предметной области для ре Статья представляет исследование методов шения задач в среде предметных посредников до проектирования концептуальных схем сих пор не рассматривались. Целью настоящей ра предметных областей для решения задач. боты является разработка семантически акцентиро При проектировании используется семан- ванного подхода к конструированию концептуаль тически акцентированный подход к форми- ных схем предметной области для решения задач в рованию спецификаций предметной облас- среде предметных посредников, исходя из сформу ти. Процесс проектирования включает фор- лированных на естественном языке спецификаций мулирование модели требований к пред- требований к задаче, таких, как техническое зада метной области, исходя из вербальных спе- ние.

цификаций требований к задаче, разработку Данная проблема соприкасается с областями, онтологии предметной области и преобра- имеющими большую историю развития [2]. Кон зование онтологии к концептуальной схеме. цептуальные схемы баз данных используются как Затронуты вопросы реализации концепту- логическое представление информационных струк альной схемы предметной области в среде тур, понятное человеку и независимое от способа предметных посредников. реализации в информационных системах. С разви тием моделей данных развивались и представления 1 Введение о концептуальных схемах, которые помимо струк тур включали спецификации поведения. Техноло В лаборатории Композиционных методов проек гии объектно-ориентированного анализа и дизайна тирования информационных систем Института про используют результаты, полученные в области кон блем информатики РАН разработаны методы и цептуальных схем баз данных, для разработки объ средства решения задач над неоднородными ин ектных спецификаций информационных систем, формационными ресурсами в среде предметных независимых от реализации. Исследования в облас посредников. Они включают средства: специфика ти онтологии продиктованы проблемами семанти ции концептуальной модели предметной области ческой интероперабельности систем и специализи задачи, унификации неоднородных информацион руются на формальном описании понятий предмет ных моделей, регистрации неоднородных информа ных областей, понятных как человеку, так и маши ционных ресурсов в посреднике и исполнительную не.

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

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

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

Труды 12й Всероссийской научной конференции «Электронные библиотеки: перспективные методы и технологии, электронные коллекции» – RCDL’2010, Казань, Россия, решения конкретной задачи. Термины «онтология»

2 Исследования, связанные с настоящей и «концептуальная схема» при этом часто исполь работой зуются непоследовательно. Так, множество проек Среди исследований, которые необходимо упо- тов манипулирует термином «онтология», имея в мянуть, говоря о проектировании концептуальных виду схемы баз данных, либо базы знаний, основан схем баз данных и информационных систем и исхо- ные на информационных моделях, используемых дя из спецификаций требований, наиболее известны для спецификации онтологий. Появляются также работы, связанные с языком спецификации UML работы по проектированию концептуальных схем [uml]. При разработке схем информационных сис- на основе онтологий, фактически же разрабаты тем на UML вначале рассматриваются участвующие вающие отображение спецификаций схем из одной агенты и их деятельности. Затем описывается по- информационной модели в другую.

следовательность их взаимодействия при помощи Необходимо отметить предшествующие резуль сигнатур функций и, наконец, определяется объект- таты, связанные с технологией предметных посред ная схема, специфицирующая информационную ников, в контексте которой проводится настоящее структуру классов и их поведение в соответствии с исследование. Для спецификации концептуальной деятельностями агентов. Спецификации функций схемы предметной области посредника в проекте задаются на языке ограничений OCL. Таким обра- используется развитый объектно-фреймовый язык зом, процесс разработки в целом ориентирован, в СИНТЕЗ [8] с логической ориентацией. Для него первую очередь, на сигнатуры функций, опреде- разработано отображение [9] в язык AMN, что по ляющих компоненты процесса решения задачи. зволяет формально обосновывать корректность Такой подход, рассматривающий деятельности уточнения типов при отображении спецификаций, и агентов как чёрные ящики, критикуется в работах в частности, проверять корректность регистрации Дж. Милопулоса и др. [3], и в качестве решения схем неоднородных информационных ресурсов в проблемы предлагается технология выделения по- посреднике.

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


ные требования, предъявляемые к разрабатываемым системам. 3 Подход к разработке спецификаций При исследовании семантически акцентирован предметной области ного подхода к проектированию концептуальных схем следует опираться на онтологическое модели- Предлагаемый подход к проектированию кон рование и методологии разработки онтологий [5]. цептуальных схем в среде предметных посредников Общий принцип разработки онтологий включает является комбинированным, объединяющим подхо анализ предметной области, выделение в ней наи- ды к разработке моделей требований, созданию он более существенных понятий и исследование их тологий и построению концептуальных схем. Про связей, включение в онтологию связанных понятий цесс проектирования включает следующие этапы:

• разработка модели требований к задаче;

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

чивости. Возникают также задачи обратного проек- • построение онтологии предметной области на тирования, когда онтология предметной области основе глоссария;

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

систем. Такой подход позволяет последовательно уточ Различные проекты, связанные с проектировани- нять и формализовать семантику предметной облас ем концептуальных схем на основе знаний, почерп- ти задачи в разрабатываемых спецификациях. При нутых из онтологий, используют в качестве тех и этом в процессе проектирования будут формиро других существенно разные представления. Напри- ваться все необходимые спецификации, составляю мер, в [7] представлен принцип разработки ER- щие определение предметного посредника.

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

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

В процессе обсуждения решаемой задачи со спе циалистами предметной области либо в процессе Выбрать кандидаты в анализа текстов технического задания фиксируются стандарты требования к спецификациям задачи. Требованием OR будем называть условие или способность, которым должна удовлетворять система для решения постав- – Выбрать первичные стан дарты Ландольта ленной задачи или для достижения цели [10]. Спе- Полнота данных цификации выявленных требований уточняются Выбрать вторичные стан путём декомпозиции на более конкретные требова- дарты (стабильные звёз + ния, которые необходимо выполнить, чтобы дос- ды) тичь выполнения рассматриваемых требований. AND При этом естественным образом наиболее общая Выбрать среди объектов спецификация требований конкретизируется дере- звёзды вом требований, которые уточняются на каждом следующем уровне. Декомпозиция выполняется до Выбрать изолированные звёзды тех пор, пока требование может быть сформулиро вано без спецификации способа его выполнения с Выбрать непеременные помощью использования конкретных информаци- звёзды онных ресурсов или агентов. Такой принцип пре- Выбрать качественные кращения декомпозиции требований позволяет аб- звёзды страгироваться от аспектов реализации, которые, в Выбрать звёзды, с малым частности, могут присутствовать в текстах техниче собственным движением ского задания, и, в дальнейшем, выделить понятия предметной области задачи независимо от предмет- Рис. 1. Фрагмент дерева требований ных областей повторно используемых информаци Выбор кандидатов в стандарты может быть вы онных ресурсов.

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

выбрать известные стандарты из таблиц Ландольта ются спецификации функциональных требований, или вторичные стандарты из звёзд со стабильными определяющих функциональность системы, кото рую она должна нести для решения задачи [10]. Де- характеристиками. Первый способ проигрывает при оценке с точки зрения нефункционального требова композиция функционального требования произво ния полноты данных, так как в заданном участке дится с помощью его разбиения на набор требова ний, совместно необходимых для выполнения дан- неба может не оказаться достаточно известных таб личных стандартов.

ного требования (AND-декомпозиция), либо на на Функциональное требование выбора астрономи бор альтернативных требований, выполнение одно го из которых обеспечивает выполнение декомпо- ческих объектов со стабильными характеристиками декомпозировано на пять требований: стандартами зируемого требования (OR-декомпозиция). Нефунк могут быть только звёзды, эти звёзды должны иметь циональные требования определяют качественные атрибуты системы, характеризующие её в разных малое собственное движение, быть изолированны ми, непеременными и качественными с точки зре аспектах, таких как надёжность, полнота информа ции, эффективность, применимость, мобильность и ния астрометрии и фотометрии.

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

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

Имя операции: getZeroMotionStars.

рева требований. Алгоритм выбора плана выполне Вход: набор астрономических объектов.

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

Предусловие: астрономические объекты из входно нальных требований описан в [11]. В требованиях, го набора должны быть звездами.

попавших в план решения задачи, описываются пред- и постусловия для их взаимодействия. Постусловие: для любого объекта из выходного набора астрономических объектов величина соб В качестве примера приведём фрагмент дерева ственного движения равна 0.

требований (рис. 1) для решения задачи в области астрономии, а именно, задачи выбора звёзд стандартов, необходимых для точной калибровки объекта в определённом участке неба. Решение дан Дальнейший анализ вербальных определений 5 Построение онтологии предметной об служит преобразованию тезауруса в онтологию, ласти задачи которая состоит из понятий, их отношений и огра Для описания предметной области, первым де- ничений. Терминам предметной области ставятся в лом, необходимо произвести её концептуализацию. соответствие онтологически определенные понятия.

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

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

В рассматриваемом примере в соответствие тер текстов в дереве требований и в других доку мину Astronomical Object определяется онтологиче ментах описания задачи, определяющие или ское понятие AstronomicalObject, с которым связаны ограничивающие его интерпретации в данной бинарные отношения и свойства: hasCoordinate, предметной области;

• каждый термин снабжается вербальным оп- hasMorphology, hasMagnitude, hasProperMotion, has ColorIndex, isIsolated, isQualitative. Одни из них об ределением, их можно выявить среди выде наруживаются в вербальном определении данного ленных фрагментов текста, либо во внешних понятия, другие следуют из вербальных определе источниках, таких как толковые словари, со ний связанных с ним понятий.

вместно используемые онтологии, публика На языке СИНТЕЗ [8] спецификация бинарного ции, специализированные информационные отношения hasCoordinate выглядит следующим об ресурсы в данной предметной области;

разом:

• из определений по индукции выбираются но вые существенные для задачи термины, и для { hasCoordinate;

них проделывается та же процедура до насы in: association, metaclass;

щения глоссария.

instance_section:

В приведённом выше примере в дереве требова { domain: astronimicalObject;

ний выявляются существенные термины для глос range: coordinate;

сария: Astronomical Object, Star, Standard, Primary inverse: coordinateOf;

Standard, Secondary Standard, Morphology, Quality, } Proper Motion, Isolation. Они определяются вербаль };

но, например: «Astronomical Object – significant physical entity on the sky having electro-magnetic Ниже приведён пример спецификации понятия emission in particular passbands»;

«Proper Motion – AstronomicalObject и некоторых связанных с ним changing of coordinates of astronomical objects on the понятий.

sky caused by relational movement of stars and Solar System». С терминами глоссария связываются ут { AstronomicalObject;

верждения или требования из вербальных специфи metaframe in: metaproperty, entity;

end каций задачи, которые определяют их или ограни in: type, concept;

чивают в предметной области задачи. Так, с терми def: {significant physical entity on the sky having ном Astronomical Object связывается утверждение electro-magnetic emission in particular технического задания: «желательно избегать объек passbands};

тов с большой величиной собственного движения».

coordinate: Coordinate;

Также глоссарий дополняется значимыми термина metaslot in: hasCoordinate;

end ми из вербальных определений уже присутствую morphology: Morphology;

щих в нём терминов и связанных с ними утвержде metaslot in: hasMorphology;

end ний по индукции: Magnitude, Passband, Coordinate, magnitudes: {set;

type_of_element: Magnitude;

};

Coordinate System, Equatorial Coordinate System, metaslot in: hasMagnitude;

end Right Ascension, Declination, и другие.

properMotion: ProperMotion;

Из вербальных определений либо из внешних metaslot in: hasProperMotion;

end источников выявляются семантические отношения colorIndex: ColorIndex;

терминов глоссария, такие, как синонимия, ги metaslot in: hasColorIndex;

end пер/гипонимия, часть/целое, зависимость, ассоциа isIsolated: Isolation;

тивная связь. Определяются свойства терминов:

metaslot in: isIsolated;

end являются ли они сущностями, ролями сущностей, isQualitative: Quality;

свойствами сущностей, процессами, измеряемыми metaslot in: isQualitative;

end величинами, группами, и др. Фактически глоссарий }, превращается в тезаурус.

{ Coordinate;

metaframe in: metaproperty, measurable;

end Спецификации представительных ресурсов in: type, concept;

обычно описываются в их собственных терминах, а def: {a point on the sky defined in some не в терминах задачи. Таким образом, могут опре coordinate system};

деляться онтологические контексты информацион coordinateOf: AstronomicalObject;

ных ресурсов. Если к ресурсу не применима онтоло metaslot in: coordinateOf;

end гия предметной области задачи, то онтология ресур coordinateSystem: CoordinateSystem;

са может быть создана в результате обратного про epoch: Epoch;

ектирования из концептуальной схемы ресурса с }, использованием документации, спецификаций тре { CoordinateSystem;

бований к ресурсу. Для дальнейшего использования in: type, concept;

ресурса в предметном посреднике необходимо про def: {a method of point location definition};

извести отображение онтологического контекста }, ресурса на онтологию предметной области задачи { EquatorialCoordinateSystem;

[15].

in: type, concept;

def: {celestial coordinate system, including declination and right ascension};

6 Построение концептуальной схемы за supertype: CoordinateSystem;

дачи ra: RightAscension;

Концептуальная схема определяет информаци de: Declination;

онные структуры и правила преобразования инфор }, мации в них при решении задачи. Спецификации { RightAscension;

концептуальной схемы включают определения аб metaframe in: metaproperty, measurable;

end страктных типов данных (АТД) с их структурой, in: type, concept;

ограничениями целостности и методами;

классов def: {one of the two coordinates of the equatorial как множеств однотипных объектов;

функций и coordinate system comparable to longitude, процессов, определяющих поведение системы.

projected onto the celestial sphere};

Используя знания о предметной области из он }, тологии, можно построить концептуальную схему { Declination;

для решения задач данной предметной области.

metaframe in: metaproperty, measurable;

end Данный процесс основан на решениях эксперта, in: type, concept;

которому могут предлагаться варианты предпочти def: {one of the two coordinates of the equatorial тельных трансформаций схемы. Общие принципы coordinate system comparable to latitude, создания концептуальной схемы на основе онтоло projected onto the celestial sphere};

гии следующие:

}, … • на основе определений выбранных понятий В метафреймах спецификаций понятий указы- онтологии создаются прототипы АТД, экс ваются свойства, говорящие о том, что данное поня- перту предлагается создать АТД для понятий, тие описывает сущность или измеримую величину. соответствующих сущностям;

• убираются лишние суперпонятия, их структу Слот in содержит метаклассы, в которые входят данные описания, и говорит о том, что специфика- ра и ограничения перетекают в текущий АТД;

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

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

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

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

для одного типа могут создаваться нием методов извлечения знаний из текстов на ос- несколько классов;

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

• функции над единственным экземпляром in: type;

supertype: Star;

АТД становятся методами данного АТД.

}, Рассмотрим преобразования онтологических по { CoordEQJ2000;

in: type;

нятий в типы концептуальной схемы на примере ra: real;

AstronomicalObject и связанных с ним типов.

de: real;

Типам ProperMotion, Isolation, Quality в онтоло };

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

ными. Атрибуту morphology соответствует тип пе речисления, так как он имеет определённый набор { astronomicalObject;

значений.

in: class;

Тип ColorIndex экспертным решением в схеме instance_section: AstronomicalObject;

преобразуется в функцию, вычисляющую показа }, тель цвета по двум параметрам, соответствующим { star;

связям понятия ColorIndex c двумя полосами про in: class;

пускания. Так как colorIndex работает с одним эк superclass: astronomicalObject;

земпляром типа AstronomicalObject, то функция instance_section: Star;

colorIndex становится методом этого типа.

}, В задаче используется только экваториальная { standard;

система координат в эпохе 2000-го года. В связи с in: class;

этим посредством введения дополнительных огра superclass: star;

ничений на тип Coordinate производится его уточ instance_section: Standard;

нение типом CoordEQJ2000: система координат мо };

жет быть только экваториальная, эпоха только J2000. Таким образом, сами типы Coordinate и В результате операционализации функциональ CoordinateSystem напрямую не используются. Они ных требований схема дополняется функциями и удаляются из схемы, а их спецификации копируют методами, необходимыми при решении задачи. На ся в подтипы CoordEQJ2000. У атрибутов ra и de пример, функция getZeroMotionStars, возвращающая типа EquatorialCoordinateSystem тип значений меня набор звёзд с малым собственным движением. Она ется на скалярный, так как им соответствуют поня станет функцией модуля, так как не связана с одним тия измеряемых величин, из схемы удаляются типы экземпляром какого-либо типа.

RightAscension и Declination. Эксперт ещё упрощает Следует отметить, что определённые в функцио схему, удаляя тип EquatorialCoordinateSystem и пе нальных требованиях пред- и постусловия в процес ренося его атрибуты ra и de непосредственно в тип се их операционализации используются для форми CoordEQJ2000.

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

кации созданных функций. Так в концептуальной in: type;



Pages:     | 1 |   ...   | 7 | 8 || 10 | 11 |   ...   | 26 |
 





 
© 2013 www.libed.ru - «Бесплатная библиотека научно-практических конференций»

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