Методы специализации онтологии процессов, ориентированной на верификацию

Удобная для пользователя формальная спецификация и верификация параллельных и распределённых систем, принадлежащих различным предметным областям, таким как системы автоматического управления, телекоммуникации, бизнес-процессы, являются активными темами исследований в силу их практической значимости. В этой статье мы представляем методы разработки специализированных ориентированных на верификацию онтологий процессов, которые используются для описания параллельных и распределенных систем предметных областей. Одним из преимуществ таких онтологий является их формальная семантика, которая делает возможной формальную верификацию описанных систем. Наш метод основан на абстрактной онтологии процессов, ориентированной на верификацию. Мы используем два метода специализации абстрактной онтологии процессов. Декларативный метод с помощью специализации классов исходной онтологии, введения новых декларативных классов, а также системы аксиом задаёт ограничения для классов и отношений абстрактной онтологии. Конструктивный метод использует техники семантической разметки и сопоставления с образцом, чтобы связать понятия предметной области с классами абстрактной онтологии процессов. Мы даём подробные онтологические спецификации этих техник. Наши методы сохраняют формальную семантику исходной онтологии процессов и, следовательно, возможность применения формальных методов верификации к специализированным онтологиям процессов. Мы показываем, что конструктивный метод является уточнением декларативного метода. Построение онтологии типовых элементов систем автоматического управления иллюстрирует наши методы: разработано декларативное описание классов и ограничений специализированной онтологии в системе Protégé на языке OWL с использованием правил вывода на языке SWRL и построена система шаблонов семантической разметки, которая реализует типовые элементы систем автоматического управления.