Верификация программ

Проблемы верификации программ занимают центральное положение в современной информатике и индустрии разработки корректного, надёжного и безопасного программного и аппаратного обеспечения. В самой общей форме проблема верификации программ заключается в построении математического доказательства утверждения о том, что анализируемая программа удовлетворяет предъявляемым к ней требованиям. Требования к программам могут отражать самые различные аспекты их функционирования, например один класс требований заключается в том, что программа корректно вычисляет заданную функцию, другой класс требований выражает различные свойства безопасности (например, отсутствие неавторизованных утечек информации в результате работы программы), третий класс требований выражает надёжность программы (т.е. её способность сохранять работоспособность в нештатных ситуациях), и т.д. Различные классы требований к программам верифицируются на основе различных математических моделей (к числу которых относятся графовые модели, логические модели, алгебраические модели, вероятностные модели, и т.п.). В настоящее время большинство проверок соответствия программ предъявляемым к ним требованиям выполняется путем тестирования программ, однако тестирование является ненадёжным механизмом обоснования соответствия программ предъявляемым к ним требованиям. Как писал один из классиков программирования Э.Дейкстра, тестирование помогает обнаружить ошибки, но не может обосновать их отсутствие. Точное обоснование соответствия программ предъявляемым к ним требованиям может быть построено только путем верификации. Для верификации различных классов программ разработаны различные математические модели и основанные на данных моделях методы и алгоритмы. В курсе будут отражены некоторые классы моделей программ и описаны соответствующие алгоритмы верификации, в частности, метод Флойда верификации блок-схем, методы структурной индукции и вычислительной индукции верификации функциональных программ, а также метод, основанный на аппарате теории процессов