Обчислювальні методи верифікації темпоральних обмежень цілісності в процесі управління змінами в онтологіях - Автореферат

Структура та номенклатура знань про продукцію та процеси у ІСП ТПВ зазнає змін з часом, тому ІСП ТПВ включає в себе процес накопичення та уточнення моделей знань про ТПВ. Метою цього процесу є забезпечення переходу від попередніх до наступної (уточненої) версії моделі таким чином, щоб забезпечити її якість за наступними контрольованими признаками: внутрішня несуперечливість уточненої моделі; її несуперечливість відносно до інших моделей, використаних в ІСП; коректність уточненої моделі відносно набору вимог, обумовлених поточними особливостями ТПВ. Водночас, складність моделей знань про процеси ТПВ з урахуванням їх динамізму призводить до цілого комплексу проблем перевірки несуперечливості відповідних ІСП. Урахування динаміки предметної області та подання динамічних предметних областей у онтологіях, а також їх формально-мовна підтримка розглядалися А. На основі виконаних теоретичних досліджень та проведених експериментів отримано нове рішення важливої наукової задачі - удосконалення засобів перевірки якості онтологій при модифікації шляхом проведення формальної верифікації темпоральних обмежень цілісності в термінах запропонованого формально-логічного апарата моделювання, призначеного для використання у процесі управління змінами в онтологіях, що дозволяє підвищити ефективність процесу технічної підготовки виробництва за рахунок зменшення кількості помилок при модифікації онтологій.Проведений аналіз існуючих підходів до управління змінами в онтологіях показав, що вони залишають відкритими цілий ряд питань: відсутність формальних засобів подання обмежень цілісності, обумовлених предметною областю, що призводить до помилок реалізації модифікацій інженерами знань; відсутність формальних методів верифікації заданих обмежень цілісності, що призводить до виконання семантично некоректних або зайвих модифікацій та їх розповсюдження на залежні елементи інформаційної системи. Аналіз дозволив визначити наступні вимоги до засобів управління змінами в онтологіях: використання декларативних засобів для подання обмежень цілісності, обумовлених предметною областю; забезпечення можливості оперувати при поданні обмежень цілісності різними версіями моделі онтології; залучення формальних методів перевірки коректності моделей онтологій відносно заданих обмежень. Динамічна предметна область - це предметна область, що зазнає зміни з часом. Для моделювання динамічної предметної області у інформаційній системі в роботі розглядаються тільки дискретні темпоральні структури, з урахуванням припущення, що зміна у предметній області не має тривалості і відбувається миттєво. Множина правильно побудованих формул вичерпується такими формулами: всі пропозиційні змінні; якщо і - формули, то , , , , є формулами PTC(MT); якщо «= » - предикатна буква, якій відповідає бінарний предикат рівності, заданий над цілими числами, і - терми, то є формулою; якщо - формула, то , , , , - також є формулами PTC(MT).У дисертації отримано нові науково обґрунтовані результати в області математичного моделювання та обчислювальних методів, що в сукупності вирішують важливу наукову задачу - удосконалення засобів перевірки якості онтологій при модифікації шляхом проведення формальної верифікації темпоральних обмежень цілісності в термінах запропонованого формально-логічного апарата моделювання, призначеного для використання на етапі специфікації модифікацій в онтологіях, що дозволяє підвищити ефективність процесу технічної підготовки виробництва за рахунок зменшення кількості помилок при модифікації онтологій. З урахуванням даних вимог проведено аналіз існуючих моделей процесу управління змінами в онтологіях, який показав, що вони не можуть повною мірою вирішувати задачі, які виникають на етапі специфікації модифікацій. Показано, що для підвищення ефективності ТПВ необхідно розробити формальний апарат моделювання динамічних предметних областей, призначений для побудови і верифікації обмежень цілісності, що мають виконуватися в процесі управління змінами в онтологіях. Запропоновано нову формальну модель онтології динамічної предметної області. Для задач управління змінами в онтологіях запропоновано використовувати дискретну лінійну в майбутнє і в минуле темпоральну структуру, в якій кожен момент часу відповідає новій версії онтології.

2. ОСНОВНИЙ ЗМІСТ РОБОТИ