Новая жизнь верификации

От программных систем все в большей степени каждодневно зависят жизнь и здоровье людей, однако программирование до сих пор остается единственной областью инженерной деятельности, где разработчик фактически не может гарантировать качество своей работы — реальные программы очень часто содержат ошибки, последствия которых не всегда безобидны. Интернет-ресурсы полны сообщениями о техногенных авариях — от гибели ребенка в автоматизированном туалете до аварий с человеческими жертвами автомобилей Toyota из-за ошибок в электронной системе торможения, причиной которых является некорректная работа программных систем управления. Спутник «Экспресс-АМ4», который должен был обеспечить доступ к Интернету и телевещанию на Дальнем Востоке, 25 марта 2012 года был выведен с околоземной орбиты и затоплен. При его запуске возник сбой в работе программного обеспечения разгонного блока, в результате чего спутник оказался на нерасчетной орбите. В связи с инцидентом страховая компания выплатила страховую сумму в размере более 7,5 млрд руб. Такие случаи делают проблему обеспечения правильности компьютерных программ особо важной.

Сложность программ давно подошла к границе их понимания человеком, а следовательно, к границе их управляемости, поэтому постоянно растет число ошибок в разработанных и сданных заказчику программных системах. Особенно подвержены ошибкам параллельные, распределенные и многопоточные программы, характерные для систем управления, причем именно такие программы получают сейчас все большее распространение —например, встраиваемые системы управления в автомобильной и авиационной промышленности, очень критичные к требованиям безопасности. В течение ближайших лет большинство новых автомобилей будут построены по схеме drive-by-wire — в них не будет механических соединений между рулем и колесами. В современном автомобиле уже имеется целая сеть из десятков связанных микропроцессоров, а бытовые ноутбуки с многоядерными процессорами ввели параллельное программирование и примитивы синхронизации параллельных процессов в широкий обиход программистов всех уровней.

Известно, что даже в тех случаях, когда функционирование каждого компонента системы параллельных взаимодействующих процессов полностью понятно, человеку трудно охватить работу всей такой системы — он в каждый момент может думать только об одной вещи, поэтому разработчик сложной программы не в состоянии уследить за многообразием событий, возникающих в параллельных системах. В мире параллельной обработки разработчик должен контролировать не последовательности возможных событий, как в последовательном программировании, а все возможные потоки частично упорядоченных событий, что значительно сложнее. Параллельные системы, которые работают правильно «почти всегда», годами могут сохранять тонкие ошибки, проявляющиеся в исключительных ситуациях.

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

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

До недавнего времени успехи в области теории алгоритмов и методов верификации были весьма скромными, а разработанные методы с большим трудом могли быть применены даже к системам средней сложности. Современный уровень возможностей в области так называемой дедуктивной верификации, основанной на методе Флойда – Хоара, демонстрирует результат, достигнутый недавно австралийскими учеными. В 2009 году исследовательский центр компании NISTA (Австралия) объявил о завершении работы по формальному доказательству корректности ядра операционной системы с помощью интерактивной системы доказательства теорем Isabelle. Верифицированная операционная система The Secure Embedded L4 microkernel содержит 7,5 тыс. строк кода на языке Cи. В процессе верификации было формально доказано 10 тыс. промежуточных теорем, а само доказательство заняло 200 тыс. строк и стало одним из самых длинных формальных доказательств, выполненных когда-либо с помощью автоматизированных инструментов. Авторы утверждают, что этот результат открывает путь к разработке нового поколения программных систем с беспрецедентным уровнем надежности.

Однако получение подобного результата весьма трудоемко — построение доказательства этой ОС потребовало около 60 человеко-лет, то есть для проверки 10 строк кода нужен месяц работы квалифицированного верификатора. Сложность доказательства оказалась в 30 раз выше, чем сложность кода, — иными словами, одна строка кода требует страницы доказательств. Эти оценки подтверждает Аллен Эмерсон из Университета штата Техас: «Раньше мы писали 15-страничный отчет о том, что программа на полстраницы корректна».

Таким образом, дедуктивная верификация, обладая несомненными достоинствами и громадным потенциалом, пока еще не может широко применяться для верификации сложных программных систем.

Прорыв

Сегодня в области верификации произошли глубокие изменения — был разработан метод формальной верификации model checking (проверка модели), который стал теоретической основой эффективных алгоритмов, позволяющих проверять правильность промышленных программно-аппаратных систем [1].

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

Алгоритмы верификации методом проверки модели были реализованы в ряде верификаторов (некоторые из них открыты для свободного использования). С их помощью проанализированы многие реальные программы, и в некоторых были найдены ошибки, причем найдены ошибки и в нескольких протоколах, несмотря на то что они были ранее рекомендованы как стандарты и использовались много лет. Например, группой профессора Эдмунда Кларка из университета Карнеги-Меллон при верификации методом проверки моделей протокола когерентности кэшей, известного как стандарт IEEE Futurebus+ 896.1-1991, было найдено несколько ошибок.

Уже сегодня метод формальной верификации начинает кардинально менять ситуацию в области разработки программных и аппаратных средств управления. В крупных корпорациях (Lockheed Martin, Rockwell Collins, NASA и др.), занимающихся разработкой бортовых авиационных и космических систем управления, были выполнены исследования по включению верификации в корпоративную технологию разработки программных комплексов. Результаты этих исследований показали, что верификация методом проверки модели может существенно повысить надежность систем для критических применений — многие ошибки выявляются на ранних этапах технологического цикла, что повышает качество разработок. В проекте Rockwell Collins, целью которого была разработка бортовой системы управления непилотируемого летательного аппарата для ВВС США, при создании одного из модулей системы было произведено сравнение результатов верификации этого модуля двумя независимо работавшими группами разработчиков. Одна из групп проводила тестирование модуля, а вторая выполняла его верификацию методом Model checking. Группа, проводившая верификацию методом проверки модели, обнаружила 12 ошибок, в то время как команда тестировщиков не нашла ни одной. При этом верификация методом проверки модели заняла на треть меньше времени, чем тестирование.

