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

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

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



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






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


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

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

Translation from Event-B into Eiffel

[Перевод моделей Event-B в Eiffel]

S. Reznikova, V. Rivera, J. Y. Lee, M. Mazzara

Innopolis University, 1 Universitetskaya St., Innopolis 420500, Russia

Аннотация: Формальные языки моделирования играют важную роль в разработке программного обеспечения, так как позволяют пользователям, во-первых, определять функциональные требования, которые также служат документацией для проекта, а во-вторых, доказывать корректность свойств систем, что особенно важно для критических систем. Однако не существует четкого понимания того, как сопоставить формальную модель и определенный язык программирования. В качестве решения данной проблемы авторы статьи предлагают использовать возможность source-to-source соответствия между моделями, описанными на языке Event-B (языке моделирования для реактивных приложений и систем), и программами на объектно-ориентированном языке программирования Eiffel. Предложенное решение не только автоматически генерирует соответствующий модели на Event-B код на Eiffel, но также переводит свойства модели в виде контрактов. Контракты соответствуют принципу Design-by-Contract и нативно поддерживаются в Eiffel. Реализация решения доступна как плагин EB2Eiffel в Rodin (среде разработки для Event-B). Таким образом, пользователи могут разрабатывать различные системы, начиная с моделирования функциональных требований (свойств) в Event-B, затем формально доказывая корректность этих свойств в Rodin и, наконец, используя EB2Eiffel для перевода модели на язык программирования. Используя Eiffel, пользователи могут расширять и модифицировать реализацию модели и доказывать корректность измененной модели относительно ее оригинальной, изначально переведенной версии. Также в статье описан процесс тестирования EB2Eiffel разными моделями, написанными на Event-B, и представлены ограничения плагина. Статья публикуется в авторской редакции.

Ключевые слова: пошаговое улучшение систем, Design-by-Contract, формальное моделирование, реактивные приложения, Event-B, Eiffel.

DOI: https://doi.org/10.18255/1818-1015-623-636

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

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

Образец цитирования: S. Reznikova, V. Rivera, J. Y. Lee, M. Mazzara, “Translation from Event-B into Eiffel”, Модел. и анализ информ. систем, 25:6 (2018), 623–636

Цитирование в формате AMSBIB
\RBibitem{RezRivLee18}
\by S.~Reznikova, V.~Rivera, J.~Y.~Lee, M.~Mazzara
\paper Translation from Event-B into Eiffel
\jour Модел. и анализ информ. систем
\yr 2018
\vol 25
\issue 6
\pages 623--636
\mathnet{http://mi.mathnet.ru/mais653}
\crossref{https://doi.org/10.18255/1818-1015-623-636}


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

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