ФОРМАЛЬНЫЕ МЕТОДЫ ВЕРИФИКАЦИИ ПРОГРАММНЫХ СИСТЕМ НА ПРИМЕРЕ ЯЗЫКА FRAMA-C

Abstract

Программное обеспечение играет важную роль в современном мире, корректность и безопасность программного кода являются ключевыми аспектами, которые нужно учитывать при разработке программных систем. В связи с этим все большую популярность получают формальные методы верификации, которые позволяют доказывать корректность программного кода математически. Одним из инструментов для формальной верификации является язык программирования Frama-C, который предназначен для анализа и верификации программных систем на языке C. Frama-C позволяет проводить статический анализ программного кода и доказывать его корректность с помощью формальных методов. Целью данной статьи является рассмотрение принципов работы языка Frama-C и его применения для анализа и верификации программного кода на языке C. Будут рассмотрены основные концепции Frama-C, а также пример его применения для анализа корректности и безопасности программного кода.