Как стать автором
Обновить

Комментарии 8

Здравствуйте. Можете чуть подробнее рассмотреть непосредственно процесс верификации? Я пытался разобраться в TLA+ и его применении к МК (книжка Formal Development of a Network-Centric RTOS), там на вход подаётся совсем не сишный код.
Добрый день! Действительно, в Formal Development of a Network-Centric RTOS верифицировался не код RTOS, а, скорее, спецификация на нее. В статье я показывал верификацию именно кода, так как спецификации могут быть и недоступны (легаси-код, сторонние библиотеки). В современных реалиях, впрочем, для создания систем повышенной надежности применяют модельно-ориентированное проектирование, где модель и есть спецификация системы, и существуют инструменты для формальной верификации моделей (Simulink Design Verifier).
Касательно самого процесса — требуется уточнить, что именно вас интересует: математика под капотом Polyspace Code Prover или процесс верификации софта в целом?
И то, и другое. Когда я пытался разобраться в предмете, все писали, что из кода верификации нельзя сгенерировать исполняемый код, неважно, темпоральная логика или абстрактные автоматы, обратное на тот момент (2015) тоже было верно. Вот мне и интересно: как (математически) можно подать на верификацию код или симулинковскую модель и получить оценку логической консистентности. Предполагается, что на входе мы имеем спецификации (текстовый ТЗ), а на выходе исполняемый код. Как построен процесс в TDD и откуда берутся артефакты в виде тестов понятно, про TLA+ тоже понятно, там в качестве артефакта спецификация на TLA, а как у вас и как генерируются артефакты?
С моделью Simulink все достаточно просто, Simulink Design Verifier интегрируется бесшовно в Simulink и умеет парсить модели для создания верифицируемого представления. То же самое и с Code Prover — сначала код «компилируется» (раскрываются дефайны, токены и т.д.), потом результаты такой «компиляции» распарсиваются самим движком инструмента.

>> на входе мы имеем спецификации (текстовый ТЗ), а на выходе исполняемый код
Текстовое ТЗ в код сложно конвертировать, обычно по ТЗ строят модель в Simulink, а потом из модели получают исходный код с помощью генератора исходного кода

Теперь, что касается верификации софта в целом — это долгий процесс, включающий в себя не только статический анализ или формальную верификацию кода, но и юнит-тестирование со сбором покрытия, интеграционное тестирование со сбором покрытия, тестирование на робастность. А еще есть отдельные сверхкритичные системы, для верификации софта которых надо собирать покрытие тестами ассемблера. И конечно, каждый тест должен быть привязан к требованию, как и любая строка кода.
Тему вы очень важную затронули, а вот пример «дикий». Больно смотреть на «pictrl.c», работа с массивами и указателями — безобразная. В коде перемешаны локальные и глобальные переменные, система именования — никакая. Ветки условных операторов не все выполняются. И без анализатора ясно, что это работать не будет.
Хотелось бы увидеть, что MISRA выдаст на этот код и сравнить с вашим софтом.
Добрый день! Я прогнал дополнительно проверки на MISRA. Так как хабр не дает прикреплять к комментам файлы, загрузил отчет сюда:
Zip с результатами
Единственное, я брал достаточно старенькую MISRA C:2012, без каких либо дополнений или поправок.
К слову, результаты проверки на соответствие MISRA C:2012 будут отличаться: Bug Finder нашел 20 нарушений, а Code Prover — 43.
очень интересно послушать про квалификацию инструмента. сами вовлечены в верификацию ПО.
Только полноправные пользователи могут оставлять комментарии. Войдите, пожалуйста.