В 2008 году три исследователя, внесшие наибольший вклад в разработку техники и алгоритмов метода проверки модели, — Эдмунд Кларк, Аллен Эмерсон и Джозеф Сифакис — были награждены премией Тьюринга. Примечательна формулировка, с которой была присуждена эта премия: «за их роль в превращении метода проверки модели в высокоэффективную технологию верификации, широко используемую в индустрии разработки ПО и аппаратных средств».

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

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

Несмотря на то что сам процесс верификации методом проверки модели полностью автоматизирован и техника его применения проще, чем теория, работа по верификации программы требует от программиста достаточно высокой квалификации. Действительно, для выполнения верификации нужно построить для программной системы адекватную модель с конечным числом состояний, которую можно преобразовать в конечную систему переходов — структуру Крипке, представить ее на входном языке верификатора, выделить подлежащие проверке свойства поведения параллельной системы и выразить их формулами темпоральной логики, суметь использовать полученный от верификатора контрпример для отладки анализируемой системы при невыполнении в ней проверяемого свойства.

Очевидно, что новые методы верификации должны быть внедрены в практику обучения программистов и разработчиков аппаратуры. В одном из отчетов NASA отмечается: «Формальные методы должны стать частью образования каждого исследователя в области информатики, каждого разработчика ПО так же, как другие ветви прикладной математики являются необходимой частью образования в других инженерных областях».

Верификация протокола транзакционной памяти

В Санкт-Петербургском политехническом университете преподавание основ верификации программ ведется уже более десяти лет, и кроме теоретических знаний студенты получают первоначальный опыт верификации нетривиальных параллельных программ, используя свободно распространяемый инструмент верификации Spin, разработанный в Bell Labs. В рамках этой дисциплины студентам даются теория, алгоритмы, элементы технологии и инструментарий, позволяющие проверять корректность параллельных и распределенных программ. Книга [1] покрывает материал лекций, в ней также изложены и некоторые результаты научной группы, работающей в этом направлении. Учебное пособие [2] содержит описание системы Spin, инструкцию по ее установке и запуску, описание входного языка верификатора и подробно разобранные примеры верификации нескольких параллельных программ.

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

В 2009 году был предложен новый алгоритм поддержки транзакционной памяти, основанный на принципе «временного окна». Описание нового протокола сопровождалось аналитическим доказательством его корректности. Авторы протокола — известные ученые в области параллельного программирования, поэтому сомнения в корректности нового протокола, опубликованного с ясными объяснениями его функций и доказательством его правильности, были минимальны. Несмотря на это новый протокол поддержки транзакционной памяти был дан для проверки студенту четвертого курса, прослушавшему курс по верификации программ. Студент построил модель протокола на входном языке системы Spin, сформулировал на языке темпоральной логики требования к поведению протокола и нашел в нем тонкую ошибку [3]. Как оказалось, в опубликованном протоколе нарушено так называемое свойство непрозрачности (opacity): в некоторых ситуациях транзакции, подлежащей завершению, не запрещается продолжать выполнение действий с несогласованными данными. Впоследствии эта транзакция будет завершена, а результаты ее работы не будут зафиксированы в памяти, однако в прикладной программе может возникнуть ошибка, если в результате действий с несогласованными данными возникнет исключительная ситуация, например деление на 0. Очевидно, что проявления этой тонкой ошибки маловероятны, поэтому ошибка, пропущенная в ходе аналитической верификации протокола, могла годами оставаться необнаруженной, прежде чем она бы привела к сбою в прикладной программе. В следующем варианте протокола, опубликованном в журнале Journal of Supercomputing, ошибка в алгоритме была исправлена, а авторы выразили студенту благодарность за найденную ошибку.

***

Верификация — строгое формальное доказательство выполнения в программе формально определенных требований к ее поведению — совершенно необходима в тех случаях, когда программа состоит из множества параллельно работающих и взаимодействующих между собой модулей. Сегодня верификация становится одним из основных методов достижения высокой надежности программного обеспечения в дополнение к традиционным методам тестирования и отладки. В последние несколько лет в области верификации произошли существенные изменения, превратившие ее из «игры разума» теоретиков в практические методики анализа реальных программ. Разработанные автоматические системы верификации позволяют даже студентам обнаруживать тонкие ошибки, допущенные профессионалами в ответственных параллельных программах. Уже сегодня методы верификации используются в технологическом цикле разработки больших индустриальных программ в ведущих компаниях, создающих программные системы для критических применений. Знание формальных моделей и методов верификации, умение использовать эти методы для обеспечения высокого качества разрабатываемых программных систем становятся необходимыми для профессиональных программистов.

Литература

1. Карпов Ю. Г. Model checking. Верификация параллельных и распределенных программных систем. // БХВ Петербург, 2010, 560 с.
2. Шошмина И. В., Карпов Ю. Г. Введение в язык Promela и систему комплексной верификации Spin. Учебное пособие. // С-Петербург, СПбГПУ, 2010, 111 с.
3. Беляев А. Б. Верификация алгоритма транзакционной памяти. // Научно-технические ведомости, СПбГПУ, 2010, № 101.

Юрий Карпов (karpov@dcn.ftk.spbstu.ru) — зав. кафедрой «Распределенные вычисления и компьютерные сети» Санкт-Петербургского политехнического университета.