Панельная секция 10 лет Центра верификации ОС Linux. Верификация реального ПО – мечта или реальность? (SECR-2015) — различия между версиями
Материал из 0x1.tv
StasFomin (обсуждение | вклад) |
StasFomin (обсуждение | вклад) (→Аннотация) |
||
== Аннотация == ;Модератор: * {{Speaker|Александр Петренко}} ;Докладчики: * {{Speaker|Виктор Иванников}} * {{Speaker|Дмитрий Завалишин}} * {{Speaker|Михаил Мериин}} * {{Speaker|Александр Оружейников}} * {{Speaker|Борис Позин}} * {{Speaker|Владимир Рубанов}} * {{Speaker|Григорий Сенин}} * {{Speaker|Алексей Хорошилов}} <blockquote> В сентябре 2005 года в рамках государственного контракта с Минобрнауки РФ в Институте системного программирования РАН был создан Центр верификации ОС Linux , который был впоследствии поддержан международным консорциумом Linux Foundation и рядом индустриальных партнеров. Центр продолжает активно работать уже десять лет. Строгий подход к верификации, развиваемый Центром, базируется на использовании формальных спецификаций требований и формальных методов анализа программ. Центр разрабатывает собственные и развивает open source инструменты верификации с использованием современных методов тестирования на основе формальных моделей, верификации моделей, дедуктивной верификации кода, современных средств доказательства теорем и решателей логических уравнений. Эти инструменты применяются для верификации ядра и библиотек ОС Linux, отечественных операционных систем реального времени и микропроцессоров, что демонстрирует их зрелость даже в контексте промышленного использования. Вместе с тем, хотя потенциальный выигрыш от использования сложных методов тестирования и формальных методов разработки и верификации очевиден – существенный рост надежности программных систем и дополнительные преимущества в конкуренции на рынке ПО, за рубежом практика использования таких методов пока еще не имеет широкого распространения, а в России встречается исключительно редко. Каковы причины такого положения дел? Что мешает применению новых технологий? Если нет универсальных технологий верификации, то как выбирать эффективный набор технологий в контексте конкретной практической задачи? – Эти вопросы будут обсуждаться в дискуссии, в которой примут участие представители академического сообщества и промышленности. </blockquote> == Видео == {{vimeoembed|143683332|800|450}} <!-- {{youtubelink|}} --> == Слайды == [[File:Панельная секция 10 лет Центра верификации ОС Linux. Верификация реального ПО – мечта или реальность? (SECR-2015).pdf|left|page=-|256px]] {{----}} == Примечания и отзывы == <!-- <blockquote>[©]</blockquote> --> * [http://2015.secr.ru/program/discussions/isp-ras-linux-verification-center Страница доклада на сайте конференции] <references/> [[Category:SECR-2015]] <!-- --> |
Версия 00:30, 23 ноября 2015
Содержание
Аннотация
- Модератор
- Докладчики
- Виктор Иванников
- Дмитрий Завалишин
- Михаил Мериин
- Александр Оружейников
- Борис Позин
- Владимир Рубанов
- Григорий Сенин
- Алексей Хорошилов
В сентябре 2005 года в рамках государственного контракта с Минобрнауки РФ в Институте системного программирования РАН был создан Центр верификации ОС Linux , который был впоследствии поддержан международным консорциумом Linux Foundation и рядом индустриальных партнеров. Центр продолжает активно работать уже десять лет.
Строгий подход к верификации, развиваемый Центром, базируется на использовании формальных спецификаций требований и формальных методов анализа программ. Центр разрабатывает собственные и развивает open source инструменты верификации с использованием современных методов тестирования на основе формальных моделей, верификации моделей, дедуктивной верификации кода, современных средств доказательства теорем и решателей логических уравнений.
Эти инструменты применяются для верификации ядра и библиотек ОС Linux, отечественных операционных систем реального времени и микропроцессоров, что демонстрирует их зрелость даже в контексте промышленного использования. Вместе с тем, хотя потенциальный выигрыш от использования сложных методов тестирования и формальных методов разработки и верификации очевиден – существенный рост надежности программных систем и дополнительные преимущества в конкуренции на рынке ПО, за рубежом практика использования таких методов пока еще не имеет широкого распространения, а в России встречается исключительно редко.
Каковы причины такого положения дел? Что мешает применению новых технологий? Если нет универсальных технологий верификации, то как выбирать эффективный набор технологий в контексте конкретной практической задачи? – Эти вопросы будут обсуждаться в дискуссии, в которой примут участие представители академического сообщества и промышленности.
Видео
Слайды
Примечания и отзывы