Новые методы решения задач извлечения и анализа процессов и их применение для проектирования информационных систем

Цель работы: разработка новых методов проверки эквивалентности и верификации автоматных моделей программ с различными расширениями, а также новых подходов к моделированию поведения информационных систем, визуализации моделей процессов, проверке соответствия наблюдаемому поведению процессов, которое регистрируется в журналах событий. При работе над новыми методами проверки эквивалентности и верификации автоматных моделей применяется теория формальных грамматик, конечных автоматов-преобразователей и логики деревьев вычислений. При работе над новыми подходами к моделированию процессов и проверке его соответствия используется аппарат теории формальных языков, сетей Петри и их расширений. Эмпирическую базу составляют конкретные примеры распределенных систем, а также журналы событий, в которых записываются данные обо всех произошедших действиях. Результаты работы: предложен новый метод эффективной проверки эквивалентности некоторых классов конечных автоматов, которые демонстрируют детерминированное поведение. На основании этого метода также построен алгоритм проверки эквивалентности для детерминированных магазинных автоматов с одним состоянием. Разработан алгоритм верификации конечных автоматов-преобразователей для расширения логики деревьев вычислений Reg-CTL*, в которой введена параметризация темпоральных операторов. Разработана система локальных преобразований моделей элементарных сетевых систем для выполнения пошагового моделирования поведения комплексных информационных систем. Рассмотрено применение предложенных преобразований для построения корректной системы взаимодействующих сетей потоков работ. Предложен метод визуализации моделей высокоуровневых сетей Петри, который учитывает их внутреннюю иерархическую структуру, а также динамику поведения на основе данных из журналов событий. Представлен программный инструмент VTMine for Visio, который поддерживает графическое моделирование и автоматизацию экспериментов, проводимых в области исследования методов обработки данных о наблюдаемом поведении информационных систем из журналов событий. Предложены методы проверки соответствия поведения моделей расширенных сетей Петри – раскрашенных и вложенных сетей Петри – информации о реальном поведении из журналов событий мультиагентных систем специального вида. Проведен анализ возможностей и ограничений применимости различных классов сетей Петри для моделирования поведения информационных систем поддержки биржевой торговли. На основании проведенного анализа предложена схема расширения сетей Петри, которое позволяет целостно охватить все аспекты поведения систем с несколькими взаимодействующими компонентами, которые оперируют с общедоступными данными. Представлен программный инструмент, который поддерживает моделирование и симуляцию поведения расширения сетей Петри, в рамках которого допускается работа с персистентными данными. Предложенные теоретические методы анализа и верификации автоматных моделей информационных систем и программ ориентированы на возможность их практической реализации. Разработанные методы моделирования, визуализации и проверки соответствия поведения информационных систем с применением информации из их журналов событий прошли проверку на реальных примерах журналов событий информационных систем.