Сирота О. П. Автоматизація аналізу несуперечності в задачах верифікації при проектуванні автоматизованих систем обробки інформації

Дисертація присвячена розв'язанню задачі аналізу несуперечності АСОІ та бізнес-правил при проектуванні АСОІ для підходу до створення АСОІ із декларативним поданням бізнес-правил. Запропоновано концепцію структурної верифікації при проектуванні АСОІ, яка полягає у розширенні процесу верифікації етапом аналізу несуперечності проекту АСОІ та бізнес-правил. Як модель АСОІ застосовано UML, для формалізації бізнес-правил застосовано SBVR. Задачу дослідження розв'язано шляхом аналізу несуперечності інтегральної моделі АСОІ та бізнес-правил. Розроблено математичну інтегральну модель АСОІ та бізнес-правил на базі моделей UML та SBVR, яка є мульт-формальною. Встановлено властивості використовуваних формалізмів, зокрема, для логіки предикатів виявлено, що застосовуються розв'язні фрагменти та класи. Для побудови визначеного класу інтегральних моделей та аналізу їх несуперечності розроблено метод подання знань. Розроблено математичний метод аналізу несуперечності АСОІ та бізнес-правил, встановлено оцінку його складності. На основі теоретичних результатів розроблено інформаційну технологію, апробовану при створенні та реінжинірингу ряду АСОІ.