АНАЛИЗ ЭФФЕКТИВНОСТИ ПРИМЕНЕНИЯ ФОРМАЛЬНЫХ МЕТОДОВ ВЕРИФИКАЦИИ В РАЗРАБОТКЕ КРИТИЧЕСКИХ ПРОГРАММНЫХ СИСТЕМ

Аннотация

В данной расширенной научной статье проводится комплексное исследование методологий обеспечения надежности программного кода через внедрение механизмов формальной верификации и статического анализа на ранних этапах жизненного цикла разработки. Актуальность работы обусловлена возрастающей сложностью программных архитектур в аэрокосмической, медицинской и оборонной отраслях, где цена логической ошибки может привести к катастрофическим последствиям. В рамках статьи осуществляется глубокая декомпозиция подходов к проверке моделей (Model Checking) и дедуктивной верификации, анализируются возможности современных систем типов в языках программирования для автоматического доказательства корректности работы алгоритмов. Авторы подробно рассматривают математический аппарат логики Хоара и исчисления предикатов как фундамента для построения безошибочных систем и доказывают, что использование формальных спецификаций позволяет обнаружить до 90% критических уязвимостей до этапа компиляции. В работе уделяется внимание инструментам автоматизированного доказательства теорем (SMT-сольверам) и их интеграции в современные конвейеры непрерывной разработки.