Інтелектуальні методи синтезу семантичних моделей програм - Автореферат

Серед важливих результатів цього напрямку досліджень слід зазначити: створення консорціумом OMG методології «розробки ПЗ, що керується моделлю», створення стандартів високорівневого моделювання та документування програм, таких як UML, BPMN та ін.; розвиток дослідницьких концепцій «фабрик ПЗ» та «корпоративної памяті»; створення мов формальної специфікації програм, таких як Object-Z, Event-B, та заснованих на них методів верифікації формалізованих моделей програм на основі класичних та нестандартних (наприклад, темпоральних) логік, методів автоматичного доведення теорем, методів моделювання поведінки моделей програм на основі абстрактних машин, онтологічної моделі подання знань в інтелектуальних системах. У звязку з цим досить актуальною є задача розробки семантичних моделей програм, а також інтелектуальних методів їх синтезу та верифікації, що можуть бути використані для створення інтелектуальних фабрик програм, систем розробки та тестування програм на основі їх семантичних моделей, баз знань, що шляхом навчання накопичують рекомендації з синтезу моделей програм та у подальшому дозволять автоматизувати цей процес. Дисертаційна робота виконувалася у Харківському національному університеті радіоелектроніки на кафедрі програмного забезпечення ЕОМ відповідно до плану НДР університету в межах розділу № 200-5 «Розробка моделей та методів для забезпечення внутрішнього моніторингу якості підготовки фахівців у Харківському національному університеті радіоелектроніки» д/б теми №200 «Методи та технології створення інформаційно-освітнього середовища з метою інтеграції у загальноєвропейський простір вищої освіти» (№ ДР0106U003152, акт впровадження від 07.10.2008 р.), в якій здобувач О.Л. Методи дослідження ґрунтуються на комплексному використанні теорій синтаксичного та семантичного аналізу формальних мов, методів логічного виводу у формальних системах, методів розвязання задач задоволення обмежень, на базі яких розроблено методи синтезу та верифікації семантичних моделей програм; методів машинного навчання, на базі яких синтезовано метод навчання систем логічного виводу на основі прецедентів; методів подання знань в інтелектуальних системах та концепції Semantic Web, які дозволили створити семантичні моделі програм та структуру онтології системи синтезу моделей програм. 2) набула подальшого розвитку модель, що формалізує семантику компютерних програм, яка відрізняється від існуючих урахуванням семантичних анотацій, що задають призначення анотованих елементів моделі, вимоги до їх поведінки та рекомендації про використання анотованих елементів у різних контекстах, що дало можливість синтезувати запропоновані семантичні моделі програм на основі анотацій їх елементів та проводити верифікацію їх здійсненності;У вступі обґрунтовано актуальність дисертаційної роботи, сформульовано основну мету і задачі дослідження, наведено відомості щодо наукової новизни отриманих у дисертації результатів, визначено їх практичну цінність, наведено відомості про апробацію та впровадження результатів. Серед досліджуваних парадигм програмування виділено як найбільш перспективну методологію «розробки програм, керовану моделлю» (MDD), яка розглядає розробку програми, як процес поетапного синтезу її моделей від високорівневої моделі до програмного коду. Проаналізовано існуючі формальні моделі специфікації програм (Object-Z, Event-B), методи їх синтезу (індуктивний, дедуктивний та трансформаційний, «фабрики ПЗ») та верифікації (синтаксичний аналіз на основі формальних граматик для мов з текстовим та графовим синтаксисом, доведення proof obligations і т. ін.). Розроблена модель (1) формалізує опис структурних та поведінкових елементів моделей програм за допомогою семантичних анотацій: SPM={m | m={e | e= \/ e=}},(1) де m - семантично анотоване подання розроблюваної програми у вигляді однієї із створених на основі стандарту UML діаграм взаємодії агентів предметної галузі (DAC), діаграм бізнес-обєктів у межах кожного агента (BOD), діаграм класів (CD), що уточнюють BOD-діаграми, діаграм процесів (PD), що детально описують процеси, які призначена виконувати програма, та діаграм інтерфейсу користувача (UI); e - смисловий або єднальний елемент відповідної діаграми m.У дисертаційній роботі наведено результати, які відповідно до поставленої мети є розвязанням актуальної задачі розробки інтелектуальних методів синтезу та верифікації семантичних моделей програм, що дозволяють підвищити ефективність розробки програмного забезпечення. Метод полягає у семантичному анотуванні елементів, що підлягають синтезу, та пошуку уточнюючих їх компонентів шляхом логічного виводу на основі прецедентів у онтології анотованих елементів моделей програм. Набула подальшого розвитку модель, яка формалізує семантику компютерних програм на основі анотацій, що задають призначення анотованих елементів моделі, вимоги до їх поведінки та рекомендації про використання анотованих елементів у різних контекстах. Багатокомпонентна модель дозволяє задавати формальну мову декількома підмоделями

Основний зміст роботи