Одним из гостей SECR стал легендарный Бертран Мейер, возглавивший кафедру программной инженерии и верификации программ в Санкт-Петербургском госуниверситете ИТ, механики и оптики
Одним из гостей SECR стал легендарный Бертран Мейер, возглавивший кафедру программной инженерии и верификации программ в Санкт-Петербургском госуниверситете ИТ, механики и оптики

На протяжении семи лет проведения конференции тема качества ПО остается на ней одной из центральных. Причины очевидны. По словам Иванникова, количество ошибок в программных системах в среднем составляет десять на тысячу строк кода. Учитывая, что современное индустриальное ПО – это миллионы строк, такая статистика говорит о том, что большие системы переполнены ошибками, даже при условии, что в наиболее отлаженных из них число ошибок может снижаться до одной-трех на тысячу строк.

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

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

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

Приглашение мировых знаменитостей – одна из традиций SECR, которым организаторы конференции остаются верны. Традиционные темы форума – актуальные тенденции разработки, результаты научных исследований в области программной инженерии, проблемы подготовки кадров. С прошлого года на конференции активно обсуждаются и вопросы предпринимательства – создание эффективных стартапов, управление продуктами и проектами, формирование нового поколения менеджеров в сфере разработки. Сама конференция производит впечатление вполне успешного проекта, хотя в прошлом году SECR пережила определенный кризис – ее организация оставляла желать много лучшего. По словам председателя нынешней конференции Николая Пунтикова, восстановление репутации форума было одним из стимулов для организаторов в этом году. И им, пожалуй, это удалось – конференция переехала из не очень удобного культурного центра Высшей школы экономики в модный Digital October, собрала около 700 участников и представила насыщенную трехдневную программу.