Rodin — платформа для разработки и верификации моделей на Event-B (Илья Щепетков, OSSDEVCONF-2014) — различия между версиями
Материал из 0x1.tv
StasFomin (обсуждение | вклад) |
StasFomin (обсуждение | вклад) (Batch edit: replace PCRE (\n\n)+(\n) with \2) |
||
(не показано 16 промежуточных версий этого же участника) | |||
== Видео == {{vimeoembed|106435742|800|450}} {{youtubelink|wFP9HKAX8LU}}{{letscomment}} <!-- pollholder --> == Слайды == == Примечания и отзывы == <!-- <blockquote>[©]</blockquote> --> <references/> [[Category:OSSDEVCONF-2014]] [[Category:Open-source projects]] [[Category:Верификация]] <!-- topub --> {{stats|disqus_comments=0|refresh_time=2018-10-19T21:44:122021-08-31T16:35:19.242764520585|vimeo_comments=0|vimeo_plays=2156|youtube_comments=0|youtube_plays=107}}232}} |
Текущая версия на 12:19, 4 сентября 2021
Аннотация
- Докладчик
- Илья Щепетков
При проектировании и анализе сложных систем часто возникает потребность в описании моделей этих систем. Одним из подходов для решения этой задачи является использование формального метода Event-B. В докладе рассказывается о свободной платформе Rodin, которая предоставляет среду для разработки, анализа и верификации моделей на Event-B.
Видео
Посмотрели доклад? Понравился? Напишите комментарий! Не согласны? Тем более напишите.
Слайды
Расширенные тезисы
Критичные по безопасности системы, ошибки в которых могут привести к гибели или травмам людей, крупным финансовым потерям и ущербу окружающей среды, имеют повышенные требования к своей корректности. Один из способов повышения уверенности в корректности заключается в моделировании системы и требований к ней и доказательстве их непротиворечия с использованием формальных методов.
Существуют различные формальные методы, многие из которых были использованы в большом количестве проектов индустриального уровня. Одним из наиболее активно развивающихся и используемых является Event-B. Средства для разработки, анализа и верификации моделей на Event-B предоставляются свободной платформой Rodin — она содержит текстовый редактор моделей, набор систем автоматического доказательства, поддержку интерактивного доказательства.
Функционал платформы может быть расширен за счет использования плагинов. Доступны плагины, позволяющие писать собственные расширения формального метода Event-B, дополнительные системы автоматического доказательства, инструменты для анимации и model checking, и т. д.
Наш опыт использования Rodin состоит в формализации и доказательстве корректности модели управления правами доступа и информационным потоками операционной системы специального назначения Astra Linux Special Edition.
Модель была полностью формализована и верифицирована, что позволило обнаружить и исправить ряд неточностей в её изначальном текстовом описании.
В результате мы можем сказать, что применение формальных методов даёт следующие преимущества:
- нахождение ошибок, которые иначе не были бы найдены;
- повышение уверенности в корректности системы;
- решение задачи сопровождения системы при последующих правках и расширениях в её описании.
Однако, при использовании Rodin мы столкнулись и с трудностями. Следует отметить
- высокий уровень трудозатрат на проведение формальной верификации;
- ограниченную поддержку Rodin командной разработки;
- отсутствие поддержки выделения часто используемых выражений в отдельные сущности с последующим доступом к ним по ссылке.
Платформа Rodin это совместный проект различных команд. Наибольший вклад в разработку вносят Саутгемптонский университет, компания Systerel и Дюссельдорфский университет.
В результате мы имеем свободный инструмент, не уступающий коммерческим аналогам, а также успешно используемый для повышения качества критичных по безопасности систем.
Примечания и отзывы
Plays:288 Comments:0