English
В сентябре 2005 года в рамках государственного контракта с Минобрнауки РФ в Институте системного программирования РАН был создан Центр верификации ОС Linux , который был впоследствии поддержан международным консорциумом Linux Foundation и рядом индустриальных партнеров. Центр продолжает активно работать уже десять лет.
Строгий подход к верификации, развиваемый Центром, базируется на использовании формальных спецификаций требований и формальных методов анализа программ. Центр разрабатывает собственные и развивает open source инструменты верификации с использованием современных методов тестирования на основе формальных моделей, верификации моделей, дедуктивной верификации кода, современных средств доказательства теорем и решателей логических уравнений.
Эти инструменты применяются для верификации ядра и библиотек ОС Linux, отечественных операционных систем реального времени и микропроцессоров, что демонстрирует их зрелость даже в контексте промышленного использования. Вместе с тем, хотя потенциальный выигрыш от использования сложных методов тестирования и формальных методов разработки и верификации очевиден – существенный рост надежности программных систем и дополнительные преимущества в конкуренции на рынке ПО, за рубежом практика использования таких методов пока еще не имеет широкого распространения, а в России встречается исключительно редко.
Каковы причины такого положения дел? Что мешает применению новых технологий? Если нет универсальных технологий верификации, то как выбирать эффективный набор технологий в контексте конкретной практической задачи? – Эти вопросы будут обсуждаться в дискуссии, в которой примут участие представители академического сообщества и промышленности.
Модератор
Александр Петренко
Заведующий отделом Технологий программирования, ИСП РАН
Научный руководитель Центра
Панелисты
Виктор Иванников
Научный руководитель, ИСП РАН
Академик Виктор Петрович Иванников – Основатель Центра.
Дмитрий Завалишин
Генеральный директор, группа ИТ-компаний DZ Systems
Принимал активное участие в создании российских сегментов сетей Интернет (Релком) и Фидонет, в частности, обеспечил прозрачное взаимодействие между ними. С 1997 года по 2002 год издавал онлайн-журнал dz online. С 2000 по 2004 год отвечал за проектирование, разработку и развитие портала компании Яндекс. Один из ключевых создателей сервиса Яндекс.Маркет. В 2006 году Дмитрий основал компанию Digital Zone.
Михаил Мериин
Руководитель службы контроля качества ПО, ВымпелКом
Работал в ведущих ИТ компаниях: Nortel Networks, Orange Ltd, Amdocs. С 2003 года руковожу службой контроля качества программного обеспечения в Билайн. За это время создана распределенная команда высококлассных специалистов. Мы тестируем более 120 основных Business и Mission Critical систем. При этом удается избежать провалов и деградаций в продуктивной среде.
Александр Оружейников
Заместитель директора центра компьютерных технологий, НПО РусБИТех
С середины 90-х годов занимался разработкой и внедрением программных систем на основе ОС Linux. С 2006 по 2008 год руководил командой разработчиков ОС МСВС. С 2008 года по настоящее время активно участвует в разработке и внедрении операционной системы специального назначения «Astra Linux Special Edition» и защищенных программных комплексов, созданных на этой платформе.
Борис Позин
Технический директор, ЕС-лизинг
Занимается автоматизированным тестированием с 1970 года, разрабатывал методы тестирования и инструментальные средства в рамках работ Минрадиопрома СССР по технологии и автоматизации разработки систем реального времени. В течение более 10 лет поставил работы по автоматизированному функциональному и нагрузочному тестированию платежной системы Банка России. Руководит работами по созданию и эксплуатации систем обеспечения жизненного цикла ответственных систем. Читает лекции по курсу методология и технология создания автоматизированных систем в МИЭМ НИУ ВШЭ и МЭСИ.
Владимир Рубанов
Вице-президент по технологиям, Odin
Рубанов Владимир Васильевич – вице-президент по технологиям и директор “Росплатформа” в Odin (Parallels). Ранее президент и генеральный конструктор РОСА “Российские операционные системы”. Был первым директором Центра верификации Linux в 2005-2011 гг. Эксперт в организации разработки сложных программных систем и технологий в глобальной распределенной среде – консорциумы и коллективы из сотрудников разных компаний, волонтеров и виртуальных сообществ. Специалист в области системного ПО, open-source, стандартизации, интероперабельности и автоматизированной верификации программного обеспечения.
Григорий Сенин
Учебный Центр Люксофт
Алексей Хорошилов
Ведущий научный сотрудник, ИСП РАН
Директор Центра. С 1999 года работает в Институте системного программирования РАН, с 2009 года работает на кафедре Системного программирования факультета Вычислительной математики и кибернетики МГУ. Основные научные результаты: участие в создании технологии разработки тестов на основе формальных моделей UniTESK и поддерживающих ее инструментов, разработка унифицированной архитектуры тестового набора, руководитель работ по развитию и внедрению технологий моделирования систем авионики, тестирования, верификации моделей программ и дедуктивной верификации операционных систем. Читает лекции по курсу “Конструирование ядра ОС” и “Формальная спецификация и верификация программ”
Comment