Форма входа

Логин:
Пароль:

Поиск

Наши координаты

Телефон:
+7 (913) 229 5479
Адрес:
г. Барнаул
пр. Строителей, 16, оф. 613
Почтовый адрес:
656067, Алтайский край, г.Барнаул, 67 отделение связи,
а/я 4180
E-mail:
support@oit-company.ru

Наши партнёры





Среда, 30.09.2020, 07:58
Приветствуем Вас Гость
Регистрация | Вход | RSS

ОТДЕЛ
ИНФОРМАЦИОННЫХ
ТЕХНОЛОГИЙ
 
Главная » 2009 » Август » 15 » Найден способ формального подтверждения 100% отсутствия ошибок в программе
Найден способ формального подтверждения 100% отсутствия ошибок в программе
10:18

Ученые из австралийского исследовательского центра NICTA нашли способ математически доказать, что определенное ПО не содержит ошибок и, соответственно, не станет причиной отказа управляемого им оборудования. Проведение такого рода тестирования жизненно необходимо во многих отраслях промышленности, таких как, например, авиа и автомобилестроение, где сбои в бортовой компьютерной сети возникают чаще, чем поломки механических агрегатов.

Для проведения теста было взято микроядро Secure Embedded L4 (seL4), содержащее 8700 строк кода базирующегося на open source проекте OKL4. Ядро является ключевым компонентом любых современных встраиваемых устройств, и имеет неограниченный доступ ко всем работающим системам. Суть тестирования заключалась в том, чтобы доказать, что написанный код удовлетворяет всем тем спецификациям, которые были заложены на этапе проектирования. В результате, испытание было пройдено успешно и достигнуто 100% соответствие предъявляемым требованиям.

Работой по формулировке алгоритма математического доказательства в течение четырех лет занималась команда из 12 исследователей NICTA, аспирантов и техников. Они успешно проверили более 10 тыс. промежуточных теорем, изучив более чем 200 тыс. строк кода. Итоговый анализ выполняется с помощью интерактивной программы Isabelle, и на сегодняшний день является самой объемной автоматизированной проверкой выполнения условий теорем.

Наряду с доказательством соответствия программного кода выполняемым функциям, тестирование показало, что seL4 не подвержен большинству известных хакерских атак. Например, атака «переполнение буфера», позволяющая внедрить злонамеренный код и захватить управление работой ядром, не даст результата.

Полное изложение работы исследователей будет озвучено на 22-ом симпозиуме, посвященном принципам работы операционных систем (SOSP). Также ожидается, что NICTA передаст все интеллектуальные права на результаты исследования opensource компании Open Kernel Labs.
Источник http://www.opennet.ru/opennews/art.shtml?num=23011
Просмотров: 822 | Добавил: sashacd | Рейтинг: 0.0/0 |

Copyright ООО "Отдел Информационных Технологий" © 2020