Автоматизація аналізу несуперечності в задачах верифікації при проектуванні автоматизованих системах обробки інформації
| dc.contributor.author | Сирота, Олена Петрівна | |
| dc.contributor.degreefaculty | Науково-дослідний інститут системних технологій | |
| dc.contributor.degreegrantor | Національний технічний університет України "Київський політехнічний інститут" | |
| dc.date.accessioned | 2010-04-26T12:35:20Z | |
| dc.date.available | 2010-04-26T12:35:20Z | |
| dc.date.created | 2009 | en |
| dc.date.issued | 2009 | |
| dc.description | Дисертація на здобуття наукового ступеня кандидата технічних наук за спеціальністю 05.13.06 – інформаційні технології. – Національний технічний університет України «Київський політехнічний інститут», Київ, 2009. Дисертація присвячена розв’язанню задачі аналізу несуперечності АСОІ та бізнес-правил при проектуванні АСОІ для підходу до створення АСОІ із декларативним поданням бізнес-правил. В роботі запропоновано концепцію структурної верифікації при проектуванні АСОІ, яка полягає у розширенні процесу верифікації етапом аналізу несуперечності проекту АСОІ та бізнес-правил. Як модель АСОІ застосовано UML, для формалізації бізнес-правил застосовано SBVR. Задачу дослідження розв’язано шляхом аналізу несуперечності інтегральної моделі АСОІ та бізнес-правил. Розроблено математичну інтегральну модель АСОІ та бізнес-правил на базі моделей UML та SBVR, яка об’єднує компоненти, подані у різних формалізмах, та є мульти-формальною. Встановлено властивості використовуваних формалізмів, зокрема, для логіки предикатів виявлено, що застосовуються розв’язні фрагменти та класи. Це забезпечує розв’язність задачі виконуваності формул логіки предикатів. Для побудови визначеного класу інтегральних моделей та аналізу їх несуперечності розроблено метод подання знань. Розроблено математичний метод аналізу несуперечності АСОІ та бізнес-правил, встановлено оцінку його складності. На основі теоретичних результатів розроблено інформаційну технологію, апробовану при створенні та реінжинірингу ряду АСОІ. | |
| dc.description | Диссертация на соискание научной степени кандидата технических наук по специальности 05.13.06 – информационные технологии. – Национальный технический университет Украины «Киевский политехнический институт», Киев, 2009. Диссертация посвящена решению задачи анализа непротиворечивости АСОИ и бизнес-правил при проектировании АСОИ. Исследованы процессы верификации при проектировании АСОИ и обнаружены недостатки в методах анализа непротиворечивости системы для подхода к созданию АСОИ с декларативным представлением бизнес-правил. Выявлено, что для анализа непротиворечивости используется только информация о существующей модели системы, без привлечения внешней информации о бизнес-правилах. Предложена концепция структурной верификации, которая состоит в расширении процесса верификации при проектировании этапом анализа непротиворечивости структурных моделей системы и бизнес-правил. Как модель АСОИ применена UML, как модель бизнес-правил – SBVR. Задача структурной верификации решается на основе анализа непротиворечивости интегральной модели, созданной путем объединения и дополнительной обработки моделей UML и SBVR. Определена математическая мульти-формальная интегральная модель на базе моделей UML и SBVR. Для решения задачи анализа непротиворечивости интегральной модели разработан комплекс методов и алгоритмов, основанный на мульти-формальном моделировании и математической логике, который включает в себя: методы приведения компонентов интегральной модели к единой формально-логической базе – теории множеств и многосортной логике первого порядка; критерии и методы анализа непротиворечивости интегральной модели и ее компонентов. Исследованы свойства формализмов, используемых для построения мульти-формальной интегральной модели. В частности, для логики предикатов установлено, что используются разрешимые фрагменты и классы, что обеспечивает разрешимость задачи анализа непротиворечивости и выполнимости формул логики предикатов. Разработана модель представления знаний (CP-модель), в основе которой лежит семантическая сеть, расширенная функциями синтаксического и семантического контроля и правилами вывода новых связей. Отличительной особенностью модели является то, что она обеспечивает средства для представления в виде семантической сети других формализмов – множеств, формул логики предикатов, объектных моделей. Представление знаний используется для построения мульти-формальных моделей и анализа их непротиворечивости. Применение CP-модели позволяет построить мульти-формальную интегральную модель АСОИ и бизнес-правил и проанализировать ее непротиворечивость. Разработан математический метод анализа непротиворечивости АСОИ и бизнес-правил путем построения интегральной модели средствами предложенного метода представления знаний. Метод предусматривает объединение моделей АСОИ и бизнес-правил в мульти-формальную интегральную модель, приведение компонентов интегральной модели к теории множеств и многосортной логике первого порядка, проверке, удовлетворяют ли элементы и выражения теории множеств комплексной системе правил, и проверке выполнимости формул многосортной логики путем применения модифицированного для этой логики метода построения множества Хинтикки. Комплексная система правил для теории множеств включает в себя аксиомы Цермело-Френкеля и другие правила, которые гарантируют возможность построения алгебраической системы. Рассчитана оценка сложности метода, которая является экспоненциальной. На основе предложенных методов и моделей разработаны инструментальный комплекс и методика автоматизации структурной верификации, которые апробированы в процессе создания и реинжиниринга ряда АСОИ. Благодаря внедрению разработанной технологии было улучшено качество систем путем уменьшения количества ошибок на стадиях анализа и проектирования. Также был достигнут экономический эффект, который состоит в экономии средств при реализации АСОИ | |
| dc.description | The dissertation is devoted to solving the task of consistency analysis of information systems and business rules at the system design stage for business rules approach. The conception of structural verification at design stage is proposed. The conception is to extend verification process at design stage with the phase of consistency analysis of information system and business rules. UML is used for information system modeling; SBVR is used for business rules formalization. Research task is solved by means of consistency analysis of system and business rules integral model. The mathematical multi-formal integral model is developed which unite components represented in different formalisms. The properties of used formalisms are determined. In particular it is established for first order logic that decidable fragments and classes are used. This ensures the decidability of satisfiability problem for the first order logic formulas. For building and consistency analysis of specified integral models the knowledge representation method is developed. The consistency analysis method of information systems and business rules is developed and its computational complexity is determined. The information technology based on theoretical results is developed. The technology is tested at development and reengineering of the number of information systems | |
| dc.identifier.uri | https://ela.kpi.ua/handle/123456789/321 | |
| dc.language.iso | uk | en |
| dc.title | Автоматизація аналізу несуперечності в задачах верифікації при проектуванні автоматизованих системах обробки інформації | en |
| dc.type | Thesis | |
| thesis.degree.discipline | кафедра технічної кібернетики | |
| thesis.degree.level | дисертація кандидата технічних наук | |
| thesis.degree.name | кандидат технічних наук | |
| thesis.degree.speciality | 05.13.06 – інформаційні технології |