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

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

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



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






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


Модел. и анализ информ. систем, 2018, том 25, номер 5, страницы 465–480 (Mi mais642)  

Верификация программ

A control flow graph based approach to make the verification of cyber-physical systems using KeYmaera easier

[Упрощение процесса верификации кибер-физических систем с использованием подхода с графом потока управления в средстве KeYmaera]

T. Baara, S. Staroletovb

a Hochschule für Technik und Wirtschaft Berlin University of Applied Sciences, Germany 75 A Wilhelminenhofstrasse, D-12459, Berlin, Germany
b Polzunov Altai State Technical University, 46 Lenina avenue, Barnaul, Altai region, 656038 Russian Federation

Аннотация: KeYmaera является средством интерактивного доказательства теорем и используется для проверки свойств безопасности кибер-физических систем (CPS). Проверка таких свойств в интерактивном режиме может быть осложнена, поскольку доказательство осуществляется с использованием классического секвентного логического исчисления и успешное доказательство требует от пользователя глубоких знаний о доступных правилах, имеющихся в логике исчисления. Еще одним препятствием для широкого применения KeYmaera является представление текущих целей только в виде текста, что предполагает хорошую подготовку пользователя для построения успешных доказательств. В этой статье мы представляем альтернативный метод верификации для KeYmaera, который значительно повышает удобство использования и минимизирует работу пользователей. Основная идея заключается в том, чтобы позволить пользователю добавлять аннотации в виде инвариантов и контрактов к состояниям гибридной программы. В нашем подходе пользователь может использовать графический язык представления моделируемой системы, что позволяет ему не работать с чисто текстовым форматом гибридных программ, являющимся входным для средства KeYmaera. Исходя из предоставленных пользователем контрактов, можно получать доказательства, которые гораздо проще, чем исходная цель доказательств в KeYmaera, и которые могут быть обработаны в большинстве случаев полностью автоматически. Статья публикуется в авторской редакции.

Ключевые слова: кибер-физические системы, KeYmaera, контракты, верификация, гибридные системы, интерактивные доказатели теорем

DOI: https://doi.org/10.18255/1818-1015-465-480

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

Тип публикации: Статья
УДК: 004.942
Поступила в редакцию: 10.09.2018
Язык публикации: английский

Образец цитирования: T. Baar, S. Staroletov, “A control flow graph based approach to make the verification of cyber-physical systems using KeYmaera easier”, Модел. и анализ информ. систем, 25:5 (2018), 465–480

Цитирование в формате AMSBIB
\RBibitem{BaaSta18}
\by T.~Baar, S.~Staroletov
\paper A control flow graph based approach to make the~verification of cyber-physical systems using~KeYmaera easier
\jour Модел. и анализ информ. систем
\yr 2018
\vol 25
\issue 5
\pages 465--480
\mathnet{http://mi.mathnet.ru/mais642}
\crossref{https://doi.org/10.18255/1818-1015-465-480}


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

    ОТПРАВИТЬ: 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
  • Моделирование и анализ информационных систем
    Просмотров:
    Эта страница:54
    Полный текст:19
    Литература:10
     
    Обратная связь:
     Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2019