Технология Выделено требований Протестировано функций Найдено ошибок



Pdf просмотр
Дата20.11.2016
Размер0.77 Mb.
Просмотров505
Скачиваний0

Институт системного программирования РАН
10 лет Центра верификации ОС Linux
Верификация реального ПО – мечта или реальность?
Александр К.Петренко,
Алексей В. Хорошилов


1994 – тестирование на основе формальных спецификаций SBT/MBT: NORTEL (API ОС – переносимость – интероперабельность)

2000 – 2002 – IPv6/CTesk Microsoft Research

2001 – LSB – борьба за интероперабельность и против фрагментации рынка приложений
ОС Linux

2004 – LSB: Intel - фальстарт
Предыстория


2005 – OLVER+LVC: Минобрнауки при поддержке
Президиума РАН (LSB Core, 1500 функций)

2006 – FSG – FSG+OSDL=Linux Foundation-LF (2007)

2007-2011 – LF+Nokia+Motorola – развитие вширь
(более 25-ти тысяч функций)

2007 – POSIX+ARINC-653: НИИСИ РАН Багет
ОС2000/3000/4000 РПКБ/КРЭТ/Электроавтоматика

Аналог: Microsoft Interoperability Initiative (2008-
2010)
Первый период. Развитие вширь.

Первый период. Развитие вширь.
Технология
Выделено
требований
Протестировано
функций
Найдено
ошибок
(реал./требов.)
CTESK /
UniTESK
24 000
1532
100 / 100
T2C
4 476
1553
40 / 40
API Sanity
AutoTest
0
24 000
10 / 0

Первый период. Развитие вширь.
Промежуточные итоги:

Информационная инфраструктура стандарта
LSB (> 40 тысяч функций)

Три слоя технологий тестирования

False positive – 0% (?)

Требования к квалификации – пользователь библиотек ОС
Технология
Производительность
(функций в неделю)
Качество
тестирования
CTESK / UniTESK
1-2
высокое
T2C
>5
среднее
API Sanity AutoTest
>100
Проверка работоспособности
(sanity testing)

Второй период.
Развитие вглубь.

2007 – software model checking – BLAST, CPAChecker

2011 – тестирование ядра ОС в условиях отказов оборудования

2012 – гипервизор для защиты приложений от скомпромитированной ОС

2013 – дедуктивная верификация, развитие
Frama-C/Why-3/Jessie

2005 – система управления требованиями

Аналоги

Microsoft Research SLAM/SDK/WDK (2002 по н.в.)

seL4 verification project (2006-2014
(Минобрнауки/Google/ГосНИИАС/РусБИТех)

Software Model Checking

Результаты

Найдено и исправлено >200 ошибок в ядре Linux

Первое место в международных соревнованиях
SV-COMP'2012 и SV-COMP'2014
по software verification в категории DeviceDrivers64
See details: http://linuxtesting.org/ldv

Промежуточные итоги:

Software model checking

трудоемкость - 2 правила в месяц,

скорость верификации –
4000 драйверов * 1 правило = 1 день

false positive – 10-90%

требования к квалификации – разработчик драйвера ОС

Дедуктивная верификация

трудоемкость 1 функция в месяц

время "переверификации" – 1 неделя

false positive – 0%

требования к квалификации

разработчик драйвера ОС + дедуктивная верификация
Второй период.
Развитие вглубь.

Планы

2017 – масштабируемая верификация модулей ОС Linux

2017 – дедуктивная верификация многопоточности в ядре ОС Linux

2016-2018 – сертифицируемая ОС реального времени – макет и пакет сертификационных документов

Дискуссия

Верификация реального ПО –
мечта или реальность?

Каковы причины такого положения дел?

Что мешает применению новых технологий?

Как выбирать эффективный набор технологий в контексте конкретной практической задачи?

Вопрос надо ставить в другой плоскости?

Институт системного программирования РАН
Все на фуршет!

Document Outline

  • Slide 1
  • Предыстория
  • Первый период. Развитие вширь.
  • Slide 5
  • Slide 6
  • Slide 12
  • Slide 13
  • Slide 14
  • Промежуточные итоги
  • Планы
  • Slide 20
  • Верификация реального ПО – мечта или реальность?
  • Все на фуршет!

Каталог: 2015
2015 -> Методические рекомендации Элиста 2015 Составитель
2015 -> Правила закаливания… Выпуск №1. Чтоб улыбка сияла. Мама первый стоматолог
2015 -> Справка о наличии печатных и электронных образовательных и информационных ресурсов муниципального казенного дошкольного образовательного учреждения «Детский сад «Колокольчик»
2015 -> Рабочая программа практического обучения по специальности 51. 02. 02 «Социально-культурная деятельность» 2014 г
2015 -> Муниципальное бюджетное
2015 -> Занятие №18 Здравствуйте, участники программ личностного развития для детей!
2015 -> Информации и коммуникации на подрастающее поколение. Научно исследовательская
2015 -> Шелакина А. А. Студентка 2 курса атп 921 ппк сгту имени Гагарина Ю. А
2015 -> 1. Название темы Проект по молодёжной политике города Таганрога


Поделитесь с Вашими друзьями:


База данных защищена авторским правом ©nethash.ru 2019
обратиться к администрации

войти | регистрация
    Главная страница


загрузить материал