`

СПЕЦИАЛЬНЫЕ
ПАРТНЕРЫ
ПРОЕКТА

Архив номеров

Best CIO

Определение наиболее профессиональных ИТ-управленцев, лидеров и экспертов в своих отраслях

Человек года

Кто внес наибольший вклад в развитие украинского ИТ-рынка.

Продукт года

Награды «Продукт года» еженедельника «Компьютерное обозрение» за наиболее выдающиеся ИТ-товары

 

Новый метод доказывает бездефектность сложных программ без тестирования

0 
 

Новый метод доказывает бездефектность сложных программ без тестирования

Группа программных инженеров из Мичиганского университета, Microsoft Research и Университета Карнеги-Меллона (штат Пенсильвания) представила созданную ими систему Armada, для проверки правильности работы сложных программ без необходимости тестировать их с полным диапазоном возможных входных величин.

«По сути, если вы не перепробуете все возможные входные данные, то можете что-то упустить, — говорит профессор Манос Каприцос (Manos Kapritsos), соавтор статьи, представленной на конференции Programming Language Design and Implementation (PDLI 2020). — И на практике это происходит сплошь и рядом. Системы, о которых мы говорим, очень сложны, и тестировщики не могут исчерпывающе проверить все варианты их поведения».

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

Формальная верификация не всегда является панацеей. Поиск удовлетворительного доказательства сложных, в том числе конкурентных или многопотоковых программ, часто превращается в длительный и ресурсоемкий процесс.

Armada подвергает подобный сложный код серии преобразований, разбивая его на более простые фрагменты. Разработчикам остаётся доказать, что каждый упрощенный код действительно является представлением более сложной программы с предыдущего этапа.

Для этого разработчик с помощью высокоуровневого синтаксиса Armada составляет краткое описание своего программного обеспечения и используемых методов проверки, на основе чего система автоматически генерирует значительно более длинное полное доказательство. В одном из случаев такое итоговое доказательство содержало 24 540 строк, при этом вручную было написано только 70 строк этого кода.

В случае неудачи доказательства пользователь генерирует новое: с изменённым описанием или другим методом из библиотеки Armada. Система использует верификатор для проверки надёжности всех предлагаемых ею методов доказательства, и допускает расширение их ассортимента в дальнейшем.

В конце концов, разработчик получает простую высокоуровневую спецификацию всей своей программы, затратив рекордно малые усилия на верификацию сложного многопотокового кода.

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


Вы можете подписаться на наш Telegram-канал для получения наиболее интересной информации

0 
 

Напечатать Отправить другу

Читайте также

 

Slack подает жалобу на Microsoft и требует антимонопольного расследования от ЕС

 
Реклама

  •  Home  •  Рынок  •  ИТ-директор  •  CloudComputing  •  Hard  •  Soft  •  Сети  •  Безопасность  •  Наука  •  IoT