«Сегодня создаются очень большие программы. И самое удивительное, что они работают». Такими словами академик, директор Института системного программирования РАН Виктор Иванников открыл научно-практическую конференцию по разработке программного обеспечения Software Engineering Conference Russia. На протяжении семи лет проведения конференции SECR тема качества ПО остается на ней одной из центральных. Причины очевидны. Иванников отметил, что количество ошибок в программных системах в среднем составляет десять на тысячу строк кода. Учитывая, что современное индустриальное ПО – это миллионы строк, такая статистика говорит о том, что большие системы переполнены ошибками, даже при условии, что в наиболее отлаженных из них число ошибок может снижаться до одной – трех на тысячу строк.

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

Однако несколько лет назад был предложен более простой и эффективный метод model сhecking, позволяющий проводить верификацию динамических, то есть развивающихся во времени систем. Он добавляет к обычной логике высказываний, описывающей требования к поведению системы, параметр времени и проверяет на модели программы истинность формул этой так называемой темпоральной логики. Специальные исследования показали, что верификация по данному методу во многом раз превышает по эффективности традиционное тестирование, позволяя выявлять наиболее серьезные программные ошибки на максимально ранних стадиях процесса разработки. По словам Карпова, к включению этого метода в промышленную разработку все чаще обращаются ведущие вендоры ПО.

Еще одним центром исследования проблем верификации в Петербурге станет кафедра программной инженерии и верификации программ, созданная в Санкт-Петербургском государственном университете ИТ, механики и оптики, которую возглавил ученый с мировым именем, профессор Высшей политехнической школы в Цюрихе Бертран Мейер, также выступивший на конференции SECR.