С моделью Simulink все достаточно просто, Simulink Design Verifier интегрируется бесшовно в Simulink и умеет парсить модели для создания верифицируемого представления. То же самое и с Code Prover — сначала код «компилируется» (раскрываются дефайны, токены и т.д.), потом результаты такой «компиляции» распарсиваются самим движком инструмента.
>> на входе мы имеем спецификации (текстовый ТЗ), а на выходе исполняемый код
Текстовое ТЗ в код сложно конвертировать, обычно по ТЗ строят модель в Simulink, а потом из модели получают исходный код с помощью генератора исходного кода
Теперь, что касается верификации софта в целом — это долгий процесс, включающий в себя не только статический анализ или формальную верификацию кода, но и юнит-тестирование со сбором покрытия, интеграционное тестирование со сбором покрытия, тестирование на робастность. А еще есть отдельные сверхкритичные системы, для верификации софта которых надо собирать покрытие тестами ассемблера. И конечно, каждый тест должен быть привязан к требованию, как и любая строка кода.
Добрый день! Я прогнал дополнительно проверки на MISRA. Так как хабр не дает прикреплять к комментам файлы, загрузил отчет сюда: Zip с результатами
Единственное, я брал достаточно старенькую MISRA C:2012, без каких либо дополнений или поправок.
К слову, результаты проверки на соответствие MISRA C:2012 будут отличаться: Bug Finder нашел 20 нарушений, а Code Prover — 43.
Добрый день! Действительно, в Formal Development of a Network-Centric RTOS верифицировался не код RTOS, а, скорее, спецификация на нее. В статье я показывал верификацию именно кода, так как спецификации могут быть и недоступны (легаси-код, сторонние библиотеки). В современных реалиях, впрочем, для создания систем повышенной надежности применяют модельно-ориентированное проектирование, где модель и есть спецификация системы, и существуют инструменты для формальной верификации моделей (Simulink Design Verifier).
Касательно самого процесса — требуется уточнить, что именно вас интересует: математика под капотом Polyspace Code Prover или процесс верификации софта в целом?
Добрый день.
Я правильно понял, что ваш вопрос заключается в том, может ли быть связь одновременно и входом и выходом? Если так, то это увы не выйдет. Это фундаментальная особенность System Composer, да и вообще Simulink — разделение входных и выходных портов. Правда, можно сделать «обратную связь»:
Добрый день! Спасибо за комментарий.
Данный метод отличается тем, что компонентам в System Composer могут быть назначены свойства с учетом природы этих компонентов (например, TDP для физического компонента или WCET для программного). Подсистемы этого не учитывают. Я как раз буду говорить о том, как работать с компонентами различной природы во второй части туториала.
Конечно, статья немного запоздала, но я все же ее написал:
https://habr.com/ru/company/etmc_exponenta/blog/534906/
>> на входе мы имеем спецификации (текстовый ТЗ), а на выходе исполняемый код
Текстовое ТЗ в код сложно конвертировать, обычно по ТЗ строят модель в Simulink, а потом из модели получают исходный код с помощью генератора исходного кода
Теперь, что касается верификации софта в целом — это долгий процесс, включающий в себя не только статический анализ или формальную верификацию кода, но и юнит-тестирование со сбором покрытия, интеграционное тестирование со сбором покрытия, тестирование на робастность. А еще есть отдельные сверхкритичные системы, для верификации софта которых надо собирать покрытие тестами ассемблера. И конечно, каждый тест должен быть привязан к требованию, как и любая строка кода.
Zip с результатами
Единственное, я брал достаточно старенькую MISRA C:2012, без каких либо дополнений или поправок.
К слову, результаты проверки на соответствие MISRA C:2012 будут отличаться: Bug Finder нашел 20 нарушений, а Code Prover — 43.
Касательно самого процесса — требуется уточнить, что именно вас интересует: математика под капотом Polyspace Code Prover или процесс верификации софта в целом?
Я правильно понял, что ваш вопрос заключается в том, может ли быть связь одновременно и входом и выходом? Если так, то это увы не выйдет. Это фундаментальная особенность System Composer, да и вообще Simulink — разделение входных и выходных портов. Правда, можно сделать «обратную связь»:
Данный метод отличается тем, что компонентам в System Composer могут быть назначены свойства с учетом природы этих компонентов (например, TDP для физического компонента или WCET для программного). Подсистемы этого не учитывают. Я как раз буду говорить о том, как работать с компонентами различной природы во второй части туториала.