Формальные методы в agile-разработке

Разработка сложных программных систем всегда требует особого подхода, и даже если стремиться к простоте, необходимость учитывать постоянно меняющиеся запросы заказчика может привести к тому, что решение постепенно утратит элегантность. Безусловно, грамотный разработчик будет учитывать предполагаемую эволюцию системы даже в тех случаях, когда нельзя точно спрогнозировать характер изменений, но соответствующие навыки приходят только с опытом и к тому же требуют особенно хорошего понимания принципов использования абстракций. Объектно-ориентированное проектирование и модуляризация, например применение Z-нотации, при аккуратном следовании правилам позволяют свести к минимуму проблемы, обусловленные изменениями. Для улучшения корректности программных систем рекомендуется пользоваться формальными методами [1, 2], а упростить адаптацию к меняющимся требованиям позволяют agile-методы, характеристики которых описаны, в частности, в «Манифесте скорой методологии разработки» (Agile Manifesto).

Формализация

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

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

Скорая (agile) разработка базируется на итеративном подходе — сама система и требования к ней эволюционируют благодаря взаимодействию участников команды; поощряется быстрый учет изменений в требованиях. Традиционные формальные методы на это не рассчитаны, но при использовании современных инструментальных средств возможна и быстрая формализованная разработка. К примеру, среда RODIN сводит к минимуму количество повторных доказательств отсутствия дефектов при изменениях системы. Существует также разработанный в МТИ инструментарий моделирования Alloy Analyzer, относительно простой в освоении для квалифицированного разработчика и быстро внедряемый в agile-процессы.

Концепция формальных agile-методов появилась в середине 2000-х годов, а в 2009 году в журнале Computer был опубликован доклад по формальным методам и agile-разработке. Многие agile-разработчики, скорее всего, уже знакомы с основами формальных методов, но если нет, то обучение хотя бы чтению формальных спецификаций не помешает, даже если соответствующий подход активно применять не планируется.

Можно ли с помощью agile-методов разрабатывать защищенное ПО, например, если формализовать требования к безопасности? Мнения по этому вопросу расходятся. Agile-методологии наподобие Scrum и XP становятся общепринятыми, однако им все же не доверяют, когда для заказчиков приоритетна защищенность разрабатываемой системы. Хотя сама проблема существует уже как минимум десять лет, до недавнего времени задачу интеграции практик обеспечения безопасности в agile-разработку решать практически не пытались. Для этого важно четко сформулировать требования к безопасности, назначив им соответствующий приоритет при разработке, чтобы уделять им внимание в каждой итерации. Agile-методы нацелены на удовлетворение потребностей заказчика, для которого часто важнее быстро получить функциональность, напрямую приносящую доход бизнесу. Безопасность же, позволяющая снизить риски и предотвратить злоупотребление реализованными функциями, к сожалению, ценится не так высоко, поэтому в ранних спринтах ей внимание не уделяют. А значит, необходимо как-то интегрировать обеспечение безопасности в agile-процесс.

Один из способов раннего обеспечения безопасности при agile-разработке заключается в составлении «историй зла» (evil stories) — рассмотрении возможностей злоупотребления атакующими той или иной функциональностью. Затем разработка идет по двум направлениям: реализация пользовательских историй (требований, сформулированных пользователем) и защита от реализации «историй зла». Еще одна практика интеграции принципов безопасности в agile-разработку — это Protection Poker, подобие карточной игры, позволяющей участникам agile-команды количественно оценивать риски безопасности. «Защитный покер» родственен широко применяемому в гибких методологиях «покеру планирования» (Planning Poker), который позволяет оценить объем усилий, необходимых для выполнения пользовательских требований.

В Microsoft относительно недавно адаптировали процесс разработки Security Development Lifecycle (SDL), рассчитанный на повышение надежности ПО, для продуктов, выпускаемых по agile-методологии, — разработчики, применяющие SDL, всерьез берутся за решение проблемы защищенности. В журнале MSDN Magazine опубликован доклад Брайана Салливэна, посвященный проблеме интеграции практик SDL в короткие циклы разработки, характерные для agile-проектов. Меры безопасности, регламентированные в SDL, автор делит на три категории: действия, обязательные для каждого спринта (например, запуск автоматизированных средств анализа безопасности и обновление модели угроз); периодические, но необязательные действия (верификация, ревизия проекта и планирование переработки); разовые задачи (например, разработка базовой модели угрозы).

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

