.jpg) |
| ОДНИМ ИЗ ГОСТЕЙ SECR стал легендарный Бертран Мейер, возглавивший кафедру программной инженерии и верификации программ в Санкт-Петербургском госуниверситете ИТ, механики и оптики |
«Сегодня создаются очень большие программы. И самое удивительное, что они работают». Такими словами академик, директор Института системного программирования РАН Виктор Иванников открыл седьмую научно-практическую конференцию по разработке программного обеспечения SECR (Software Engineering Conference Russia). На протяжении семи лет проведения конференции тема качества ПО остается на ней одной из центральных. Причины очевидны. По словам Иванникова, количество ошибок в программных системах в среднем составляет десять на тысячу строк кода. Учитывая, что современное индустриальное ПО — это миллионы строк, такая статистика говорит о том, что большие системы переполнены ошибками, даже при условии, что в наиболее отлаженных из них число ошибок может снижаться до одной-трех на тысячу строк.
Поиск эффективных и научно обоснованных методов гарантии качества программных продуктов в последнее время становится одним из наиболее активных направлений университетских исследований в области программной инженерии, постепенно находя отклик и в индустрии разработки ПО. Об этом говорил в своем выступлении профессор Юрий Карпов из Санкт-Петербургского политехнического университета. В университете занимаются изучением новых методов верификации программных систем.
Верификация представляет собой формальное доказательство того, что программная система, описанная с помощью формальной модели, удовлетворяет формально определенным требованиям. Как рассказал Карпов, до недавнего времени основным методом верификации был дедуктивный. Его применение в практике разработки оказывалось невозможным, поскольку сложность доказательства правильности программы с помощью этого метода в десятки раз превышает сложность самой программы. Для одной строки кода получалась целая страница доказательств.
Однако несколько лет назад был предложен более простой и эффективный метод — model сhecking, позволяющий проводить верификацию динамических, то есть развивающихся во времени систем. Он добавляет к обычной логике высказываний, описывающей требования к поведению системы, параметр времени и проверяет на модели программы истинность формул темпоральной логики. Специальные исследования показали, что верификация в соответствии с новым методом во много раз превышает по эффективности традиционное тестирование, позволяя выявлять наиболее серьезные программные ошибки на ранних стадиях процесса разработки. По словам Карпова, к включению этого метода в промышленную разработку все чаще обращаются ведущие производители ПО, например корпорация Microsoft. Они же спонсируют исследования возможностей практического использования верификации — эта область программной инженерии становится очень популярной в университетах. В личной беседе Карпов посетовал, что его кафедре пока серьезно не хватает финансирования, несмотря на достигнутые успехи.
Еще одним центром исследования проблем верификации в Петербурге станет образованная нынешним летом кафедра программной инженерии и верификации программ в Санкт-Петербургском госуниверситете ИТ, механики и оптики (ИТМО), которую возглавил ученый с мировым именем, профессор Высшей политехнической школы в Цюрихе Бертран Мейер. Вопросы создания качественного ПО занимают в научной деятельности Мейера центральное место, но выступление на SECR он посвятил другой теме — разработке требований. Мейер противопоставил свой систематический подход скорым (agile) методам, тем самым вступив в неявную дискуссию с другим гуру, приехавшим в этом году на конференцию, — создателем метода скорой разработки Scrum Джефом Сазерлендом.
Приглашение мировых знаменитостей — одна из традиций SECR, которым организаторы конференции остаются верны. Традиционные темы форума — актуальные тенденции разработки, результаты научных исследований в области программной инженерии, проблемы подготовки кадров. С прошлого года на конференции активно обсуждаются и вопросы предпринимательства — создание эффективных стартапов, управление продуктами и проектами, формирование нового поколения менеджеров в сфере разработки. Сама конференция производит впечатление вполне успешного проекта, хотя в прошлом году SECR пережила определенный кризис — ее организация оставляла желать много лучшего.
По словам председателя нынешней конференции Николая Пунтикова, восстановление репутации форума было одним из стимулов для организаторов в этом году. И им, пожалуй, это удалось — конференция переехала из не очень удобного культурного центра Высшей школы экономики в модный Digital October, собрала около 700 участников и представила насыщенную трехдневную программу.