На чем зиждется уверенность в правильности ПО

Однако при сравнении мира разработки типичных ИТ-приложений с миром технических систем происходит интересный концептуальный сдвиг. ИТ-приложения в значительной степени представляют собой системы программного обеспечения. В технических же системах, по определению, есть ряд внепрограммных областей (электроника, механика, оптика и т.п.), в которых работает система. Эти другие контексты, как представляется, ведут к тонкому, но возможно, существенно иному способу рассмотрения таких понятий, как требования, конструкции и тесты, и иному способу определения связей между ними. В типичном ИТ-проекте эти понятия тщательно изолируются по практическим, часто договорным причинам и по соображениям валидации и верификации. Но при системотехническом подходе в определенных обстоятельствах такое разделение задач (и обязанностей) менее очевидно. Эта ситуация ставит вопрос о том, как выполнить достаточно независимую валидацию и верификацию в системотехнике. Когда в игру вступают формальные методы, связь между различными техническими артефактами становится еще теснее.

Различие между подходами на основе моделей и формальными подходами

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

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

Рисунок 1. Триада проверки требований, кода и тестирования

Это существенно упрощенное представление процесса верификации программного обеспечения показывает, что из сформулированных требований относительно независимо получаются код и тесты. Затем код проверяется тестами на соответствие требованиям. Этот цикл представляет собой широко признанный подход к валидации и верификация систем программного обеспечения. В некотором смысле код и тесты - это разные интерпретации требований (несмотря на то, что те и другие в конечном итоге - исполняемые интерпретации).

Источник расхождений между тестами и кодом

Что происходит, когда выполнение приводит к неожиданным результатам? В этот момент расхождения между кодом и тестами позволяют глубже проанализировать тонкие различия в толкованиях первоначальных требований в коде и в тестах. Они также предоставляет возможность более детального проанализировать сами спецификации требований. Без проверки нельзя сказать, какой из трех элементов виноват в том, что выполнение теста приводит к неожиданному результату. Источником расхождений между фактическим и ожидаемым результатами могут быть тесты, код или и то, и другое (и даже требования, а иногда и выполнение).

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

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

Результаты, когда требования, код и тесты независимы

Что происходит в том случае, когда требования, код и тесты не столь независимы, как это предполагается в упрощенном представлении на рисунке 1? В частности, что происходит, когда код, или тесты, или то и другое находятся в некоторой логической зависимости от спецификации системы или проистекает из нее? Как показано на рисунке 2, разработка на основе моделей и тестирование на основе моделей - популярные тенденции в области программного обеспечения, которые не укладываются в тривиальные рамки независимости, требуемой триадной моделью верификации. Кажется, что они нарушают независимость триады, потому что в первоначальную спецификацию и фактическую реализацию системы вводится строгая логическая связь. Таким образом, тестирование по первоначальной спецификации в случае сгенерированной программной системы становится замкнутым кругом, так как нет места для расхождений между абстрактной спецификацией и сгенерированной реализацией. Так как же в случае проектирования на основе моделей и проектирования по формальной спецификации узнать, что система достигает цели, до ее развертывания?

Рисунок 2. Верификация сгенерированного кода

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

Если сравнить дополнительные усилия на исправление ошибок, не обнаруживаемых вследствие потери независимости реализации тестов, то можно подумать, что преимущества, показанные в левой части рисунка 2, утрачены. Как ни странно, на практике эта утрата не происходит. Как это объяснить, пользуясь элементарной теорией познания?

Верификация и валидация

Верификация устанавливает соответствие системы установленным для нее требованиям. Валидация часто определяется как проверка соответствия системы потребностям ее конечных пользователей и в первую очередь проверка правильности самих требований. Барри Боем популярно объяснил разницу между валидацией и верификацией в форме двух вопросов: "Правильная ли система построена?" и "Правильно ли построена система?".

Это различие важно, потому что оно помогает уточнить, как формальные спецификации и разработка на основе моделей улучшают процесс проектирования систем. Строгость, обеспечиваемая абстрактной формальной спецификацией, позволяет выполнить гораздо более интенсивную валидацию требований и реализации проекта и кода. Она также позволяет выполнить валидацию намного раньше (и более полно), чем это возможно при упрощенном представлении, показанном на рисунке 1. Это упрощенное представление воплощено в большом количестве организаций по разработке программного обеспечения и систем.

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

Рисунок 3. Валидация с верификацией и формальная спецификация

Заключение

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