Реальные программные системы постоянно эволюционируют — под действием изменений бизнес-требований или экономических сил добавляется новая функциональность или изымается прежняя, разрабатываются новые платформы, появляются новые технологии. В результате возникает необходимость смены парадигмы разработки программных систем, перехода на agile-методы без принесения в жертву надежности.

Важным видом эволюции является перенос ПО, особенно написанного на ассемблере, а это до сих пор актуально, учитывая, что более 70% критически важного для бизнеса ПО сейчас работает на мэйнфреймах и более 10% всего кода реализовано на ассемблере (в общей сложности примерно 140–220 млрд строк). Однако пул опытных программистов на ассемблере стремительно уменьшается. Правда, происходит отход от низкоуровневого языка, и со временем проблема унаследованного ассемблерного кода станет менее острой.

Существует agile-метод эволюции ПО, основанный на системе автоматического эквивалентного преобразования программ FermaT. Он состоит из четырех этапов: перевод ассемблерного кода на язык Wide Spectrum Language, трансляция и реструктуризация объявлений типов данных, преобразование кода WSL, перевод кода WSL на целевой язык с анализом и повышением уровня абстрагирования. Данный подход позволяет применять формализованную agile-методологию для эволюции ПО.

Трансформация алгоритма программирования

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

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

Данный метод применялся для решения описанной Дональдом Кнутом задачи сложения многочленов на основе использования четырехнаправленных связных списков. Выяснилось, что выведенный исходный код работает вдвое быстрее, чем реализация Кнута. Тот же метод применялся для выведения алгоритма умножения многочленов с использованием аналогичных структур данных. Вначале была просто изменена формальная спецификация («+» заменили на «*»), а преобразование осуществлялось с использованием тех же неформальных идей, что и для алгоритма сложения. В результате была получена эффективная реализация умножения многочленов, заработавшая с первого раза.

***

Объединение формальных и agile-методов разработки ПО, безусловно, важная задача. Но применение тяжеловесных формальных методов полного доказательства отсутствия дефектов, скорее всего, будет слишком сложным и нецелесообразным для типичного agile-процесса. Этого практически и не делают из-за проблем с масштабированием и сложности использования доступных инструментов. Более типичен облегченный вариант, при котором формальные методы применяются только на ранних этапах для улучшения понимания проекта и, возможно, при тестировании. При разработке безопасных систем придется решать дополнительные проблемы, но и здесь сочетание формальных и agile-методов может быть эффективным. Мало того, agile-подход пригодится и в том случае, когда потребуется целиком переписать ПО на новом языке, а формальный фундамент позволит уверенно проводить agile-эволюцию больших программных систем.

Литература

1. J.P. Bowen, M.G. Hinchey. Ten Commandments of Formal Methods…Ten Years Later. Computer, vol. 39, no. 1, 2006, P. 40–48.
2. J.P. Bowen, M.G. Hinchey. Formal Methods. Computing Handbook, 2nd ed., vol. 1, CRC Press, 2014, P. 1–25.
3. R.M. Hierons et al. Using Formal Specifications to Support Testing. ACM Computing Surveys, vol. 41, no. 2, 2009; doi:10.1145/1459352.1459354.

Джонатан Бауэн (jonathan.bowen@bcu.ac.uk) — профессор, Бирмингемский университет; Майк Хинчи (hinchey@lero.ie) — профессор, Лимерикский университет (Ирландия); Хельге Янике (heljanick@dmu.ac.uk) — преподаватель, Мартин Уорд (martin@gkc.org.uk) — преподаватель, Университет Де Монфор (Великобритания); Хуссейн Зедан (hussein.zedan@gmail.com) — декан, Университет прикладных наук (Бахрейн).