RUS  ENG ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ЛИЧНЫЙ КАБИНЕТ
Общая информация
Последний выпуск
Архив
Импакт-фактор

Поиск публикаций
Поиск ссылок

RSS
Последний выпуск
Текущие выпуски
Архивные выпуски
Что такое RSS



Модел. и анализ информ. систем:
Год:
Том:
Выпуск:
Страница:
Найти






Персональный вход:
Логин:
Пароль:
Запомнить пароль
Войти
Забыли пароль?
Регистрация


Модел. и анализ информ. систем, 2018, том 25, номер 6, страницы 607–622 (Mi mais652)  

Семантика, спецификация и верификация программ

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

Н. О. Гаранина, И. С. Ануреев, О. И. Боровикова

Институт систем информатики имени А.П. Ершова СО РАН, пр. акад. Лаврентьева, 6, г. Новосибирск, 630090 Россия

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

Ключевые слова: онтология, верификация, проверка моделей, процессы.

Финансовая поддержка Номер гранта
Российский фонд фундаментальных исследований 17-07-01600_а
Работа поддержана грантом РФФИ 17-07-01600.


DOI: https://doi.org/10.18255/1818-1015-607-622

Полный текст: PDF файл (831 kB)
Список литературы: PDF файл   HTML файл

Тип публикации: Статья
УДК: 004.052, 519.179.2
Поступила в редакцию: 20.07.2018
Исправленный вариант: 10.10.2018

Образец цитирования: Н. О. Гаранина, И. С. Ануреев, О. И. Боровикова, “Онтология процессов, ориентированная на верификацию”, Модел. и анализ информ. систем, 25:6 (2018), 607–622

Цитирование в формате AMSBIB
\RBibitem{GarAnuBor18}
\by Н.~О.~Гаранина, И.~С.~Ануреев, О.~И.~Боровикова
\paper Онтология процессов, ориентированная на верификацию
\jour Модел. и анализ информ. систем
\yr 2018
\vol 25
\issue 6
\pages 607--622
\mathnet{http://mi.mathnet.ru/mais652}
\crossref{https://doi.org/10.18255/1818-1015-607-622}


Образцы ссылок на эту страницу:
  • http://mi.mathnet.ru/mais652
  • http://mi.mathnet.ru/rus/mais/v25/i6/p607

    ОТПРАВИТЬ: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru


    Citing articles on Google Scholar: Russian citations, English citations
    Related articles on Google Scholar: Russian articles, English articles
  • Моделирование и анализ информационных систем
    Просмотров:
    Эта страница:7
    Полный текст:2
    Литература:1

     
    Обратная связь:
     Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2019