Онтология процессов, ориентированная на верификацию

В статье представлена онтология процессов, близких взаимодействующим последовательным процессам Хоара. Она является частью интеллектуальной системы поддержки верификации свойств поведения таких процессов. Наше онтологическое представление процессов ориентировано как на применение формальных методов верификации, так и на извлечение информации из технической документации (с помощью нашей ранее разработанной системы извлечения информации из текстов на естественном языке). Мы описываем классы и домены онтологии, которые определяют взаимодействующие процессы. Эти процессы характеризуются множествами локальных и разделяемых переменных, списком действий над этими переменными, которые изменяют их значения, списком каналов взаимодействия процессов (которые, в свою очередь, характеризуются типом чтения сообщений, емкостью, способами записи и считывания, а также надежностью), списком коммуникационных действий для отправки сообщений. Помимо формального математического определения классов и доменов онтологии, приведены примеры описаний некоторых онтологических классов, а также типовых свойств и аксиом для них в редакторе Protǵн́а языке OWL с использованием правил вывода на языке SWRL. Для онтологического представления взаимодействующих процессов определяется их формальная операционная семантика, которая задается с использованием помеченной системы переходов. В интерливинговой модели она сводится к локальной операционной семантике отдельных экземпляров процессов. Представлена специализация онтологии для некоторых типов процессов из предметной области систем автоматического управления, моделирующих типовые функциональные элементы системы автоматического управления (датчики, сравнивающие устройства и регулирующие устройства), а также их комбинации. Понятия специализированной онтологии иллюстрируются на примере управляющей части системы розлива бутылок.